(* 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
use int.Iter
type t
val predicate eq (x y : t)
ensures { result <-> x = y }
(* let f be a function from t to t *)
val function f t : t
(* given some initial value x0 *)
val constant x0: t
(* we can build the infinite sequence defined by x{i+1} = f(xi) *)
function x (i: int): t = Iter.iter f 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. *)
(* lambda and mu are skomlemized *)
constant mu : int
constant lambda : int
(* they are axiomatized as follows *)
axiom mu_range: 0 <= mu
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
lemma cycle_induction:
forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n
(* Now comes the code.
Two references, tortoise and hare, traverses the sequence (xi)
at speed 1 and 2 respectively. We stop whenever they are equal.
The challenge is to prove termination.
Actually, we even prove that the code runs in time O(lambda + mu). *)
use import ref.Ref
use import relations.WellFounded
(* 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
predicate rel (t2 t1: t) =
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)
axiom wfrel: well_founded rel
let tortoise_hare () =
let tortoise = ref (f x0) in
let hare = ref (f (f x0)) in
while not (eq !tortoise !hare) do
invariant {
exists t: int.
1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\
forall i: int. 1 <= i < t -> x i <> x (2*i) }
variant { !tortoise with rel }
tortoise := f !tortoise;
hare := f (f !hare)
done
(* TODO: code to find out lambda and mu. See wikipedia. *)
end