# [TYPES] Eliminators in type theory

Ulrich Berger U.Berger at swansea.ac.uk
Fri Mar 17 10:32:59 EST 2006

```Even if you disallow function types as result type of an elimination,
coding of two numbers into a single one as well as the corresponding
projections can be defined (old stuff in books on computability theory
or logic).

Uli

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