[TYPES] Eliminators in type theory
Yong Luo
Y.Luo at kent.ac.uk
Thu Mar 16 12:28:02 EST 2006
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
More information about the Types-list
mailing list