|
![](images/spacer.gif) |
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. |
|
|