[TYPES] Eliminators in type theory

[Yong Luo]

I am not sure the system I specified is the same as the system T, and would
like to know how the fib function can be defined by the type of natural
numbers without introducing any other types.

Yong

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