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:

Higher order. Programs are represented by the native functions of higher order logic. This light representation means that the proof tools already provided in the logic can be immediately applied to programs. Since functions in the logic can be higher order and (ML-style) polymorphic, the class of programs that can be represented can also be higher order and polymorphic. Therefore a wide class of programs from popular functional languages like ML and Haskell can be quickly formalized and reasoned about.
Total. All programs in TFL terminate; therefore, a program defined in TFL will have the same behaviour regardless of which compiler or reduction strategy it is executed under. Thus TFL captures a wide class of programs that are inter-language portable.
Fully formal. Logically, the environment is a conservative extension. Therefore, using it will not suddenly allow false theorems to be derived. In particular, definitions of recursive programs can be made without any worries about introducing inconsistency. This sort of security is very important, especially as proof developments grow ever larger.
Portable. As a result of its fully formal foundation, TFL is itself portable. It can be instantiated to very different proof systems, as has already been done in instantiating it to HOL and Isabelle.
Extensible. As the user builds a formalization, TFL keeps pace by extending its internal datastructures. The system is also parameterized by simplifiers and termination solvers so that better tools can be "plugged-in" when they become available.

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:

Automatic extraction of termination conditions. We make novel use of congruence-based contextual rewriting to automatically capture termination conditions and make them available to termination solvers, and if the solvers fail, to the user.
Pattern matching and variable binding operators. Our syntax effectively deals with the pattern-matching style of definition popular in functional programming languages. Another feature of functional languages is let bindings. These are used to share computation, and therefore are of great importance in writing efficient algorithms. Our congruence-based rewriter handles such variable-binding constructs. For example, the following classical definition of quicksort is accepted by our system
```
       fun qsort(R:order,[]) = []
         | qsort(R, x::rst) = 
              qsort,(R, filter(not o R x) rst)
              ++ [x] ++
              qsort(R, filter(R x) rst)

    
```
as is the following more efficient version, which uses a single pass to partition the input to recursive calls:
```
    (* Partition a list into two sublists *)
    fun part(P,[], l1,l2) = (l1,l2)
      | part(P, h::rst, l1,l2) = 
           if P h then part(P,rst, h::l1, l2)
                  else part(P,rst, l1, h::l2);

    (* A faster quicksort *)
    fun fqsort(R:order,[]) = []
      | fqsort(R, x::rst) = 
          let (l1,l2) = part((\y. R y x), rst,[],[])
          in
          fqsort(R,l1) ++ [x] ++ fqsort(R,l2)
    
```
Syntax note: "\" is lambda abstraction; "++" is list concatenation; and "::" is the "cons" operation for lists.
Deferral of termination arguments. In other systems, termination of a function needs to be proved before it can be used. This can be a bother, especially since one would sometimes like to first define a collection of functions and prove their termination separately. Our system provides a neat way of doing this. The result is that defining functions is very easy in TFL, and the potentially difficult work of finding a wellfounded relation under which a function terminates can be postponed (although never completely avoided!).
Nested recursion. Nested recursive programs are notoriously difficult to deal with. Some authors have asserted that partial and total correctness need to be proved simultaneously for such programs. We have shown that this is not exactly true: the reason why a program terminates is (largely) independent of what the program computes.

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:

Independent of termination relation. The construction of the induction theorem is driven by the structure of the recursive function, and the theorem is not affected by which relation is given to show termination. In other words, it doesn't matter why the function terminates, just that it does. In fact, if the function cannot be proved to terminate, the termination condition persists on the assumptions of the induction theorem, thus preserving consistency.

Use of patterns. Also, the use of patterns in the recursive definition allows the use of patterns to express the induction theorem. For instance, if we define Euclid's algorithm (on the natural numbers) with the following in TFL

    fun gcd (0,y) = y
      | gcd (Suc x, 0) = Suc x
      | gcd (Suc x, Suc y) = 
           if (y <= x) then gcd(x - y, Suc y) 
                       else gcd(Suc x, y - x);

we get the following induction principle for reasoning about gcd:

    |- !P. (!y. P(0,y)) /\
           (!x. P(Suc x,0)) /\
           (!x y.
             (~(y <= x) ==> P(Suc x, y - x)) /\ 
               (y <= x  ==> P(x - y, Suc y)) ==> P (Suc x,Suc y))
           ==>
           !v v1. P(v,v1)

Syntax note: "!" is universal quantification; "/\" is conjunction; "~" is negation, and "==>" is implication.

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