[TYPES] Eliminators in type theory

[Yong Luo]

I would like to understand  how powerful the eliminators of inductive types
can be in type theory.

Suppose a type system has the type of natural numbers ONLY, that is, we have
only Nat, Zero, Successor (Succ) and the eliminator Elim_Nat and its two
computation rules.

Can we define fib function in such a system? Note that we don't have pairs
and function types.

fib 0 = 1
fib 1 = 1
fib (n+2) = fib n + fib (n+1)

In such a  system, we know some functions can be defined, for example,
plus x y = Elim_Nat (\n->Nat) x (\m,n->(S n)) y
If we add the type of pairs, then more efficient fib can be easily defined.

Thanks,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent