1(*---------------------------------------------------------------------------*)
2(* Tail recursive version of Ackermann's function.                           *)
3(*---------------------------------------------------------------------------*)
4
5val ackTail = 
6  ``(Ack [] y = y) /\
7    (Ack (0::t) y = Ack t (y+1)) /\
8    (Ack (n::t) 0 = Ack ((n-1)::t) 1) /\
9    (Ack (n::t) y = Ack (n::n-1::t) y)``;
10
11Fact: ack x y = Ack [x] y
12
13(* ---------------------------------------------------------------------------*)
14(* Termination of ackTail ... multiset order probably.                        *)
15(* ---------------------------------------------------------------------------*)
16
17val f91Tail =
18  ``t91 n z =
19     if n=0 then z else
20     if 100<z then t91 (n-1) (z-10)
21     else t91 (n+1) (z+11)``;
22
23Fact: f91 n = f91Tail 1 n
24
25
26