[TYPES] Eliminators in type theory

[Andreas Abel]

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/