foetus - Termination Checker for Simple Functional Programs

Andreas Abel^{∗}

July 16, 1998

Abstract

We introduce a simple functional language foetus (lambda calculus with tuples, constructors and pattern matching) supplied with a termination checker. This checker tries to find a well-founded structural order on the parameters on the given function to prove termination. The components of the check algorithm are: function call extraction out of the program text, call graph completion and finding a lexical order for the function parameters. The HTML version of this paper contains many ready-to-run Web-based examples.

1 Introduction

Since the very beginning of informatics the problem of termination has been of special interest, for it is part of the problem of program verification for instance. Because the halting problem is undecidable, there is no method that can prove or disprove termination of all programs, but for several systems termination checkers have been developed. We have focused on functional programs and designed the simple language foetus^{1}, for which we have implemented a termination prover. foetus is a simplification of MuTTI (Munich Type Theory Implementation) based on partial Type Theory (ala Martin Löf) extended by tuples, constructors and pattern matching. For the syntax see section 2.1.

∗Theoretical Computer Science, Institute of Computer Science, Ludwigs-Maximilians-University, Oettingenstr. 67, D-80538 Munich, Germany, email:

abel@informatik.uni-muenchen.de. I want to thank my supervisor Thorsten Altenkirch and Rolf Backofen for his friendly support in technical questions.

1In German foetus is an abbreviation of “Funktionale – Obgleich Eingeschränkt – Termination Untersuchende Sprache” ;-). It also expresses that it is derived from MuTTI (this is the German term for Mum).

To prove the termination of a functional program there has to be a well founded order on the product of the function parameters such that the arguments in each recursive call are smaller than the corresponding input regarding this order. We have limited to structural orderings. foetus tries to find such an order by collecting all recursive calls of the given function and the belonging behaviour of the function arguments. To handle mutually recursive functions a call graph is constructed and completed.

Section 2 introduces the foetus “body” (syntax and type system). Section 3 provides some examples to intuitively learn the language and see the interpreter and termination checker work. Then in section 4 we explain the “heart” of foetus: the call extractor; we also informally introduce call graph completion and finding of the lexical order: the “brain” of foetus. The latter is formally described in section 5.

2 foetus Language

2.1 foetus Syntax

A foetus program consists of terms and definitions.

P ::  empty program
| term; P  term to be evaluated
| definition; P definition for further use

When processing input, foetus evaluates the terms and stores the definitions in the environment. “Reserved words” in the foetus language are case, of, let and in. Special characterss are ( ) [ ] { } | . , ; = =>. An identifier may contain letters, digits, apostrophies and underscores. If it starts with a small letter it stands for a variable, else it denotes a constant.

Term syntax. In the following x, x_{1}, x_{2}, … denote variables, C, C_{1}, C_{2}, … constants and u, t, t_{1}, t_{2}, … foetus terms.

t :: x  variable
| [x]t  lambda
| tu  application
| C(t)  constructor
| case t of { C_{1}x_{1} ⇒ t_{1}| … |C_{n}x_{n} ⇒ t_{n} } pattern matching
| (C_{1} = t_{1}, …, C_{n} = t_{n})  tuple
| t.C  projection
| let x_{1} = t_{1}, …, x_{n} = t_{n} in t  let
| (t)  (extra parentheses)

Definitions. A definition statement has the form x_{1} = t_{1}, …, x_{n} = t_{n} (it is a let-term without a “body”). All variables x_{1}, …, x_{n} are defined simultanously, thus can refer to each other.

Example. The following foetus program defines addition on natural numbers (spanned by the two constructors O “zero” and S “successor”) and calculates 1 + 1.

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

Note that although O is a zero-argument-constructor the syntax forces us to supply a dummy variable z within the pattern definition and also empty tuple () in the definition of one.

2.2 foetus Type System

In the following x, x_{1}, x_{2}, … denote variables, C, C_{1}, C_{2}, … constants, u, t, t_{1}, t_{2}, … foetus terms, τ, σ, σ_{1}, σ_{2}, … foetus types and X, X_{1}, X_{2}, … type variables. Γ = x_{1} : σ_{1}, …, x_{n} : σ_{n} denotes the context. The judgement

Γ ⊢ t : σ

means “in context Γ term t is of type σ”.

Type formation.

τ :: σ → τ  →-type
| {C_{1} : σ_{1}| … |C_{n} : σ_{n}}  labeled sum type
| (C_{1} : σ_{1}, …, C_{n} : σ_{n})  labeled product type
| {X}τ  polymorphic type
| τσ  instantiation of polymorphic type
| Let X_{1} = σ_{1}, …, X_{n} = σ_{n} in τ recursive type

In the formation of a recursive type with Let X_{i} may only appear strict positiv in σ_{i}. We define congruence on types ≅ as the smallest congruence closed under

Let X⃗ = σ⃗ in τ ≅ τ[X_{1} := Let X⃗ = σ⃗ in X_{1}; …; X_{n} := Let X⃗ = σ⃗ in X_{n}]

(X⃗ = σ⃗ abbreviates X_{1} = σ_{1}, …, X_{n} = σ_{n}). Thus we can substitute congruent types:

{Γ ⊢ t : σ σ ≅ τ \atop Γ ⊢ t : τ}

For ploymorphic types we have rules like in System F:

Γ ⊢ t : σ X not free type variable in Γ

\overline{poly − i}
Γ ⊢ t : {X}σ
Γ ⊢ t : {X}σ
\overline{poly − e}
Γ ⊢ t : σ[X := τ]

2.3 Typing rules for foetus terms

We here only briefly introduce the typing rules. For more detailed explanation, read a book about type theorie, e.g. [NPS90].

Lambda abstraction.

Γ, x : σ ⊢ t : τ
\overline{→ −i}
Γ ⊢ [x]t : σ → τ

Application.

Γ ⊢ t : σ → τ Γ ⊢ u : σ
\overline{→ −e}
Γ ⊢ tu : σ

Constructor.

Γ ⊢ t : σ_{i}
\overline{\{\} − i}
Γ ⊢ C_{i}(t) : {C_{1} : σ_{1}| … |C_{n} : σ_{n}}

Pattern matching.

Γ ⊢ t : {C_{1} : σ_{1}| … |C_{n} : σ_{n}} Γ, x_{i} : σ_{i} ⊢ u_{i} : σ for all 1 ≤ i ≤ n

\overline{\{\} − e}
Γ ⊢ case t of {C_{1}(x_{1}) ⇒ u_{1}| … |C_{n}(x_{n}) ⇒ u_{n}} : σ

Tupels.

Γ ⊢ t_{i} : σ_{i} for all 1 ≤ i ≤ n
\overline{() − i}
Γ ⊢ (C_{1} = t_{1}, …, C_{n} = t_{n}) : (C_{1} : σ_{1}, …, C_{n} : σ_{n})

Projection.

Γ ⊢ t : (C_{1} : σ_{1}, …, C_{n} : σ_{n})
\overline{() − e}
Γ ⊢ t.C_{i} : σ_{i}

Let.

Γ, x_{1} : σ_{1}, …, x_{n} : σ_{n} ⊢ t_{i} : σ_{i} for all 1 ≤ i ≤ n Γ, x_{1} : σ_{1}, …, x_{n} : σ_{n} ⊢ u : τ

\overline{let}

Γ ⊢ let x_{1} = t_{1}; …; x_{n} = t_{n} in u : τ

In foetus type checking is not yet implemented and it is assummed that all terms entered are well typed. Of course, only for well typed terms the termination check produces valid results.

Example. The following well-known example for non-termination passes the foetus termination checker, but it is not well typed.

f = [x]x x;
a = f f;

foetus output:

f passes termination check
a passes termination check

3 Examples

3.1 Addition and multiplication

On the natural numbers

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

we define add, mult : nat → nat → 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()))))))

3.2 Subtraction

We define the predecessor function p : nat → nat and substraction on natural numbers sub : nat → nat → nat. Note sub x y calculates 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) };
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()))

3.3 Division

Division div : nat → nat → nat can be implemented as follows in functional languages (note that div x y calculates ⌊\frac{y}{x}⌋):

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 ≠ 0 → 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.

3.4 Ackermann function

The not primitive recursive Ackermann function ack : nat → nat → 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())))

3.5 List processing

We define lists over type α as

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

The well-known list processing functions map : (α → β) → listα → listβ and foldl : (α → β → β) → β → listα → β 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())))

3.6 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 ver-

sion flatten : list(listα) → listα 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α → list(listα) → listα 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()))))))

3.7 Merge sort

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

we can define le nat: nat → nat → bool and merge : (α → α → bool) → listα → listα → listα 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()))))))

3.8 Parameter permutation: list zipping

The following function zip : listα → listα → listα 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()))))

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

3.9 Tuple parameter

This example, an alternative version of add : (X : nat, Y : nat) → 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

3.10 Transfinite addition of ordinal numbers

The type of ordinal numbers is

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

and addord : ord → ord → 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

3.11 Fibonacci numbers

Iterative version fib : nat → 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

3.12 Non-terminating mutual recursion

The following three functions f, g, h : nat → nat → 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 ∀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 → g → f still does not prevent termination. But then call graph completion finds f → g → g → 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

4 Termination Checker Overall Outline

4.1 Function call extraction

The task of foetus is to check whether functions terminate or not. Because the foetus language is functional and no direct loop constructs exist, the only means to form loops is recursion. Therefore out of the program text all function calls have to be extracted to find direct or indirect recursive calls that may cause termination problems.

The heart of foetus is a analyzer that runs through the syntax tree of the given foetus program and looks for applications. Consecutive applications are gathered and formed in to a function call, e.g. in example 3.1, function add. There the two applications ((add x') y) form the call add(x′, y). As you see in this example “add” is always terminating because in each recursive call the first argument x is decreased. foetus stores with each call information about how the arguments of the call (x′, y in the example) relate to the parameters of the calling function (here: x, y), the so-called depedencies (here: x′ < x, y = y). We distinguish three kinds of relations: < (less), = (equal) and ? (unknown, this includes ‘greater’).

The abilities of foetus to recognise dependencies are yet very limited. So far only three cases are considered:

1. Constructor elimination. Be x, y variables and C a constructor, and x = C(y). It follows y < x. This is applied in case constructs (see example above).

2. Projection.

Be x, y variables, L a label, ρ a relation in {<, =} and y ρ x. Here it follows y.L ρ x, i.d. a component is considered as big as the entire tuple.

3. Application.

Be x, y variables, a a vector of terms (arguments of y), ρ a relation in {<, =} and y ρ x. It follows (ya) ρ x.

The rule 3 may have a strange looking, but it can be applied in example 3.10 (addord). In the third case x = Lim(f) we have with rule 1 f < x and with rule 3 (fz) < x, therefore addord is terminating.

4.2 Call graph

In the end the whole of extracted function calls form the call graph. It is a multigraph; each vertex represents a function and each edge from vertex f to vertex g a call of function g within the function of f. The edges are labeled with the dependency information (see above) put in a call matrix. The call matrix for the only one call add → add in example 3.1 would be

\begin{aligned}& x & y \\ x′ & < & ? \\ y & ? & = \end{aligned}

Note that each row represents one call argument and its relations to the calling function parameters.

Now if a function f calls a function g and the latter calls another function h, f indirectly calls h. The call matrix of this combined call f → h is the product of the two matrices of g → h and f → g. We get the completed call graph if we insert all combined calls (as new edges) into the original graph.

To find out whether a function f is terminating you have to collect all calls from f to itself out of the completed call graph (this includes the direct and the indirect calls). When a lexical order exists on the function parameters of f so that every recursive call decreases the order of the parameters, we have proven the termination of f. This order we call termination order.

We could call the algorithms of call graph completion and finding a lexical order the “brain” of foetus; it is described more precisely and formally in the next section.

5 Formal Description

5.1 Call Matrix

Be R = {<, =,?} set of the relations “less than”, “equal to” and “relation unknown”. In the context of “f(x, y) calls g(a, b)” a < y means “we know that (call) argument a is less than (input) parameter y”, a = y means “a is (at least) equal to y (if not less than)” and a? y means “we do not know the relation between a and y”.

With the two operations + and · defined as in table 1 R forms a commutative rig^{2} with 0-element ? and 1-element =. The operation + can be understood as “combining parallel information about a relation”, e.g. if we have a? y and a < y we have a (?+ <) y and that simplifies to a < y. The operation · however is “serial combination”, e.g. a < y and y = z can be combined into a (< · =) z, simplified: a < z. ? is neutral regarding + because it gives you no new information, whereas < is dominant because it is the strongest information. Regarding · the relation = is neutral and ? is dominant because it “destroys” all information. Check the table to see which relation overrides which.

2On the WWW I found the English term “rig” for what Germans call a “Halbring”. This is probably a play of words: Compared to a “ring” a “rig” misses an “n” as well as inverse elements regarding addition. I cite Ross Moore (see

\begin{aligned}+ & < & = & ? \\ < & < & < & < \\ = & < & = & = \\ ? & < & = & ? \end{aligned}  \begin{aligned}· & < & = & ? \\ < & < & < & ? \\ = & < & = & ? \\ ? & ? & ? & ? \end{aligned}

Table 1: Operations on R

Now we can define multiplication on matrices over R as usual:

· : R^{n×m} × R^{m×l} → R^{n×l}

((a_{ij}), (b_{ij})) ↦ (c_{ij}) = (∑_{k=1}^{m} a_{ik}b_{kj})

Why is this a reasonable definition? Assume you have three sets of variables {x_{1}, …, x_{n}}, {y_{1}, …, y_{m}} and {z_{1}, …, z_{l}}, a matrix A = (a_{ij}) ϵ R^{n×m} reflecting the relations between the x_{i}s and the y_{i}s (i.d. a_{ij} = ρ ⟺ x_{i} ρ y_{j}) and a matrix B ϵ R^{m×l} reflecting the relations between the y_{i}s and the z_{i}s. Then the matrix product C = AB reflects the relations between the x_{i}s and the z_{i}s. Because

c_{ij} = a_{i1} · b_{1j} + a_{i2} · b_{2j} + … + a_{im} · b_{mj},

we have e.g. x_{i} < z_{j} if we know it by intermediate variable y_{1} (a_{i1}·b_{1j} = ‘<′) or by intermediate variable y_{2} or … (to be continued).

a0 = 0 = 0a

http://www.mpce.mq.edu.au/∼ross/maths/Quantum/Sect1.html#206):

A rig is a set R enriched with two monoid structures, a commutative one

written additively and the other written multiplicatively, such that the fol-

lowing equations hold:

a(b + c) = ab + ac, (a + b)c = ac + ab The natural numbers ℕ provide an example of a rig.

A ring is a rig for which the additive monoid is a group. The integers ℤ

provide an example.

A rig is commutative when the multiplicative monoid is commutative.

Definition. A call matrix is a matrix over R with no more than one element different from ? per row.

CM(n, m) := {(a_{ij}) ϵ R^{n×m} : ∀i∀j∀k ≠ j(a_{ij} = ? ∨ a_{ik} = ?)}

Remark. The reason we define call matrices this way is these are the only ones foetus produces by function call extraction (see section 4.1). Because foetus recognizes only the three described cases of dependecies, a call argument can only depend of one function parameter. But multiple dependecies are imaginable, like in

f(x,y) = if (x=0) then 0 else let a=min(x,y)-1 in f(a,x)

Here the second call argument a is less than both x and y. The next proposition assures that all matrices foetus will have do deal with are call matrices.

Proposition. Matrix multiplication on matrices induces a multiplication on call matrices

· : CM(n, m) × CM(m, l) → CM(n, l)

This operation is well defined.

Proof. Be A = (a_{ij}) ϵ CM(n, m), B = (b_{ij}) ϵ CM(m, l), AB = C = (c_{ij}) ϵ R^{n×l} and k(i) the index of the element of the ith row of A that is different to ? (or 1, if no such element exists). The we have with the rules in rig R

c_{ij} = ∑_{k=1}^{m} a_{ik}b_{kj} = a_{i,k(i)}b_{k(i),j}

Now consider the ith row of C:

c_{i} = (c_{ij})_{1≤j≤l} = (a_{i,k(i)}b_{k(i),j})_{1≤j≤l}

Because at most one b_{k(i),j} is unequal to ?, at most one element of c_{i} is unequal to ?. Therefore C ϵ CM(n, l).

5.2 Call Graph

For each i ϵ ℕ we assume a set F^{(i)} = {f^{(i)}, g^{(i)}, h^{(i)}, ...} of identifiers for functions of arity i, F = ⨄_{i ϵ ℕ} F^{(i)}.

Definition. We form the set of calls as follows

C = {(f^{(n)}, g^{(m)}, A) : f^{(n)} ϵ F^{(n)}, g^{(m)} ϵ F^{(m)}, A ϵ CM(m, n)}

On calls we define the partial operation combination of calls

∘ : C × C → C
((g^{(m)}, h^{(l)}, B), (f^{(n)}, g^{(m)}, A)) ↦ (f^{(n)}, h^{(l)}, BA)

Meaning: If g calls h with call matrix B and f calls g with call matrix A, then f indirectly calls h with call matrix BA. ∘ cannot be applied to calls that have no “common function” like g, therefore it is partial. ∘ can be expanded to sets of calls

∘ : P(C) × P(C) → P(C)
(C, C′) ↦ {c ∘_{C} c′ : c ϵ C, c′ ϵ C′, (c, c′) ϵ Dom(∘_{C})}

Here we combine each call in C with each call in Ĉ to which ∘_{C} is applicable and form a set of the combined calls. ∘_{P(C)} is a total function.

Definition. A call graph is a graph (V, E) with vertices V = F and edges E ⊂_{finit} C. A call graph is complete if

E ∘ E ⊆ E

Definition. The completion of a call graph (V, E) is a call graph (V, E′) such that

(1) (V, E′) is complete,

(2) E ⊆ E′ and

(3) for all E′′ satisfying (1) and (2) we have E′ ⊆ E′′.

Proposition. The completion of a call graph (V, E) is the call graph (V, E′) such that

c ϵ E′ ⟺ ∃n > 0, c_{1}, …, c_{n} ϵ E : c_{1} ∘ … ∘ c_{n} = c

Proof.

(1) Be c ϵ E′ ∘ E′. Then there are d, e ϵ E′ with c = d ∘ e. Because (V, E′) is complete, we have

d = d_{1} ∘ … ∘ d_{n}  d_{1}, …, d_{n} ϵ E
e = e_{1} ∘ … ∘ e_{m}  e_{1}, …, e_{m} ϵ E

Thus c = d_{1} ∘ … ∘ d_{n} ∘ e_{1} ∘ … ∘ e_{m} ϵ E′.

(2) E ⊆ E′ is trivial with n = 1.

(3) Be (V, E′′) complete and E ⊆ E′′. This gives us E ∘E ⊆ E′′ from which we gain by induction

\underbrace{E ∘ … ∘ E}_{n−times} =: E^{n} ⊆ E′′ for all n.

Now be c ϵ E′. That implies c = c_{1} ∘ … ∘ c_{n} (c_{i} ϵ E) for a suitable n. Hence c ϵ E^{n} ⊆ E′′. q · e · d

Proposition. (Completion algorithm) Be (V, E) a call graph, (V, E′) its completion and (E_{n})_{n ϵ ℕ} a sequence of sets of calls defined as follows:

E_{0} = E
E_{n+1} = E_{n} ∪ (E_{n} ∘ E)

Then there is a n ϵ ℕ so that

E′ = E_{n} = E_{n+1} = E_{n+2} = …

(Obviously the E_{n} grow monotonously.)

Proof. First we show by induction that E_{n} ⊆ E′ for all n ϵ ℕ: It is obvious that E_{0} ⊆ E′. Now be E_{n} ⊆ E′ and c ϵ E_{n+1} \ E_{n}. Then c ϵ E_{n} ∘ E, therefore c = d_{1} ∘ … ∘ d_{n} ∘ e, d_{1}, …, d_{n}, e ϵ E. It follows c ϵ E′, E_{n+1} ⊆ E′.

Second: Because we have a finit set of starting edges E and therefore a finit set of reachable vertices and also a finit set of possible edges between two vertices (limited by the number of different call matrices of fixed dimensions) the E_{i}s cannot grow endlessly. Thus an n ϵ ℕ exists with E_{n} = E_{n+1}.

Third: We show that E′ ⊆ E_{n} for that particular n. Be c ϵ E′. Then there exists an m such that c = d_{1} ∘ … ∘ d_{m}, therefore c ϵ E_{m}. Now if m ≤ n then E_{m} ⊆ E_{n}, otherwise m > n and hence E_{m} = E_{n}, in both cases c ϵ E_{n}. q · e · d

5.3 Lexical Order

Definition. Be (V, E) a complete call graph and f^{(i)} a function of arity i. We call

E_{f^{(i)}} := {Δ(C) : (f^{(i)}, f^{(i)}, C) ϵ E} ⊂ R^{i}

the recursion behaviour of function f^{(i)}. (Δ takes the diagonal of square matrices).

Each row of this set represents one possible recursive call of f^{(i)} and how the orders of all parameters are altered in this call. The diagonals of the call matrices are taken because we want to know only how a parameter relates to its old value in the last call to f^{(i)}. E_{f^{(i)}} of course is a finite subset of R^{i}.

In the following we identify lexical orders on parameters with permutations π ϵ S_{n} of the arguments. Often not all of the parameters are relevant for termination; these are not listed in the lexical order and can appear in the permutation in any sequence.

In example 3.11 (fib') only the argument 0 has to be considered to prove termination, the order of argument 1 and 2 are irrelevant and therefore both permutations

π_{1} = ( \begin{matrix}0 & 1 & 2 \\ 0 & 1 & 2 \end{matrix} )

and

π_{2} = ( \begin{matrix}0 & 1 & 2 \\ 0 & 2 & 1 \end{matrix} )

are valid continuations of the lexical order “0”.

Note: In the following we abbreviate the notation of permutations to π_{1} = [012] and π_{2} = [021].

Definition. (1) Be B the recursion behaviour of function f^{(n)}. We call the permutation π ϵ S_{n} a termination order for f^{(n)} if

∀r ϵ B∃1 ≤ k ≤ n : r_{π(k)} = ‘<′ ∧ (∀1 ≤ i ≤ k : r_{π(i)} = ‘=′)

This definition is a very wide one. In most cases you will look for more special termination orders:

Definition. (2, inductive) Be B the recursion behaviour of a given function. We call the permutation π ϵ S_{n} a termination order on B if |B| = 0 or

∃r ϵ B : r_{π(0)} =<
∧ ∄r ϵ B : r_{π(0)} = ?
∧ π′_{0} ϵ S_{n−1} termination order on B′ := {r′_{π(0)} : r_{π(0)} ≠<} ⊂ R^{n−1}

whereas π′_{i} = [k_{0} … k_{i−1}k_{i+1} … k_{n−1}] ϵ S_{n−1} given π = [k_{0} … k_{n−1}] ϵ S_{n} and r′_{i} = (k_{0}, …, k_{i−1}, k_{i+1}, …, k_{n−1}) ϵ R^{n−1} given r = (k_{0}, …, k_{n−1}) ϵ R^{n}.

The algorithm implemented in foetus searches termination orders like in definition (2); it is a one-to-one transfer of this definition. Every termination order matching definition (2) also matches definition (1) and it can easily be shown that if there is a termination order of type (1) there also exists on of type (2).

Example 5.1 Be E = {(=, <,?), (=, =, <), (=, <, =)} the given recursion behaviour. Then π_{1} = [012] is a type (1) termination order on E and π_{2} = [120] is of both types.

6 Implementation

foetus has been implemented in SML 97. We have used the new Standard ML Basis Library to ensure a safe and possibly optimized handling of standard data structures like lists etc. The parser for the foetus terms has been created with ML-Lex and ML-Yacc. The ML implementation currently used is Standard ML of New Jersey, Version 109.32.

foetus.lex  foetus language token specification for ml-lex
foetus.grm  foetus language grammar for ml-yacc
aux.sml  auxiliary functions
closure.sml  terms and environment
foetus.sml  values, evaluation function hnf, printing
matrix.sml  polymorphic matrices with necessary operations
simpledeps.sml simple implementation of dependecies
analyse.sml  static analysis of foetus code
check.sml  termination check via call graph
top.sml  top level environment
load.sml  loader and foetus parser

Table 2: foetus source files

7 Conclusion

We have seen that foetus and its “brain”, the call graph completion and finding a lexical order on the function arguments, contributes to automated termination proofs. Of course, in its current state it is no more than a toy to gather experience on his subject. Some improvements have to be done: foetus should be able to recognize more kinds of dependencies (see section 4.1).

• Let assignments. The use of let-constructs to save values within functions is discouraged because foetus stores no relations concerning them; it performs no symbolic evaluation during analyzation. For example:

     case list of
             {Cons pair => let
                    hd = pair.HD,
                    tl = pair.TL in ...

foetus does not know that hd < list and that tl < list. At least such simple assignments (for code shortening) should be handled.

• Tuple handling. foetus should trace the dependencies not only of the whole tuples but also of their components. At the moment you cannot define functions with one tuple as parameter instead of separate parameters and still expect a termination proof (see example 3.9).

• Function results. The reason that foetus cannot prove termination of div (see example 3.3) is that it does not know x ≠ 0 → (y − x = 0 ∨ y − x < y). But this could be shown for the sub function by induction and result in a dependency foetus could use [BG96].

Furthermore the call graph completion algorithm could be adopted to prove termination of parameter permuting functions like zip (see example 3.8).

If foetus has “grown older” in the described manner it could be “born into” one of the “adult” program verfication systems or theorem provers like ALF, Isabelle, LEGO or MuTTI ;-).

References

[BG96] Jürgen Brauburger and Jürgen Giesl. Termination analysis for partial functions. In Proceedings of the Third International Static Analysis Symposium (SAS’96), Aachen, Germany, Lecture Notes in Computer Science 1145, Springer-Verlag, 1996.

[Gie97] Jürgen Giesl. Termination of nested and mutually recursive algorithms. Journal of Automated Reasoning 19: 1–29, 1997.

[NPS90] Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990.

[Pau91] Lawrence C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.

[Sli96] Konrad Slind. Function definition in higher order logic. In Proceedings of TPHOLs 96 (LNCS 1125), 1996.

[Sli97a] Konrad Slind. Derivation and use of induction schemes in higherorder logic. In Proceedings of TPHOLs97 (LNCS 1275), 1997.

[TTu97b] Alastair Telford and David Turner. Ensuring Streams Flow. In Michael Johnson, editor, Algebraic Methodology and Software Technology, 6th International Conference, AMAST ’97, Sydney Australia, December 1997, volume 1349 of Lecture Notes in Computer Science, pages 509–523. AMAST, Springer-Verlag, December 1997.