tortoise_hare.mlw 1.73 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 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

(* Floyd's ``the tortoise and the hare'' algorithm. *)

module TortoiseHare

  use import int.Int

  (* We consider a function f over an abstract type t *)

  type t

  logic f t : t

  (* Given some x0 in t, we consider the sequence of the repeated calls 
     to f starting from x0. *)

  logic x int : t

  axiom xdef: forall n:int. n >= 0 -> x (n+1) = f (x n)

  logic x0 : t = x 0

  (* If t is finite, this sequence will eventually end up on a cycle.
     Let us simply assume the existence of this cycle, that is
     x (i + lambda) = x i, for some lambda > 0 and i large enough. *)

  logic mu : int
  axiom mu: mu >= 0

  logic lambda : int
  axiom lambda: lambda >= 1

  axiom cycle: forall i:int. mu <= i -> x (i + lambda) = x i

  lemma cycle_gen: 
    forall i:int. mu <= i -> forall k:int. 0 <= k -> x (i + lambda * k) = x i

  (* The challenge is to prove that the recursive function
    
       let rec run x1 x2 = if x1 <> x2 then run (f x1) (f (f x2))

     terminates when called on x0 and (f x0).
  *)

  logic dist int int : int

  axiom dist_def1: 
    forall n m: int. 0 <= n <= m -> 
    x (n + dist n m) = x m
  axiom dist_def2:
    forall n m: int. 0 <= n <= m -> 
    forall k: int. x (n + k) = x m -> dist n m <= k

  logic r (x12 : (t, t)) (x'12 : (t, t)) =
    let x1, x2 = x12 in 
    let x'1, x'2 = x'12 in
    exists m:int. 
    x1 = x (m+1) and x2 = x (2*m+2) and x'1 = x m and x'2 = x (2*m) and
    m < mu or (mu <= m and dist (m+1) (2*m+2) < dist m (2*m))
  
  let rec run x1 x2 variant { (x1, x2) } with r =
    { exists m:int [x m]. x1 = x m and x2 = x (2*m) }
    if x1 <> x2 then
      run (f x1) (f (f x2))
    { }

end

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_hare.gui"
End: 
*)