[TYPES] Eliminators in type theory

[Jonathan Seldin]

If you are talking about a functional language that includes pure  
lambda-calculus, you might be interested in the discussion in Curry,  
Hindley, and Seldin, Combinatory Logic, vol. II (North-Holland,  
1968), section 13D.  Here R is Elim_Nat.  Definitions of Elim_Nat and  
pairs are given in terms of an iterator (called Z), which takes each  
numeral to its corresponding Church numeral (\xy.x(x(...(xy)...)),  
where there are n x's after the dot), and since this iterator can  
easily be defined in terms of Elim_Nat, the definitions would work in  
the proposed system.  This shows, I think, that fib could be defined  
in the proposed system without the numerical coding of pairs.

But this contains no information about efficiency.

On 17-Mar-06, at 8:32 AM, Ulrich Berger wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
> types-list ]
>
> 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
>>>
>>>
>>
>>
>>

Jonathan P. Seldin                                     tel: 403-329-2364
Department of Mathematics and Computer Science  jonathan.seldin at uleth.ca
University of Lethbridge                              seldin at cs.uleth.ca
4401 University Drive                    http://www.cs.uleth.ca/~seldin/
Lethbridge, Alberta, Canada, T1K 3M4