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