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:
x | y | |
x' | ` < ' | `?' |
y | `?' | ` = ' |
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.