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)

1 Answer 1


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

  1. take a CPS converted version the program, and
  2. 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

Not the answer you're looking for? Browse other questions tagged or ask your own question.