tortoise_and_hare.mlw 5.54 KB
Newer Older
1 2 3 4 5

(* Floyd's cycle detection, also known as ``tortoise and hare'' algorithm.

   See The Art of Computer Programming, vol 2, exercise 6 page 7. *)

6
module TortoiseAndHareAlgorithm
7 8

  use import int.Int
9 10 11 12 13 14
  use import int.EuclideanDivision
  use import int.Iter
  use import seq.Seq
  use import seq.Distinct
  use import ref.Refint
  use import pigeon.Pigeonhole
15

16
  val function f int : int
17

18 19 20 21 22
  (* f maps 0..m-1 to 0..m-1 *)
  constant m: int
  axiom m_positive: m > 0

  axiom f_range: forall x. 0 <= x < m -> 0 <= f x < m
23

24
  (* given some initial value x0 *)
25 26
  val constant x0: int
    ensures { 0 <= result < m }
27

28
  (* we can build the infinite sequence defined by x{i+1} = f(xi) *)
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  function x (i: int): int = iter f i x0

  let rec lemma x_in_range (n: int)
    requires { 0 <= n } ensures { 0 <= x n < m }
    variant  { n }
  = if n > 0 then x_in_range (n - 1)

  (* First, we prove the existence of mu and lambda, with a ghost program.
     Starting with x0, we repeteadly apply f, storing the elements in
     a sequence, until we find a repetition. *)
  let ghost periodicity () : (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 s = ref (singleton x0) in
    let cur = ref x0 in
    for k = 1 to m do
      invariant { 1 <= length !s = k <= m /\ !cur = !s[length !s - 1] }
      invariant { forall i. 0 <= i < length !s -> !s[i] = x i }
      invariant { distinct !s }
      cur := f !cur;
      (* look for a repetition *)
      for mu = 0 to length !s - 1 do
        invariant { forall i. 0 <= i < mu -> !s[i] <> !cur }
        if !cur = !s[mu] then return (mu, length !s - mu)
      done;
      s := snoc !s !cur;
      if k = m then pigeonhole (m+1) m (pure { fun i -> !s[i] })
    done;
    absurd

  (* Then we can state the condition for two elements to be equal. *)
  let lemma equality (mu lambda: int)
    requires { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
               x (mu + lambda) = x mu }
    requires { forall i j. 0 <= i < j < mu + lambda -> x i <> x j }
    ensures  { forall r n. r > n >= 0 ->
               x r = x n <-> n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda }
  = let rec lemma plus_lambda (n: int) variant { n }
      requires { mu <= n }
      ensures  { x (n + lambda) = x n } =
      if n > mu then plus_lambda (n - 1) in
    let rec lemma plus_lambdas (n k: int) variant { k }
      requires { mu <= n } requires { 0 <= k }
      ensures  { x (n + k * lambda) = x n } =
      if k > 0 then begin
        plus_lambdas n (k - 1); plus_lambda (n + (k - 1) * lambda) end in
    let decomp (i: int) : (int, int)
      requires { i >= mu }
      returns  { qi,mi -> i = mu + qi * lambda + mi && qi >= 0 &&
                 0 <= mi < lambda && x i = x (mu + mi) } =
      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) *)
109 110
    let tortoise = ref (f x0) in
    let hare = ref (f (f x0)) in
111 112
    let n = ref 1 in
    while !tortoise <> !hare do
113
      invariant {
114 115 116
        1 <= !n <= mu+lambda /\ !tortoise = x !n /\ !hare = x (2 * !n) /\
        forall i. 1 <= i < !n -> x i <> x (2*i) }
      variant { mu + lambda - !n }
117
      tortoise := f !tortoise;
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
      hare     := f (f !hare);
      incr n;
      if !n > mu + lambda then begin
        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
163 164

end