<p>From the point of view of lambda-calculus "tail call optimization" means</p>

<ol>
<li>take a CPS converted version the program, and</li>
<li>eta-reduce continuations of the form $\lambda x. k\;x$ to $k$</li>
</ol>

<p>Since eta-conversion is part of the equational theory of the lambda-calculus, this has no effect on the semantics of the program. </p>

<p>Furthermore, in the lambda calculus, all of the recursion schemes you list above are instances of the iteration scheme at higher type. (The appropriate calculus is Goedel's System T.) I'll illustrate with some Ocaml code.</p>

<p>First, we can start with a datatype for natural numbers, and define primitive iteration for it:</p>

<pre><code>type nat = Z | S of nat

let rec iter m z s =    (* iter : nat -&gt; 'a -&gt; ('a -&gt; 'a) -&gt; 'a *)
  match m with 
  | Z -&gt; z
  | S n -&gt; s (iter n z s)
</code></pre>

<p>This is already sufficient to define addition, multiplication, and exponentiation:</p>

<pre><code>let suc n = S n 

let add m n = iter m n suc 
let mul m n = iter m Z (add n)
let exp m n = iter n (suc Z) (mul m)
</code></pre>

<p>Note that <code>iter</code> is a polymorphic definition, and the type parameter <code>'a</code> can be instantiated to any type, including function types. This means that iteration with parameters is definable, which we can (for example) use to define the predecessor:</p>

<pre><code>let pred n =
  iter n (fun u -&gt; Z) (fun g h -&gt; h (g suc)) (fun u -&gt; u)
</code></pre>

<p>Observe that the type of <code>iter n (fun u -&gt; Z) (fun g h -&gt; h (g suc))</code> is <code>(nat -&gt; nat) -&gt; nat</code>. Once we have predecessor, defining primitive recursion is easy:</p>

<pre><code>let prim_rec n z s =
  iter n (fun k -&gt; z) (fun r n -&gt; s n (r (pred n))) n
</code></pre>

<p>Indeed, even Ackermann's function is definable:</p>

<pre><code>let shift g n = iter (suc n) (suc Z) g
let ack n = iter n suc shift
</code></pre>

CC BY-SA 3.0
2016-06-22T12:06:24.603Z
2016-06-22T12:06:24.603Z
Neel Krishnaswami
<p>I'm rather confused by the recursion theory.</p>

<p>From the <a href="http://plato.stanford.edu/entries/recursive-functions/" rel="nofollow">link</a>, the recursion theory was formed by Dedekind, Gödel and some other famous mathematicians. There are the following types of recursion. But where is tail recursion? can this concept parallel to these concepts? what else concept goes parallel to tail recursion?</p>

<pre><code>1.1 The Initial Functions
1.2 Iteration
1.3 Primitive recursion
1.4 Primitive recursion with parameters
1.5 Course-of-value recursion
1.6 Double recursion
1.7 Minimization (least search)
</code></pre>

CC BY-SA 3.0
2016-06-22T07:36:37.603Z
https://en.wikipedia.org/wiki/Tail_call
Kaveh
CC BY-SA 3.0
2016-06-22T20:45:28.517Z
Also on cs.se: http://cs.stackexchange.com/questions/59887/what-is-the-relationship-between-tail-recursion-with-other-recursions.
Yuval Filmus
<cc.complexity-theory><computability><recursion><recursive>
What is the relationship between tail recursion with other recursions?
user3329081
# What is the relationship between tail recursion with other recursions?

(Asked by: username_0 on 2016-06-22)

I'm rather confused by the recursion theory.
From the link, the recursion theory was formed by Dedekind, Gödel and some other famous mathematicians. There are the following types of recursion. But where is tail recursion? can this concept parallel to these concepts? what else concept goes parallel to tail recursion?
1.1 The Initial Functions
1.2 Iteration
1.3 Primitive recursion
1.4 Primitive recursion with parameters
1.5 Course-of-value recursion
1.6 Double recursion
1.7 Minimization (least search)

**Tags:** cc.complexity-theory, computability, recursion, recursive

> **Comments:**
> **username_1**: https://en.wikipedia.org/wiki/Tail_call  
> **username_2**: Also on cs.se: http://cs.stackexchange.com/questions/59887/what-is-the-relationship-between-tail-recursion-with-other-recursions.  

---

## 1 answers

### Answer by username_3 on 2016-06-22. Score: 4

From the point of view of lambda-calculus "tail call optimization" means

take a CPS converted version the program, and
eta-reduce continuations of the form $\lambda x. k\;x$ to $k$

Since eta-conversion is part of the equational theory of the lambda-calculus, this has no effect on the semantics of the program. 
Furthermore, in the lambda calculus, all of the recursion schemes you list above are instances of the iteration scheme at higher type. (The appropriate calculus is Goedel's System T.) I'll illustrate with some Ocaml code.
First, we can start with a datatype for natural numbers, and define primitive iteration for it:
type nat = Z | S of nat

let rec iter m z s =    (* iter : nat -> 'a -> ('a -> 'a) -> 'a *)
  match m with 
  | Z -> z
  | S n -> s (iter n z s)

This is already sufficient to define addition, multiplication, and exponentiation:
let suc n = S n 

let add m n = iter m n suc 
let mul m n = iter m Z (add n)
let exp m n = iter n (suc Z) (mul m)

Note that iter is a polymorphic definition, and the type parameter 'a can be instantiated to any type, including function types. This means that iteration with parameters is definable, which we can (for example) use to define the predecessor:
let pred n =
  iter n (fun u -> Z) (fun g h -> h (g suc)) (fun u -> u)

Observe that the type of iter n (fun u -> Z) (fun g h -> h (g suc)) is (nat -> nat) -> nat. Once we have predecessor, defining primitive recursion is easy:
let prim_rec n z s =
  iter n (fun k -> z) (fun r n -> s n (r (pred n))) n

Indeed, even Ackermann's function is definable:
let shift g n = iter (suc n) (suc Z) g
let ack n = iter n suc shift


---

