|
|
 |
|
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
Y.
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. |
|
|
