TFL: An Environment for Terminating Functional Programs

TFL: An Environment for Terminating Functional Programs

TFL is an environment for defining and reasoning about terminating programs written in a purely functional manner. It has the following significant features: So much for the executive summary; now for a little more detail. (For a lot more detail, you might want to read the papers Function Definition in Higher-Order Logic and Derivation and Use of Induction Schemes in Higher-Order Logic.)

A small (and out-of-date) battery of examples has been developed in the TFL/HOL instantiation.


Formal Basis

The formal basis builds on the abstract notion of wellfoundedness: a relation is wellfounded iff it allows no infinite decreasing chains. From this definition, a general induction theorem can be proved, and also a recursion theorem that justifies the definition of terminating recursive functions. Some useful theorems for constructing new wellfounded relations from old are supplied. This allows termination to be expressed at a high level.

Mechanization of Recursive Definitions

Instead of attempting to analyze the syntactic structure of a proposed recursive function to see whether it terminates or not (and is hence a consistent addition to the logic) our machinery uses inference steps to instantiate the wellfounded recursion theorem. This approach is completely safe, in contrast to the syntactic method. The following are some of the other interesting aspects of our approach to definitions:

Termination

Proving termination of a recursively defined function divides into two tasks: (1) finding a wellfounded relation R; (2) showing that the recursive calls decrease under R. Our system supports the first task by providing high-level constructs to express wellfounded relations with. Specifically we provide transitive closure, lexicographic combination, subset, and inverse image as means of building new wellfounded relations from old. For the second task, i.e., actually proving termination, we observe that, although termination is an undecidable problem, in most cases a measure function is used to show termination. In such cases, we have used a decision procedure for the unquantified fragment of Presburger arithmetic and found it to be quite effective.

Induction

For each recursive function definition, the system derives a principle of recursion induction, by instantiating and manipulating the wellfounded induction theorem. In recursion induction, the property to be proved is assumed to hold for arguments to recursive calls, and the task is to show that the property holds for the original call. If that can be shown, then the property holds for every invocation of the function. Our induction theorems have the following interesting aspects:

Summary

This concludes our discussion of TFL. The system has been instantiated to 2 systems, HOL and Isabelle. The HOL version has been incorporated into the latest hol release. Likewise, in the latest Isabelle release the functionality of TFL is accessible from Isabelle theory files (due to the efforts of Larry Paulson).

Konrad Slind, kxs@cl.cam.ac.uk