Termination Checker Overall Outline  

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, $\rho$ a relation in {` < ',` = '} and y $\rho$ x . Here it follows y.L $\rho$ 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 ), $\rho$ a relation in {` < ',` = '} and y $\rho$ x . It follows (ya) $\rho$ 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.

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 $\rightarrow$ add in example 3.1 would be

x y

x' ` < ' `?'

y `?' ` = '

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 $\rightarrow$ h is the product of the two matrices of g $\rightarrow$ h and f $\rightarrow$ 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.