Vendredi 20 Novembre

Retour à la vue des calendrier
Vendredi 20 Novembre
Heure: 11:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: The Y=Y(SI) problem
Description: Andrew Polonsky We discuss an important problem in untyped lambda calculus. Put forward by
Statman, it asks whether there exists a fixed point combinator Y such that
Y=Ydelta, where delta = SI = yx.x(yx). It is conjectured that there is no such

After basic introduction and examples, we will show how Statman's conjecture
naturally generalizes in two directions.

In the first perspective, we investigate general conditions on terms G1,..,GN
which are fpc generators: for all terms M, M fpc => M G1 .. GN fpc

In the second direction, we look at the simply-typed Y-calculus, in which a
"formal" fpc is introduced together with the rewrite rule Yx –> x(Yx) Given
an arbitrary fpc Y, there is an obvious interpretation of this calculus in the
untyped lambda calculus. The Y=Y(SI) conjecture is reduced to the
conservativity of this interpretation, for any Y.