[TYPES] Y-combinator in Type:Type?
Herman Geuvers
herman at cs.ru.nl
Fri May 16 10:50:33 EDT 2008
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
More information about the Types-list
mailing list