[TYPES] Eliminators in type theory
txa at cs.nott.ac.uk
Fri Mar 17 05:17:20 EST 2006
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).
> 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.
> Dr. Yong Luo
> Computing Laboratory
> University of Kent
Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516
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.
More information about the Types-list