Wiki Agenda Contact Version française

McCarthy's 91 function

Two different versions of McCarthy's 91 function:

Both implementations are interesting examples of termination proofs.

For the recursive implementation to be proved terminating, that is to prove that the variant 101-n decreases, we must actually establish a behavioral postcondition, which is here (n <= 100 and result = 91) or (n >= 101 and result = n - 10).

For the non-recursive implementation to be proved terminating, we need a lexicographic ordering.


Authors: Jean-Christophe Filliâtre

Topics: Tricky termination / Historical examples

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


(* McCarthy's ``91'' function. *)

module McCarthy91

  use import int.Int

  (* traditional recursive implementation *)

  let rec f91 (n:int) : int variant { 101-n }
    ensures { result = if n <= 100 then 91 else n - 10 }
  = if n <= 100 then
      f91 (f91 (n + 11))
    else
      n - 10

  (* non-recursive implementation using a while loop *)

  use import ref.Ref

  function f (x: int) : int = if x <= 100 then 91 else x-10

  (* iter k x = f^k(x) *)
  clone import int.Iter with type t = int, function f = f

  let f91_nonrec (n0: int) ensures { result = f n0 }
  = let e = ref 1 in
    let n = ref n0 in
    while !e > 0 do
      invariant { !e >= 0 /\ iter !e !n = f n0 }
      variant   { 101 - !n + 10 * !e, !e }
      if !n > 100 then begin
        n := !n - 10;
        e := !e - 1
      end else begin
        n := !n + 11;
        e := !e + 1
      end
    done;
    !n

end

download ZIP archive