How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?

Question

Suppose you have a version of the STLC with one base type, similar to:

 data Tree = Branch Tree Tree | Leaf

Now, suppose you want to add recursion to that language, while still guaranteeing termination. Someone suggested a "Recur" primitive, which can only be applied at sub-expressions of pattern matches, making the following legal:

id (Tree a b) = Tree (id a) (id b)
id Leaf = Leaf

This is obviously terminating, so that sounds like a good idea. Now, mind that function:

foo (Tree (Tree a b) c) = foo (Tree a c)
foo (Tree a b) = Tree (foo a) (foo b)
foo Leaf = Leaf 

Now this function is obviously terminating, but it includes a recursion that is not applied directly to a sub expression of a pattern match, namely, foo (Tree a c), so you can't express it on the suggested system. My question is: is there a more general way to introduce recursion that will still guarantee termination without making some valid cases illegal?

Answer 1

Which of the following are you asking: are there ways of enriching the simply-typed $\lambda$-calculus with mechanisms (presumably by restricting the available forms of recursion) such that

1. exactly the terminating programs are typable?

2. more terminating programs are encodable than with the simple restriction you are describing in your question?

The answer to (1), as pointed out by Toxaris, is: if you want type-checking to be decidable, then no. This follows directly from the uncomputability of the halting problem. The answer to (2) is positive, and Dave Clarke's answer gives an example. Indeed there are countless ways of doing so, some ad-hoc: e.g. if you have a particular (terminating) program $M$ of type $\alpha$ you want to add to the simply-typed $\lambda$-calculus, you simply add a rule $\Gamma \vdash M : \alpha$ to your typing system. For a more interesting and principled way you could look at Barendregt's $\lambda$-cube, which presents three orthogonal axes of extending the simply-typed $\lambda$-calculus, all of which make the simply-typed $\lambda$-calculus strictly more expressive without losing normalisation. Relatedly, you can look at induction principles, which are related closely to recursion. Note that this is an active area of research because the more expressive you make your typing system, the harder it becomes to prove that the calculus indeed only types normalising programs.

Note that the problem is usually not to find a fragment of total functions that we can use to program our terminating programs in. The total fragments of lambda-calculus given by more expressive parts of the $\lambda$-cube (e.g. $F_{\omega}$ or the calculus of constructions) are very expressive. The problem is usually that it is often inconvenient to encode a terminating program in such a fragment. R. Harper gives the example of the $gcd$ function computing the greatest common divisor: $$ \begin{align*} \textit{gcd}(m,0) & = m \\ \textit{gcd}(0,n) & = n \\ \textit{gcd}(m,n) & = \textit{gcd}(m-n,n) \quad \text{if}\ m>n \\ \textit{gcd}(m,n) & = \textit{gcd}(m,n-m) \quad \text{if}\ m<n \end{align*} $$

It is easy to see that this function terminates, but expressing it using simple recursion schemes is no fun. Most programs we care about in daily programming life are terminating for simple reasons and can typically be encoded using relatively simple recursion schemes (e.g. primitive recursion). That's why it was a major insight of Ackermann's and Sudan's that primitive recursion is not enough. For this reason powerful recursion schemes (including the unrestricted recursion of most programming languages) are typically a convenient device to make programming simpler, rather than necessary for expressivity. Note that in the presence of higher-order functions, primitive recursion is quite powerful, and enables us to encode e.g. the Ackermann function:

$$ \begin{array}{lcl} \textit{Ackermann} \ 0 & = & \lambda x. x+1 \\ \textit{Ackermann} \ ( m+1 ) & = & \textit{Iter}\ ( \textit{Ackermann}\ m ) \\ \textit{Iter}\ f\ 0 & = & f\ 1 \\ \textit{Iter}\ f\ ( n+1 ) & = & f\ ( \textit{Iter}\ f\ n ) \end{array} $$

BTW, the simply-typed $\lambda$-calculus with primitive recursion is also known as Gödel's System T and its expressivity has been studied in great detail and is well understood: we can define exactly the recursive function whose totality can be proved in first-order logic, starting from the usual axioms for the elementary data types, eg the Peano axioms for natural numbers.

In this context, you may find the paper Total Functional Programming by DA Turner interesting.

Non-typing work on termination. There's also a lot of ongoing work, both theoretical and implementation oriented, on termination analysis that's not using (compositional) typing systems, but static analysis techniques. An example is Microsoft's T2 termination prover.

Answer 2

Is there a more general way to introduce recursion that will still guarantee termination without making some valid cases illegal?

No. It is undecidable whether a program with general recursion terminates or not. Hence you cannot define a restricted form of recursion that selects precisely the terminating programs.

Answer 3

The programming language Charity offers a solution to your problem (though it may be polymorphic).

They key is to introduce folds into the language as combinators rather than using general fixed point recursion. Folds are very much like the recur primitive that you mention. Other such combinators are possible. Such combinators are known by strange names such as catamorphisms, anamorphisms, hylomorphisms, and paramorphisms (also known as Bananas, Lenses, Envelopes and Barbed Wire. Other work on recursion schemes expand the class of functions that can be expressed.

Now folds are required to pull a data structure apart – building one up you need an unfold. Much of the work cited above, or cited in the work above, or building upon the work above, also deals with combinators or recursion schemes like unfold. (Caveat: I'm not sure that all of these schemes are strongly normalising – the ones in Charity supposedly are.)

Returning to your example. You are essentially stating that this example cannot be encoded using a folds. I suspect that it can be, because, for instance, a filter can be encoded as a fold, and your example is a bit similar to a filter on trees.

Answer 4

To add tho the already good answers, there is a huge field of research called Termination Analysis which deals with methods to analyze the termination of various computation formalisms. Of particular interest are Term Rewrite Systems which seem to capture quite well the termination problems of functional programs.

I can't even begin to outline the various lines of work involved in this vast field. My personal work has been related to size types (see e.g. Barthe et al.), which integrates quite well with the STLC.