cours sur les interprétations

Description

-1-INF 554 Luc MarangetInterpr´etation(environnements)[e-mail]://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 : ...

Sujets

• informatique

Informations

• Publié par: Vyof
• Nombre de lectures: 19
• Langue: Français

Extrait

-1-

INF 554

Luc Maranget

Interpre´tation (environnements)

[e-mail] http://www.enseignement.polytechnique.fr/profs/ informatique/Luc.Maranget/TLP/

-2-

A

B

C

Un petit tour autour du point fixe.

Del’e´valuatona`l’interpr´etation:

Interpre´tationparvaleur.

environnements.

-3-

Pointfixeetr´eduction

Ons’inte´resseaux«uslniotos»gedue:nrtauqsnoie´’d

x= s t,avecxvariable, etto`urmedePCFetxappa.tıˆar

s «= s »´lansda´eitaleg´’ltse.eituqmena

Soitu=Fixx->tavec

u−→[ux]t

C’est-`a-dire,inventonslepointfixeexplicite.

Onposel’exigences´emantiquet−→t ′ ⇒t= s t ′ .

Ilestalors´evidentqueuest solution dex= s t.

-4-

Point fixe construit

Unepremi`ere´etape:«abstrairexdanst».

x= (Funy->t ′ )x,avect ′ = [yx]t.

◮On a trivialement (Funy->t ′ )x−→t.

◮e(opni-txfiehcrehel’oelecnrmerequnttıˆaialcalIrappx= Φx) d’une fonction Φ =Funy->t ′ .

Soit un termeutel queu−→ ∗ Φu−→[uy]t ′ ,

Soit en fait (cart ′ = [yx]t) :

u− ∗ [uy][yx]t= [ux]t →

C’esta`direqueuest solution.

-5-

Construction explicite

Deutel queu←→ ∗ Φu.

Soit la fonction suivantecurry:

Funf-> (Funx->f(x x)) (Funx->f(x x))

On va montrer que pour tout terme Φ :

curryΦ←→ ∗ Φ (curryΦ)

(←→ ∗ erurfle´efeetrmrte´euqievixmys-sntit-arevide−→aˆınentr,e . = s )

-6-

D´emonstrationdecurryΦ←→ ∗ Φ (curryΦ)

Posonsv=Funx->f(x x) Par uneβt:envide´r-linoitcu

v v−→f(v v)

Lemme:t−→t ′ ⇒[ux]−→[ux]t ′

Donc : [Φf](v v)−→[Φf]f(v v).

Or (uneβ) :curryΦ−→[Φf](v v)

Et c’est fini :

(1)

(2)

curryΦ−→[Φf](v v)−→[Φf](f(v v ([Φ)) = Φf](v v))←−Φ (curryΦ)

-7-

Astuce ultime

NotonsF=Fixx->t effectue les substitution de. Onxdanst, d`ˆet: es que pr

F→[Fx]t→[[Fx]tx]t→[[[Fx]tx]tx]t→. . .

On obtient un terme«infini»unarepbl:heapgrr,peneat´rse

t

x

-8-

Plus

n

clair sur un

Fun

n

Ifz

0

n

*

exemple

@

n

-

1

-9-

Fabriquer un tel graphe

◮!fie´denu,lmaCnEvesiurecr´ontini

l e t recpcf fact= _ Fun("n", Ifz(Var"n",Num0, Op(Mul,Var"n", App(pcf_fact,Op(Sub,Var"n",Num1)))))

◮En Java/langage machine : modification d’un terme.

Pcf node= newApp(null,newOp(Sub,newVar("n"),newNum Pcf top=newFun("n",newIfz(. . .)) ; node.left=top

(1)))

;

-10-

Environnements

-11-

Appel par nom

t 1 ֒→ n Funx->t 3 [t 2 x]t 3 ֒→ n v t 1 t 2 ֒→ n v

Funx->t ֒→ n Funx->t

[t 1 x]t 2 ֒→ n v Letx=t 1 Int 2 ֒→ n v

t 1 ֒→ n 0t 2 ֒→ n v Ifzt 1 Thent 2 Elset 3 ֒→ n v

t 1 ֒→ n n 1 t 2 ֒→ n n 2 t 1 opt 2 ֒→ n n 1 opn 2

[(Fixx->t)x]t ֒→ n v Fixx->t ֒→ n v

t ֒→n(n6=0)t

t 1 ֒→ n n(n6=0)t 3 ֒→ n v Ifzt 1 Thent 2 Elset 3 ֒→ n v

n ֒→ n n