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

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?

-
How am I supposed to read the definition of foo? The first and second case overlap. Is the first one supposed to take precedence? – Andrej Bauer May 4 '14 at 10:04
@AndrejBauer The code seems Haskell-like, in which case: yes, patterns are checked in the order of declaration. – Bakuriu May 4 '14 at 11:26

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.

-
Martin, let me just ask a question. You probably are aware of what I am interested in, but to be specific, I am programming an online code editor which one of the main features is a huge, integrated encyclopedia of functions. Now I'm looking for the best language to fit it. Obviously the language must be, at least, referentially transparent (it would make no sense to have a catalog of unpure functions!). This eliminates almost all practical languages other than Haskell, but Haskell is kinda heavyweight, in the sense it can't be ported to the web and be fast enough. – Viclib May 6 '14 at 2:13
Also, more than that, I'd like people to do things like 3D graphics on that language without having to invoke external libraries such as OpenGL. So, in a way, the compiler for that language must at least be smart enough to figure out when you are mapping a function to a 1024x1024 and represent them as GPU arrays instead. So, now you probably know where I'm coming at, please, could you answer 2 questions: 1. where I can find relevant papers and resources that will interest me? 2. what would you suggest me to do, given your experience? Thank you very much, hope I'm not abusing your goodwill. – Viclib May 6 '14 at 2:16
@Viclib I'm not sure the language you are looking for exists, at least if we are talking about non-toy languages. While developing a toy-language is easy, producing an industrial strength language with a viable number of users is hard. In particular, languages that do clever things with GPUs are rare. One option regarding termination could be to take a language that offers hooks into the compiler (e.g. Scala or Java) and instrument it so that only restricted forms of recursions can be compiled, thus guaranteeing termination. – Martin Berger May 6 '14 at 2:37
Have you looked at ATS, Ur/Web, Idris, Elm, Agda and $\Omega$mega. – Martin Berger May 6 '14 at 2:40
Yep... all of them. And I think all of those are actually really promising. Won't do what I need, though. I guess you are right, languages that do clever things with the GPU are rare. Dependently typed languages are rare. Well, even pure functional languages are rare enough. Add to that being able to compile to a lot of platforms and I guess we get an empty intersection. Sadly, seems like I'll have to do that myself, hard or not. Thanks for the insights! – Viclib May 6 '14 at 7:05

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.

-
Then why that idea works (only being able to call a recursive function on sub-exprs of pattern matched values)? – Viclib May 3 '14 at 22:43
@Viclib: That idea works by making some valid cases illegal. – Toxaris May 4 '14 at 0:34
OK, I think what I am asking is wether there is how to improve that idea in the sense of making less valid cases illegal. – Viclib May 4 '14 at 1:05

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.

-

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.

-
Thanks for the input. STLC apart, I am interested in any system which is powerful enough to encode practical routine algorithms (such as image processing, sorting etc) while still weak enough that computation always terminate and it is trivial to prove function equality. Is there any such system you can recommend? – Viclib May 5 '14 at 7:41
@Viclib The problem is usually not to find a fragment of total functions that we can use to program our terminating programs in. The most fragments in the $\lambda$-cube are very expressive. The problem is one of convenience. I have augmented my answer to this effect. See also Harper's blog post that I quoted. – Martin Berger May 5 '14 at 9:25
Note that function equality is undecidable even for primitive recursive functions. What you get in terminating systems is much weaker (just equality of normal forms). – cody May 5 '14 at 22:43