- Addition and multiplication
- Subtraction
- Division
- Ackermann function
- List processing
- List flattening
- Merge sort
- Parameter permutation: list zipping
- Tuple parameter
- Transfinite addition of ordinal numbers
- Fibonacci numbers
- Non-terminating mutual recursion

nat : = Let nat = {`O`() |`S`( nat ) } in nat

add = [x][y]case x of { O z => y | S x' => S(add x' y) }; mult = [x][y]case x of { O z => O z | S x' => (add y (mult x' y)) }; add (S(S(O()))) (S(O())); mult (S(S(O()))) (S(S(S(O()))));

< =: add -> add add passes termination check by lexical order 0 < =: mult -> mult mult passes termination check by lexical order 0 result: S(S(S(O()))) result: S(S(S(S(S(S(O()))))))Run example.

p = [x]case x of { O z => O z | S x' => x' }; sub = [x][y]case x of { O z => y | S x' => sub x' (p y) }; sub (S(S(O()))) (S(S(S(S(O())))));

p passes termination check < ?: sub -> sub sub passes termination check by lexical order 0 result: S(S(O()))Run example.

div (x,y) = div'(x,y+1-x) div'(x,y) = if (y=0) then 0 else div'(x,y-x)

p = [x]case x of { O z => O z | S x' => x' }; sub = [x][y]case x of { O z => y | S x' => sub x' (p y) }; div = [x][y]let div' = [y']case y' of { O z => O z | S dummy => S(div' (sub x y')) } in (div' (sub (p x) y)); div (S(S(O()))) (S(S(S(S(S(O()))))));

p passes termination check < ?: sub -> sub sub passes termination check by lexical order 0 div passes termination check ?: div' -> div' div' FAILS termination check result: S(S(O()))Here

ack = [x][y]case x of { O z => S(y) | S x' => ack x' (case y of { O z => S(O()) | S y' => ack x y'} ) }; ack (S(S(O()))) (O());

foetus $Revision: 1.0 $ = <: ack -> ack < ?: ack -> ack ack passes termination check by lexical order 0 1 result: S(S(S(O())))Run example.

list : = {}Let list = {`Nil` () |`Cons`(`HD` : `,TL` : list ) } in list

nil = Nil(); cons = [hd][tl]Cons(HD=hd,TL=tl); l1 = cons (A()) (cons (B()) (cons (C()) nil)); map = [f][list]let map' = [l]case l of { Nil z => Nil() | Cons pair => Cons (HD=(f pair.HD), TL=(map' pair.TL))} in map' list; map ([el]F(el)) l1; foldl = [f][e][list]let foldl' = [e][l]case l of { Nil z => e | Cons p => foldl' (f p.HD e) p.TL } in foldl' e list; rev = [list]foldl cons nil list; rev l1;

nil passes termination check cons passes termination check l1 passes termination check map passes termination check <: map' -> map' map' passes termination check by lexical order 0 result: Cons(HD=F(A()), TL=Cons(HD=F(B()), TL=Cons(HD=F(C()), TL=Nil()))) foldl passes termination check ? <: foldl' -> foldl' foldl' passes termination check by lexical order 1 rev passes termination check result: Cons(HD=C(), TL=Cons(HD=B(), TL=Cons(HD=A(), TL=Nil())))Run example.

nil = Nil(); cons = [hd][tl]Cons(HD=hd,TL=tl); l1 = cons (A()) (cons (B()) (cons (C()) nil)); ll = (cons l1 (cons l1 nil)); flatten = [listlist]case listlist of { Nil z => Nil() | Cons p => case p.HD of { Nil z => flatten p.TL | Cons p' => Cons(HD=p'.HD, TL=flatten (Cons(HD=p'.TL, TL=p.TL))) }}; flatten ll; f = [l]case l of { Nil z => Nil() | Cons p => g p.HD p.TL }, g = [l][ls]case l of { Nil z => f ls | Cons p => Cons(HD=p.HD, TL=(g p.TL ls)) }; f ll;

nil passes termination check cons passes termination check l1 passes termination check ll passes termination check ?: flatten -> flatten <: flatten -> flatten flatten FAILS termination check result: Cons(HD=A(), TL=Cons(HD=B(), TL=Cons(HD=C(), TL=Cons(HD=A(), TL=Cons(HD=B(), TL=Cons(HD=C(), TL=Nil())))))) <: f -> g -> f f passes termination check by lexical order 0 ? <: g -> f -> g < =: g -> g g passes termination check by lexical order 1 0 result: Cons(HD=A(), TL=Cons(HD=B(), TL=Cons(HD=C(), TL=Cons(HD=A(), TL=Cons(HD=B(), TL=Cons(HD=C(), TL=Nil()))))))Run example.

bool : = {`True`() |`False`() }

merge = [le][l1][l2]case l1 of { Nil z => l2 | Cons p1 => case l2 of { Nil z => l1 | Cons p2 => case (le p1.HD p2.HD) of { True z => Cons(HD=p1.HD, TL=merge le p1.TL l2) | False z => Cons(HD=p2.HD, TL=merge le l1 p2.TL) }}}; le_nat = [x][y]case x of { O z => True() | S x' => case y of { O z => False() | S y' => le_nat x' y' }}; i = S(O()); ii = S(S(O())); iii = S(S(S(O()))); iv = S(S(S(S(O())))); v = S(S(S(S(S(O()))))); l1 = Cons(HD=O(), TL=Cons(HD=iii, TL=Cons(HD=iv, TL=Nil()))); l2 = Cons(HD=i, TL=Cons(HD=ii, TL=Cons(HD=v, TL=Nil()))); merge le_nat l1 l2;

= < <: merge -> merge -> merge = = <: merge -> merge = < =: merge -> merge merge passes termination check by lexical order 1 2 < <: le_nat -> le_nat le_nat passes termination check by lexical order 0 result: Cons(HD=O(), TL=Cons(HD=S(O()), TL=Cons(HD=S(S(O())), TL=Cons(HD=S(S(S(O()))), TL=Cons(HD=S(S(S(S(O())))), TL=Cons(HD=S(S(S(S(S(O()))))), TL=Nil()))))))Run example.

zip = [l1][l2]case l1 of { Nil z => l2 | Cons p1 => Cons(HD=p1.HD, TL=zip l2 p1.TL) }; zip (Cons(HD=A(), TL=Cons(HD=C(), TL=Nil()))) (Cons(HD=B(), TL=Cons(HD=D(), TL=Nil())));

? ?: zip -> zip -> zip -> zip < <: zip -> zip -> zip ? ?: zip -> zip zip FAILS termination check result: Cons(HD=A(), TL=Cons(HD=B(), TL=Cons(HD=C(), TL=Cons(HD=D(), TL=Nil()))))Run example. Here in the recursion of

Of course there are simple orders
that fulfill the demanded criteria, like < on |*l*1| + |*l*2| .
Another solution is to ``copy'' `zip` into `zip'` and implement
*mutual recursion* as follows:

zip = [l1][l2]case l1 of { Nil z => l2 | Cons p1 => Cons(HD=p1.HD, TL=zip' l2 p1.TL) }, zip'= [l1][l2]case l1 of { Nil z => l2 | Cons p1 => Cons(HD=p1.HD, TL=zip l2 p1.TL) }; zip (Cons(HD=A(), TL=Cons(HD=C(), TL=Nil()))) (Cons(HD=B(), TL=Cons(HD=D(), TL=Nil())));

< <: zip -> zip' -> zip zip passes termination check by lexical order 0 < <: zip' -> zip -> zip' zip' passes termination check by lexical order 0 result: Cons(HD=A(), TL=Cons(HD=B(), TL=Cons(HD=C(), TL=Cons(HD=D(), TL=Nil()))))Run example.

add = [xy]case xy.X of { O z => xy.Y | S x' => S(add (X=x', Y=xy.Y)) };

?: add -> add add FAILS termination checkRun example.

ord : = Let ord = {`O`() |`S`( ord ) |`Lim`( nat ord ) } in ord

addord = [x][y]case x of { O o => y | S x' => S(addord x' y) | Lim f => Lim([z]addord (f z) y) };

< =: addord -> addord addord passes termination check by lexical order 0Run example.

fib' = [n][fn][fn']case n of { O z => fn | S n' => fib' n' (add fn fn') fn}; fib = [n]fib' n (S(O())) (O());

< ? ?: fib' -> fib' -> fib' < ? ?: fib' -> fib' fib' passes termination check by lexical order 0 fib passes termination checkRun example.

h = [x][y]case x of { O z => case y of { O z => O() | S y' => h x y' } | S x' => h x' y }, f = [x][y]case x of { O z => O() | S x' => case y of { O z => O() | S y' => h (g x' y) (f (S(S(x))) y') } }, g = [x][y]case x of { O z => O() | S x' => case y of { O z => O() | S y' => h (f x y) (g x' (S(y))) } }; (* f (S(S(O()))) (S(S(O()))); *)

< <: h -> h -> h < =: h -> h = <: h -> h h passes termination check by lexical order 0 1 < ?: f -> g -> g -> f ? ?: f -> f -> g -> g -> f < =: f -> g -> f ? <: f -> f f FAILS termination check ? <: g -> f -> f -> g ? ?: g -> g -> f -> f -> g < =: g -> f -> g < ?: g -> g g FAILS termination checkRun example.