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

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.