tortoise_and_hare.mlw 2.43 KB
 Jean-Christophe Filliatre committed Aug 05, 2011 1 2 3 4 5 6 7 8 9 `````` (* Floyd's cycle detection, also known as ``tortoise and hare'' algorithm. See The Art of Computer Programming, vol 2, exercise 6 page 7. *) module TortoiseAndHare use import int.Int `````` Jean-Christophe Filliatre committed Aug 05, 2011 10 11 12 `````` (* let f be a function from t to t *) type t function f t : t `````` Jean-Christophe Filliatre committed Aug 05, 2011 13 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 14 `````` (* given some initial value x0 *) `````` Jean-Christophe Filliatre committed Feb 06, 2012 15 `````` constant x0: t `````` Jean-Christophe Filliatre committed Aug 05, 2011 16 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 17 18 19 20 21 22 23 24 25 26 27 `````` (* we can build the infinite sequence defined by x{i+1} = f(xi) *) clone import int.Iter with type t = t, function f = f function x (i: int): t = iter i x0 (* let use assume now that the sequence (x_i) has finitely many distinct values (e.g. f is an integer function with values in 0..m) it means that there exists values lambda and mu such that (1) x0, x1, ... x{mu+lambda-1} are all distinct, and (2) x{n+lambda} = x_n when n >= mu. *) `````` Jean-Christophe Filliatre committed Aug 05, 2011 28 29 `````` (* lambda and mu are skomlemized *) `````` Jean-Christophe Filliatre committed Feb 06, 2012 30 31 `````` constant mu : int constant lambda : int `````` Jean-Christophe Filliatre committed Aug 05, 2011 32 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 33 `````` (* they are axiomatized as follows *) `````` Jean-Christophe Filliatre committed Aug 05, 2011 34 `````` axiom mu_range: 0 <= mu `````` Jean-Christophe Filliatre committed Aug 05, 2011 35 `````` `````` Jean-Christophe Filliatre committed Aug 05, 2011 36 37 38 39 40 41 42 43 `````` axiom lambda_range: 1 <= lambda axiom distinct: forall i j: int. 0 <= i < mu+lambda -> 0 <= j < mu+lambda -> i <> j -> x i <> x j axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n `````` Jean-Christophe Filliatre committed Aug 05, 2011 44 45 46 `````` lemma cycle_induction: forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n `````` Jean-Christophe Filliatre committed Aug 05, 2011 47 `````` (* Now comes the code. `````` Jean-Christophe Filliatre committed Aug 05, 2011 48 49 `````` Two references, tortoise and hare, traverses the sequence (xi) at speed 1 and 2 respectively. We stop whenever they are equal. `````` Jean-Christophe Filliatre committed Aug 05, 2011 50 51 52 53 `````` The challenge is to prove termination. Actually, we even prove that the code runs in time O(lambda + mu). *) `````` Andrei Paskevich committed Oct 13, 2012 54 `````` use import ref.Ref `````` Jean-Christophe Filliatre committed Aug 05, 2011 55 `````` `````` Jean-Christophe Filliatre committed Aug 16, 2011 56 57 58 59 60 61 62 63 64 `````` (* the minimal distance between x i and x j *) function dist int int : int (* it is defined as soon as i,j >= mu *) axiom dist_def: forall i j: int. mu <= i -> mu <= j -> dist i j >= 0 /\ x (i + dist i j) = x j /\ forall k: int. 0 <= k -> x (i + k) = x j -> dist i j <= k `````` Jean-Christophe Filliatre committed Aug 05, 2011 65 `````` predicate rel (t2 t1: t) = `````` Jean-Christophe Filliatre committed Aug 16, 2011 66 67 `````` exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda /\ (i >= mu -> dist (2*i+2) (i+1) < dist (2*i) i) `````` Jean-Christophe Filliatre committed Aug 05, 2011 68 69 70 71 72 73 74 `````` let tortoise_hare () = let tortoise = ref (f x0) in let hare = ref (f (f x0)) in while !tortoise <> !hare do invariant { exists t: int. `````` Jean-Christophe Filliatre committed Aug 05, 2011 75 `````` 1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\ `````` Jean-Christophe Filliatre committed Aug 05, 2011 76 `````` forall i: int. 1 <= i < t -> x i <> x (2*i) } `````` Andrei Paskevich committed Oct 13, 2012 77 `````` variant { !tortoise with rel } `````` Jean-Christophe Filliatre committed Aug 05, 2011 78 79 80 81 82 83 84 `````` tortoise := f !tortoise; hare := f (f !hare) done (* TODO: code to find out lambda and mu. See wikipedia. *) end``````