[TYPES] Eliminators in type theory

[Thorsten Altenkirch]

Yong Luo wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> 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.

This is a functional representation of arithmetic, i.e. Goedel's system T. All functions 
provable total in arithmetic can be defined. Adding dependent types doesn't affect the 
strength of the system, nether does the addition of pairs (whether dependent or not).

T.

> 
> 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
> 
> 

-- 
Dr. Thorsten Altenkirch		   phone : (+44) (0)115 84 66516
Lecturer			   http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT	   University of Nottingham

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.