<p>The programming language <a href="http://pll.cpsc.ucalgary.ca/charity1/www/home.html" rel="nofollow">Charity</a> offers a solution to your problem (though it may be polymorphic).</p>

<p>They key is to introduce <em>folds</em> 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 <a href="http://eprints.eemcs.utwente.nl/7281/01/db-utwente-40501F46.pdf" rel="nofollow">Bananas, Lenses, Envelopes and Barbed Wire</a>. 
Other work on <a href="http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/urs.pdf" rel="nofollow">recursion schemes</a> expand the class of functions that can be expressed.</p>

<p>Now folds are required to pull a data structure apart – building one up you need an <em>unfold</em>. 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. (<em>Caveat</em>: I'm not sure that all of these schemes are strongly normalising – the ones in Charity supposedly are.)</p>

<p>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 <em>filter</em> can be encoded as a fold, and your example is a bit similar to a filter on trees.</p>

CC BY-SA 3.0
2014-05-04T05:35:05.357Z
2014-05-04T05:35:05.357Z
Dave Clarke
<blockquote>
  <p>Is there a more general way to introduce recursion that will still guarantee termination without making some valid cases illegal?</p>
</blockquote>

<p>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.</p>

CC BY-SA 3.0
2014-05-03T22:43:42.263Z
Then why that idea works (only being able to call a recursive function on sub-exprs of pattern matched values)?
MaiaVictor
CC BY-SA 3.0
2014-05-04T00:34:33.633Z
@Viclib: That idea works by making some valid cases illegal.
Toxaris
CC BY-SA 3.0
2014-05-04T01:05:34.543Z
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.
MaiaVictor
CC BY-SA 3.0
2014-05-03T21:00:34.390Z
2014-05-03T21:00:34.390Z
Toxaris
<p>To add tho the already good answers, there is a huge field of research called <a href="http://en.wikipedia.org/wiki/Termination_analysis" rel="nofollow">Termination Analysis</a> which deals with methods to analyze the termination of various computation formalisms. Of particular interest are <a href="http://en.wikipedia.org/wiki/Rewriting" rel="nofollow">Term Rewrite Systems</a> which seem to capture quite well the termination problems of functional programs.</p>

<p>I can't even begin to outline the various lines of work involved in this vast field. My personal work has been related to <em>size types</em> (see e.g. <a href="http://perso.ens-lyon.fr/colin.riba/papers/tutorial-tbt.pdf" rel="nofollow">Barthe <em>et al.</em></a>), which integrates quite well with the STLC.</p>

CC BY-SA 3.0
2014-05-05T07:41:18.160Z
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?
MaiaVictor
CC BY-SA 3.0
2014-05-05T09:25:59.510Z
@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
CC BY-SA 3.0
2014-05-05T22:43:26.843Z
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
CC BY-SA 3.0
2014-05-04T16:34:58.797Z
2014-05-04T16:34:58.797Z
cody
<p>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</p>

<ol>
<li><p>exactly the terminating programs are typable? </p></li>
<li><p>more terminating programs are encodable than with the simple
    restriction you are describing in your question?</p></li>
</ol>

<p>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 <a href="https://en.wikipedia.org/wiki/Lambda_cube" rel="nofollow">Barendregt's $\lambda$-cube</a>,
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.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Calculus_of_constructions" rel="nofollow">calculus of constructions</a>)
are very expressive. The problem is usually that it is
often <strong>inconvenient</strong> to encode a terminating program in such a
fragment. <a href="http://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-still-theorems/" rel="nofollow">R. Harper gives the example</a> of the $gcd$ function computing
the greatest common divisor:
$$
\begin{align*}
\textit{gcd}(m,0) &amp; = m \\
\textit{gcd}(0,n) &amp; = n \\
\textit{gcd}(m,n) &amp; = \textit{gcd}(m-n,n) \quad \text{if}\ m&gt;n \\
\textit{gcd}(m,n) &amp; = \textit{gcd}(m,n-m) \quad \text{if}\ m&lt;n
\end{align*}
$$</p>

<p>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 <a href="https://en.wikipedia.org/wiki/Ackermann_function" rel="nofollow">major insight of Ackermann's and Sudan's</a> that primitive
recursion is not enough.
For this reason  powerful recursion schemes
(including the unrestricted recursion of most programming languages)
are typically a <strong>convenient</strong> 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:</p>

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

<p>BTW, the simply-typed $\lambda$-calculus with primitive recursion is also known as G&ouml;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. </p>

<p>In this context, you may find the paper <a href="http://www.eis.mdx.ac.uk/staffpages/dat/sblp1.pdf" rel="nofollow">Total Functional Programming</a> by DA Turner interesting.</p>

<p><strong>Non-typing work on termination.</strong> 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 <a href="https://research.microsoft.com/en-us/projects/t2/" rel="nofollow">T2 termination prover</a>.</p>

CC BY-SA 3.0
2014-05-06T02:13:53.153Z
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.
MaiaVictor
CC BY-SA 3.0
2014-05-06T02:16:17.940Z
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.
MaiaVictor
CC BY-SA 3.0
2014-05-06T02:37:22.910Z
@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
CC BY-SA 3.0
2014-05-06T02:40:59.353Z
Have you looked at [ATS](http://www.ats-lang.org/), [Ur/Web](http://www.impredicative.com/ur/), [Idris](http://www.idris-lang.org/), [Elm](http://elm-lang.org/), [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) and [$\Omega$mega](https://en.wikipedia.org/wiki/%CE%A9mega).
Martin Berger
CC BY-SA 3.0
2014-05-06T07:05:18.730Z
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!
MaiaVictor
CC BY-SA 3.0
2014-05-04T06:39:10.010Z
2014-05-05T11:12:24.710Z
2014-05-05T11:12:24.710Z
Martin Berger
<p>Suppose you have a version of the STLC with one base type, similar to:</p>

<pre><code> data Tree = Branch Tree Tree | Leaf
</code></pre>

<p>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:</p>

<pre><code>id (Tree a b) = Tree (id a) (id b)
id Leaf = Leaf
</code></pre>

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

<pre><code>foo (Tree (Tree a b) c) = foo (Tree a c)
foo (Tree a b) = Tree (foo a) (foo b)
foo Leaf = Leaf 
</code></pre>

<p>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, <code>foo (Tree a c)</code>, 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?</p>

CC BY-SA 3.0
2014-05-04T10:04:59.923Z
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
CC BY-SA 3.0
2014-05-04T11:26:35.450Z
@AndrejBauer The code seems Haskell-like, in which case: yes, patterns are checked in the order of declaration.
Bakuriu
<pl.programming-languages><computability>
How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?
MaiaVictor
# How to introduce recursion to Simply Typed Lambda Calculus while at the same time keeping strong normalisation?

(Asked by: username_0 on 2014-05-03)

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?

**Tags:** pl.programming-languages, computability

> **Comments:**
> **username_1**: How am I supposed to read the definition of `foo`? The first and second case overlap. Is the first one supposed to take precedence?  
> **username_2**: @AndrejBauer The code seems Haskell-like, in which case: yes, patterns are checked in the order of declaration.  

---

## 4 answers

### Answer by username_6 on 2014-05-04. Score: 8 | Accepted answer

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 username_4, 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 username_3'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](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/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](http://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-still-theorems/) 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

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](https://en.wikipedia.org/wiki/Ackermann_function) 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](http://www.eis.mdx.ac.uk/staffpages/dat/sblp1.pdf) 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](https://research.microsoft.com/en-us/projects/t2/).

> **Comments:**
> **username_0**: 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.  
> **username_0**: 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.  
> **username_6**: @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.  
> **username_6**: Have you looked at [ATS](http://www.ats-lang.org/), [Ur/Web](http://www.impredicative.com/ur/), [Idris](http://www.idris-lang.org/), [Elm](http://elm-lang.org/), [Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) and [$\Omega$mega](https://en.wikipedia.org/wiki/%CE%A9mega).  
> **username_0**: 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!  

---

### Answer by username_3 on 2014-05-04. Score: 3

The programming language [Charity](http://pll.cpsc.ucalgary.ca/charity1/www/home.html) 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](http://eprints.eemcs.utwente.nl/7281/01/db-utwente-40501F46.pdf).
Other work on [recursion schemes](http://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/urs.pdf) 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 by username_4 on 2014-05-03. Score: 3

> 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.

> **Comments:**
> **username_0**: Then why that idea works (only being able to call a recursive function on sub-exprs of pattern matched values)?  
> **username_4**: @Viclib: That idea works by making some valid cases illegal.  
> **username_0**: 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.  

---

### Answer by username_5 on 2014-05-04. Score: 2

To add tho the already good answers, there is a huge field of research called [Termination Analysis](http://en.wikipedia.org/wiki/Termination_analysis) which deals with methods to analyze the termination of various computation formalisms. Of particular interest are [Term Rewrite Systems](http://en.wikipedia.org/wiki/Rewriting) 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.*](http://perso.ens-lyon.fr/colin.riba/papers/tutorial-tbt.pdf)), which integrates quite well with the STLC.

> **Comments:**
> **username_0**: 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?  
> **username_6**: @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.  
> **username_5**: 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).  

---

