# [TYPES] Eliminators in type theory

Andreas Abel abel at informatik.uni-muenchen.de
Fri Mar 17 08:11:32 EST 2006

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