[TYPES] Eliminators in type theory
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
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.
> 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
>>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.
>>Dr. Yong Luo
>>University of Kent
More information about the Types-list