[TYPES] Y-combinator in Type:Type?

[Herman Geuvers]

Edsko de Vries wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Hi,
>
> Assuming that Type:Type (or *:*) in dependently typed languages is said
> to be inconsistent (Girard's paradox?). Does that mean that it is
> possible to define a Y combinator in such a language? 
>
>   

No but you can define a family of looping combinators:
    Y_0, Y_1, Y_2 ...
satisfying the property
    Y_i F = F(Y_{i+1} F)

This is proven in* A-translation and Looping Combinators in Pure Type 
Systems by Thierry Coquand, Hugo Herbelin, Journal of Functional 
Programming (1994)***

This is enough to type all partial recursive functions.
(For the know proof of representation of recursive functions in lambda 
calculus, a looping combinator suffices.)

Using the short proof of inconsistency by Hurkens, one can actually 
exhibit such a looping combinator, and if you look at the underlying 
"Curry variant" of it (which you can exhibit in the system lambda-U), 
then it is a fixed point combinator indeed. So the looping occurs just 
because the type information in the term gets bigger and bigger; the 
underlying untyped term is a fixed-point combinator. See also an old 
note of mine, where the latter result is just mentioned without proof.

Best Regards

Herman Geuvers


Reference:
||A. J. Hurkens, "A simplification of Girard's paradox", Proceedings of 
the 2nd international conference Typed Lambda-Calculi and Applications 
(TLCA'95), 1995.

H. Geuvers,
Inconsistency of classical logic in type theory, 
<http://www.cs.ru.nl/%7Eherman/PUBS/newnote.ps.gz> Short Note (Version 
of November 27, 2001) http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz