[TYPES] Eliminators in type theory

[Jonathan P. Seldin]

Dear Sergei,

Thank you for calling my attention to this.

However, the answer to Yong is still contained in Cjombinatory Logic,  
vol II.  In section 13D2 (pp. 277-279), Curry considers three pairing  
combinators D.  All three have types of the form A -> A -> B -> A for  
a type B which depends on the particular pairing combinator and any  
type A (including the type of natural numbers).  (The type B is  
related to the projection functions.)  With any of these pairing  
combinators, it should be possible to define fib.  (The problem that  
Curry reported with these pairing combinators was that they only had  
types if the first and second element of the pair had the same  
type.)  This shows that the numerical coding of pairs is not necessary.

In section 13D4 (pp. 285ff), Curry defines the class of functions he  
calls prorecursive to be those whose defining terms have types in his  
system, and in Theorem 13D1 (pp. 285-6), he proves that all primitive  
recursive functions are prorecursive using Elim_Nat restricted to  
output type Nat.  He goes on to assert that he has a proof that all  
doubly recursive numerical functions are prorecursive, and presents a  
conjecture that all n-recursive functions are in this class.  He does  
not explicitly say there that he has used Elim_Nat only with output  
of type Nat, but I have his notes here, and I can check his proof.

On Mar 18, 2006, at 5:14 AM, Sergei Soloviev wrote:

> Dear Jonathan,
>
> as far as I understand Yong, he considers typed lambda-calculus and  
> does not permit Elim_Nat
> with values in any other type than Nat, and in this situation it  
> seems not clear how to define iterator Z.
>
> Best regards,
>
> Sergei Soloviev
> IRIT
> Universite Paul Sabatier
> Toulouse
>
> (I did work for some time with Zhaohui Luo and his student Yong Luo.)
>
> ----- Original Message ----- From: "Jonathan Seldin"  
> <jonathan.seldin at uleth.ca>
> To: "type-list" <types-list at lists.seas.upenn.edu>
> Sent: Friday, March 17, 2006 8:15 PM
> Subject: Re: [TYPES] Eliminators in type theory
>
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/ 
>> types-list ]
>>
>> 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
>>
>

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