-1-INF 554 Luc MarangetInterpr´etation(environnements)Luc.Maranget@inria.frhttp://www.enseignement.polytechnique.fr/profs/informatique/Luc.Maranget/TLP/-2-A Un petit tour autour du point fixe.B De l’´evaluaton `a l’interpr´etation : environnements.C Interpr´etation par valeur.-3-Point fixe et r´eductionOn s’int´eresse aux « solutions » d’´equations du genre :x = t, avec x variable, et t terme de PCF ou` x apparaˆıt.s« = » est l’´egalit´e dans la s´emantique.sSoit u =Fix x -> t avecu−→ [u\x]tC’est-a`-dire, inventons le point fixe explicite.′ ′On pose l’exigence s´emantique t−→ t ⇒ t = t .sIl est alors ´evident que u est solution de x = t.s-4-Point fixe construitUne premi`ere ´etape : « abstraire x dans t ».′′x = (Fun y -> t ) x, avec t = [y\x]t.′◮ On a trivialement (Fun y -> t ) x−→ t.◮ Il apparaˆıt clairement que l’on recherche le point-fixe (x = Φ x)′d’une fonction Φ =Fun y -> t .∗ ′Soit un terme u tel que u−→ Φ u−→ [u\y]t ,′Soit en fait (car t = [y\x]t) :∗u−→ [u\y][y\x]t = [u\x]tC’est `a dire que u est solution.-5-Construction explicite∗De u tel que u←→ Φ u.Soit la fonction suivante curry :Fun f -> (Fun x -> f (x x)) (Fun x -> f (x x))On va montrer que pour tout terme Φ :∗curry Φ←→ Φ (curry Φ)∗(←→ fermeture r´eflexive-sym´etrique-transitive de−→, entraˆıne= ).s-6-∗D´emonstration de curry Φ←→ Φ (curry Φ)Posons v =Fun x -> f (x x) Par une β-r´eduction il vient :v v−→ f (v v)′ ′Lemme : t−→ t ⇒ [u\x]−→ [u\x]tDonc : ...