Recursion in the calculus of construction

Question

How to define a recursive function in the (pure) calculus of constructions? I do not see any fixpoint combinator there.

Answer 1

People in the CS stack exchange might be able to provide some more insight, but here is an attempt.

Inductive data types are defined in the calculus of constructions with a Church encoding: the data type is the type of its fold function. The most basic example are the natural numbers, which are defined as follows, using a Coq-like notation:

nat := forall (T : Type), T -> (T -> T) -> T

This encoding yields two things: (1) terms zero : nat and succ : nat -> nat for constructing natural numbers, and (2) an operator nat_rec for writing recursive functions.

zero : nat
zero T x f := x

succ : nat -> nat
succ n T x f := f (n T x f)

nat_rec : forall T, T -> (T -> T) -> nat -> T
nat_rec T x f n := n T x f

If we pose F := nat_rec T x f for terms x : T and f : T -> T, we see that the following equations are valid:

F zero = x
F (succ n) = f (F n)

Thus, nat_rec allows us to define recursive functions by specifying a return value x for the base case, and a function f to process the value of the recursive call. Note that this does not allow us to define arbitrary recursive functions on the natural numbers, but only those that perform recursive calls on the predecessor of their argument. Allowing arbitrary recursion would open the door to partial functions, which would compromise the soundness of the calculus.

This example can be generalized to other inductive data types. For instance, we can define the type of lists of natural numbers as the type of their fold right function:

list_nat := forall T, T -> (nat -> T -> T) -> T