tortoise_and_hare.mlw 2.43 KB
Newer Older
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

10 11 12
  (* let f be a function from t to t *)
  type t
  function f t : t
13

14
  (* given some initial value x0 *)
15
  constant x0: t
16

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. *)
28 29

  (* lambda and mu are skomlemized *)
30 31
  constant mu     : int
  constant lambda : int
32

33
  (* they are axiomatized as follows *)
34
  axiom mu_range: 0 <= mu
35

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

44 45 46
  lemma cycle_induction:
    forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n

47
  (* Now comes the code.
48 49
     Two references, tortoise and hare, traverses the sequence (xi)
     at speed 1 and 2 respectively. We stop whenever they are equal.
50 51 52 53

     The challenge is to prove termination.
     Actually, we even prove that the code runs in time O(lambda + mu). *)

54
  use import ref.Ref
55

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

65
  predicate rel (t2 t1: t) =
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)
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.
75
        1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\
76
        forall i: int. 1 <= i < t -> x i <> x (2*i) }
77
      variant { !tortoise with rel }
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