Commit 8a6f9e75 by Jean-Christophe Filliâtre

### tortoise and hare example totally revamped

`this is much closer now to TAOCP, vol 2, exercise 6 page 7`
parent 626ca4d8
 ... @@ -3,88 +3,162 @@ ... @@ -3,88 +3,162 @@ See The Art of Computer Programming, vol 2, exercise 6 page 7. *) See The Art of Computer Programming, vol 2, exercise 6 page 7. *) module TortoiseAndHare module TortoiseAndHareAlgorithm use import int.Int use import int.Int use int.Iter use import int.EuclideanDivision use import int.Iter use import seq.Seq use import seq.Distinct use import ref.Refint use import pigeon.Pigeonhole type t val function f int : int val predicate eq (x y : t) ensures { result <-> x = y } (* let f be a function from t to t *) (* f maps 0..m-1 to 0..m-1 *) val function f t : t constant m: int axiom m_positive: m > 0 axiom f_range: forall x. 0 <= x < m -> 0 <= f x < m (* given some initial value x0 *) (* given some initial value x0 *) val constant x0: t val constant x0: int ensures { 0 <= result < m } (* we can build the infinite sequence defined by x{i+1} = f(xi) *) (* we can build the infinite sequence defined by x{i+1} = f(xi) *) function x (i: int): t = Iter.iter f i x0 function x (i: int): int = iter f i x0 (* let use assume now that the sequence (x_i) has finitely many distinct let rec lemma x_in_range (n: int) values (e.g. f is an integer function with values in 0..m) requires { 0 <= n } ensures { 0 <= x n < m } variant { n } it means that there exists values lambda and mu such that = if n > 0 then x_in_range (n - 1) (1) x0, x1, ... x{mu+lambda-1} are all distinct, and (* First, we prove the existence of mu and lambda, with a ghost program. (2) x{n+lambda} = x_n when n >= mu. *) Starting with x0, we repeteadly apply f, storing the elements in a sequence, until we find a repetition. *) (* lambda and mu are skomlemized *) let ghost periodicity () : (int, int) constant mu : int returns { mu, lambda -> constant lambda : int 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ x (mu + lambda) = x mu /\ (* they are axiomatized as follows *) forall i j. 0 <= i < j < mu + lambda -> x i <> x j axiom mu_range: 0 <= mu } = let s = ref (singleton x0) in axiom lambda_range: 1 <= lambda let cur = ref x0 in for k = 1 to m do axiom distinct: invariant { 1 <= length !s = k <= m /\ !cur = !s[length !s - 1] } forall i j: int. 0 <= i < mu+lambda -> 0 <= j < mu+lambda -> invariant { forall i. 0 <= i < length !s -> !s[i] = x i } i <> j -> x i <> x j invariant { distinct !s } cur := f !cur; axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n (* look for a repetition *) for mu = 0 to length !s - 1 do lemma cycle_induction: invariant { forall i. 0 <= i < mu -> !s[i] <> !cur } forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n if !cur = !s[mu] then return (mu, length !s - mu) done; (* Now comes the code. s := snoc !s !cur; Two references, tortoise and hare, traverses the sequence (xi) if k = m then pigeonhole (m+1) m (pure { fun i -> !s[i] }) at speed 1 and 2 respectively. We stop whenever they are equal. done; absurd The challenge is to prove termination. Actually, we even prove that the code runs in time O(lambda + mu). *) (* Then we can state the condition for two elements to be equal. *) let lemma equality (mu lambda: int) use import ref.Ref requires { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ use import relations.WellFounded x (mu + lambda) = x mu } requires { forall i j. 0 <= i < j < mu + lambda -> x i <> x j } (* the minimal distance between x i and x j *) ensures { forall r n. r > n >= 0 -> function dist int int : int x r = x n <-> n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } = let rec lemma plus_lambda (n: int) variant { n } (* it is defined as soon as i,j >= mu *) requires { mu <= n } axiom dist_def: forall i j: int. mu <= i -> mu <= j -> ensures { x (n + lambda) = x n } = dist i j >= 0 /\ if n > mu then plus_lambda (n - 1) in x (i + dist i j) = x j /\ let rec lemma plus_lambdas (n k: int) variant { k } forall k: int. 0 <= k -> x (i + k) = x j -> dist i j <= k requires { mu <= n } requires { 0 <= k } ensures { x (n + k * lambda) = x n } = predicate rel (t2 t1: t) = if k > 0 then begin exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda /\ plus_lambdas n (k - 1); plus_lambda (n + (k - 1) * lambda) end in (i >= mu -> dist (2*i+2) (i+1) < dist (2*i) i) let decomp (i: int) : (int, int) requires { i >= mu } axiom wfrel: well_founded rel returns { qi,mi -> i = mu + qi * lambda + mi && qi >= 0 && 0 <= mi < lambda && x i = x (mu + mi) } = let tortoise_hare () = let qi = div (i - mu) lambda in let mi = mod (i - mu) lambda in plus_lambdas (mu + mi) qi; qi, mi in let lemma equ (r n: int) requires { r > n >= 0 } requires { x r = x n } ensures { n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } = if n < mu then (if r >= mu then let _ = decomp r in absurd) else begin let qr,mr = decomp r in let qn, mn = decomp n in assert { mr = mn }; assert { r-n = (qr-qn) * lambda } end in () (* Finally, we implement the tortoise and hare algorithm that computes the values of mu and lambda in linear time and constant space *) let tortoise_and_hare () : (int, int) returns { mu, lambda -> 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ x (mu + lambda) = x mu /\ forall i j. 0 <= i < j < mu + lambda -> x i <> x j } = let mu, lambda = periodicity () in equality mu lambda; (* the first loop implements the tortoise and hare, and finds the smallest n >= 1 such that x n = x (2n) *) let tortoise = ref (f x0) in let tortoise = ref (f x0) in let hare = ref (f (f x0)) in let hare = ref (f (f x0)) in while not (eq !tortoise !hare) do let n = ref 1 in while !tortoise <> !hare do invariant { invariant { exists t: int. 1 <= !n <= mu+lambda /\ !tortoise = x !n /\ !hare = x (2 * !n) /\ 1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\ forall i. 1 <= i < !n -> x i <> x (2*i) } forall i: int. 1 <= i < t -> x i <> x (2*i) } variant { mu + lambda - !n } variant { !tortoise with rel } tortoise := f !tortoise; tortoise := f !tortoise; hare := f (f !hare) hare := f (f !hare); done incr n; if !n > mu + lambda then begin (* TODO: code to find out lambda and mu. See wikipedia. *) let m = lambda - mod mu lambda in let i = mu + m in assert { 2*i - i = (div mu lambda + 1) * lambda }; absurd end done; let n = !n in assert { n >= mu }; assert { exists k. k >= 1 /\ n = k * lambda >= 1 }; assert { forall j. j >= mu -> x j = x (j + n) }; let xn = !tortoise in (* a first loop to find mu *) let i = ref 0 in let xi = ref x0 in (* = x i *) let xni = ref xn in (* = x (n+i) *) while !xi <> !xni do invariant { 0 <= !i <= mu } invariant { !xi = x !i /\ !xni = x (n + !i) } invariant { forall j. 0 <= j < !i -> x j <> x (n + j) } variant { mu - !i } xi := f !xi; xni := f !xni; incr i; done; let m = !i in assert { m = mu }; (* and a second loop to find lambda (this is slightly less efficient than the argument in TAOCP, but since the first loop is already O(mu+lambda), using two loops respectively O(mu) and O(lambda) is not a problem). *) i := 1; xni := f xn; while !xni <> xn do invariant { !xni = x (n + !i) } invariant { forall j. 1 <= j < !i -> x (n + j) <> x n } invariant { 1 <= !i <= lambda } variant { lambda - !i } xni := f !xni; incr i done; assert { !i = lambda }; m, !i end end
 ... @@ -2,30 +2,370 @@ ... @@ -2,30 +2,370 @@ "http://why3.lri.fr/why3session.dtd">