# [TYPES] Eliminators in type theory

Andreas Abel abel at informatik.uni-muenchen.de
Fri Mar 17 10:23:16 EST 2006

```Sorry, I misread your message the first time.  You said you have neither
pair nor function types.

Anyway, pairs of natural numbers can be coded using the old trick

pair x y = 2^x * 3^y

This is primitive recursive (i.e., definable using Elim_Nat), and fst
and snd should be codable primitive recursively as well.  Then, fib is
definable using primitive recursion, but do not ask me about efficiency ;-)

Andreas

Andreas Abel wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Pairs can be simulated by with higher-order primitive recursion.  For
> instance, the following (Haskell) functions 'iter' and 'fib' are
> definable in type theory with function spaces, natural numbers, and
> eliminators alone.
>
> iter :: Int -> Int -> Int -> Int
> iter k l 0     = k
> iter k l (n+1) = iter l (k+l) n
>
> fib :: Int -> Int
> fib = iter 0 1
>
> fibs = [ fib i | i <- [0..]]
>
> test = take 15 fibs
> -- [0,1,1,2,3,5,8,13,21,34,55,89,144,233,377]
>
> Maybe you have to reformulate your question, such that the eliminators
> can only produce something of base type, e.g., inductive type, but not
> function type.  Then, the Ackermann function is not definable.
>
> Cheers,
> Andreas
>
> 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.
>>
>>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
>>
>>
>
>
>

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
```