[TYPES] Eliminators in type theory

[Ulrich Berger]

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