[TYPES] Y-combinator in Type:Type?

[Thorsten Altenkirch]

Dear Jonathan,

you are right primitive recursion can be defined from iteration. E.g.  
in the case of natural numbers, given

	It : (A:Type) -> A -> (A -> A) -> N -> A

satisfying

	It A z s 0 = z
	It A z s (succ n) = s (It A z s a)

we can define (using products)

	R : (A:Type) -> A -> (N -> A -> A) -> N -> A
	R A z s n = fst (It (NxA) (0,z) (\ (n,a) -> (succ n,s n a)) n)

but we cannot derive the equation

	R A a z s (succ n) = s n (R A a z s n)

from the equations for the iterator. We can only show by induction  
that the equation holds for all numerals, i.e. for all definable  
elements of type N.

Cheers,
Thorsten



On 19 May 2008, at 23:36, Jonathan P. Seldin wrote:

> I cannot believe the last statement about getting iteration but not  
> primitive recursion.  In Combinatory Logic, vol. II, section 3A3,  
> Curry gives several methods for defining the primitive recursion  
> combinator R in terms of an iterator Z, and the compatibility of  
> some of them with simple types is shown in section 13D3, especially  
> Theorem 13D3 for the R he calls R(Kp).  (The typing system Curry is  
> using here is $\lambda \rightarrow$, and he is writing Fab instead  
> of a -> b; furthermore, he is taking the type N of natural numbers  
> as an atomic type.  But with the Pi types and the impredicative  
> definitions, N can be defined.)
>
> On 19-May-08, at 8:16 AM, Thorsten Altenkirch wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>>  ]
>>
>> Actually, the initial PTS (Type : Type) has got no identity types but
>> only Pi-types. However, we can encode an equality type using the  
>> usual
>> "Leibniz encoding"
>>
>> Eq : (A:Type) -> A -> A -> Type
>> Eq A a b = Pi P:A -> Type.P a -> P b
>>
>> and this behaves like intensional equality actually worse: we cannot
>> even show that equality is a groupoid (actually using eta we can show
>> that it is a category but the laws involving symmetry require
>> parametricity, I think).
>>
>> If you add W-types with the normal elimination principle you get a
>> fixpoint combinator (See Thierry's paper on the paradox of Trees).
>> That's maybe cheaper then extensional equality (depending on your
>> currency). The problem is that the impredicative encodings don't give
>> you primitive recursion but only iteration - I'd say.
>>
>> Cheers,
>> Thorsten
>>
>> On 16 May 2008, at 16:41, Thomas Streicher wrote:
>>
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
>>>  ]
>>>
>>> But if you have Type:Type together with extensional identity types
>>> then
>>> every type X is equal to X->X and thus provides a model for untyped
>>> lambda calculus and thus allows one to write down an Y-combinator of
>>> type X.
>>>
>>> So the problem is open because of intensional identity types, isn't
>>> it?
>>>
>>> Thomas
>>
>>
>> This message has been checked for viruses but the contents of an  
>> attachment
>> may still contain software viruses, which could damage your  
>> computer system:
>> you are advised to perform your own checks. Email communications  
>> with the
>> University of Nottingham may be monitored as permitted by UK  
>> legislation.
>>
>
> 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
>
>
>


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.