Examples  

Addition and multiplication  

On the natural numbers

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

we define add ,mult : nat $\rightarrow$ nat $\rightarrow$ 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()))));

foetus output:

< =: 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.

Subtraction  

We define the predecessor function p : nat $\rightarrow$ nat and substraction on natural numbers sub : nat $\rightarrow$ nat $\rightarrow$ nat . Note sub x y calculates y$\;\stackrel{\cdot}{-}\;$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) };
sub (S(S(O()))) (S(S(S(S(O())))));

foetus output:

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

Run example.

Division  

Division div : nat $\rightarrow$ nat $\rightarrow$ nat can be implemented as follows in functional languages (note that div x y calculates $\lfloor$${\frac{y}{x}}$$\rfloor$ ):

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

div' (just like division on natural numbers) terminates if the divisor x is unequal 0 because then y-x < y in the recursive call and thus one function argument is decreasing. But foetus recognizes only direct structural decrease and cannot see that sub x y' is less than y'. To prove termination of div' you need a proof for x $\not=$0 $\rightarrow$ sub x y < y [BG96].

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()))))));

foetus output:

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 foetus says div' fails termination check, so div will not terminate either. div would terminate, if div' terminated, therefore you get the answer div passes termination check. Run example.

Ackermann function  

The not primitive recursive Ackermann function ack : nat $\rightarrow$ nat $\rightarrow$ nat .

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 output:

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 processing  

We define lists over type $\alpha$ as

list : = {$$\alpha$$}Let list = {Nil () |Cons(HD : $$\alpha$$,TL : list ) } in list

The well-known list processing functions map : ($\alpha$ $\rightarrow$ $\beta$) $\rightarrow$ list $\alpha$ $\rightarrow$ list $\beta$ and foldl : ($\alpha$ $\rightarrow$ $\beta$ $\rightarrow$ $\beta$) $\rightarrow$ $\beta$ $\rightarrow$ list $\alpha$ $\rightarrow$ $\beta$ are implemented and testet.

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;

foetus output:

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.

List flattening  

The task is to transform a list of lists into a list, so that the elements of the first list come first, then the elements of the second list and so on. Example: flatten [[A,B,C],[D,E,F]] = [A,B,C,D,E,F]. The first version flatten : list(list $\alpha$) $\rightarrow$ list $\alpha$ works but fails termination check because of the limited pattern matching abilities of foetus, but it is also bad style and inefficient because it builds a temporary list for the recursive call. However, the second version f with a mutual recursive auxiliary function g : list $\alpha$ $\rightarrow$ list(list $\alpha$) $\rightarrow$ list $\alpha$ passes termination check.

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;

foetus output:

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.

Merge sort

With type

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

we can define le_nat : nat $\rightarrow$ nat $\rightarrow$ bool and merge : ($\alpha$ $\rightarrow$ $\alpha$ $\rightarrow$ bool ) $\rightarrow$ list $\alpha$ $\rightarrow$ list $\alpha$ $\rightarrow$ list $\alpha$ as follows:

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;

foetus output:

= < <: 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.

Parameter permutation: list zipping  

The following function zip : list $\alpha$ $\rightarrow$ list $\alpha$ $\rightarrow$ list $\alpha$ combines two lists into one by alternately taking the first elements form these lists and putting them into the result list.

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())));

foetus output:

? ?: 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 zip one arguments is decreasing, but arguments are switched. Thus only a even number of recursive calls produces a structural decrease on l1 and l2. foetus does not recognize zip to be terminating because not every (direct or indirect) recursive call makes the arguments smaller on any structural lexical order.

Of course there are simple orders that fulfill the demanded criteria, like < on |l1| + |l2| . 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())));

foetus output:

< <: 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.

Tuple parameter  

This example, an alternative version of add : (X : nat ,Y : nat ) $\rightarrow$ nat , shows that foetus loses dependency information if you ``pack'' and ``unpack'' tuples.

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

foetus output:

?: add -> add
add FAILS termination check

Run example.

Transfinite addition of ordinal numbers  

The type of ordinal numbers is

ord : = Let ord = {O() |S( ord ) |Lim( nat $$\rightarrow$$ ord ) } in ord

and addord : ord $\rightarrow$ ord $\rightarrow$ ord can be implemented as follows:

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

foetus output:

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

Run example.

Fibonacci numbers  

Iterative version fib : nat $\rightarrow$ nat of algorithm to calculate the fibonacci numbers fib (0) = 1 , fib (1) = 1 , 2, 3, 5, 8, ... . Only the first parameter is important for termination, the second and the third parameter are ``accumulators''.

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());

foetus output:

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

Run example.

Non-terminating mutual recursion

The following three functions f ,g ,h : nat $\rightarrow$ nat $\rightarrow$ nat are an artificial example for non-termination that has been designed to show to what extent the call graph has to be completed to assure correct results of the termination checker. Function h (here h(x,y) = 0  $\forall$x,y ) could be any function that ``looks into'' its arguments, e.g. add.

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()))); *)

foetus output: Note that the combined call f $\rightarrow$ g $\rightarrow$ f still does not prevent termination. But then call graph completion finds f $\rightarrow$ g $\rightarrow$ g $\rightarrow$ f that destroys the lexical order 1 0 that was possible until then.

< <: 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 check

Run example.