Rachunek lambda CBN i CBV

P. Urzyczyn: Materia ly do wyk ladu z semantyki¹

Rachunek lambda CBN i CBV

Rachunek lambda czesto uwa˙zamy za abstrakcyjny j_, ezyk programowania funkcyjnego. Jednak_, ewaluacja wyra˙zenia w rzeczywistych jezykach funkcyjnych r´_, o˙zni sie istotnie od beta-redukcji._, Po pierwsze, mamy wtedy okre´slona deterministyczn_, a strategi_, e redukcji. Po drugie, zwykle nie_, dokonuje sie ewaluacji_,

”pod lambda”: wyra˙zenie zdolne do pobrania argumentu (zg laszaj_, ace_, prompt) jest uwa˙zane za

”gotowa funkcj_, e” i nie podlega ewaluacji a˙z do chwili dostarczenia_, parametru aktualnego. Dlatego lepszymi modelami jezyk´_, ow funkcyjnych sa takie wersje ra-_, chunku lambda, w kt´orych ka˙zda abstrakcj_, e uwa˙zamy za warto´_, s´c. Jeden z takich modeli to leniwy rachunek lambda, nazywany te˙z rachunkiem CBN . Opiszemy trzy rodzaje semantyki operacyjnej dla term´ow zamknietych tego j_, ezyka. B_, ed_, a to:_,

• Semantyka tranzycyjna, okre´slona za pomoc

a maszyny abstrakcyjnej. Modeluje ona,

proces obliczenia przez opisanie zmian stanu maszyny.

• Semantyka strukturalna (SOS²), w dw´och smakach:

– Semantyka ma lych krok´ow, kt´ora definiuje pojedynczy krok ewaluacji

”po´srednio”, przez indukcje ze wzgl_, edu na struktur_, e ewaluowanego wyra˙zenia;_,

– Semantyka du˙zych krok´ow, kt´ora definiuje od razu relacje M ⇓ V pomi_, edzy_, wyra˙zeniem M i jego warto´scia V ._,

Ma le kroki dla CBN

Relacja → w zbiorze term´ow to najmniejsza taka relacja, ˙ze (λxA)B → A[B/x], oraz je´sli A → B to tak˙ze AC → BC. Zapisujemy to w skr´ocie w postaci takich regu l:

(λxA)B → A[B/x] A → B

AC → BC Du ˙ze kroki dla CBN

Relacja M ⇓ V , gdzie M jest dowolnym termem zamknietym, a V jest warto´_, scia, czyli_, abstrakcja, jest okre´_, slona regu lami:

V ⇓ V M ⇓ λxA A[N/x] ⇓ V

M N ⇓ V

Udowodnimy, ˙ze te dwie definicje sa r´_, ownowa˙zne. Poni˙zej mowa o termach zamknietych._, Lemat 0.1 Je´sli M ⇓ V , to M  V .

Dow´od: Indukcja ze wzgledu na definicj_, e M ⇓ V . W kroku indukcyjnym zak ladamy, ˙ze_, M N ⇓ V , bo M ⇓ λxA oraz A[N/x] ⇓ V . Te dwie asercje maja kr´_, otsze wyprowadzenia, wiec z za lo˙zenia indukcyjnego wnioskujemy, ˙ze M  λxA oraz A[N/x]  V . Ostatecznie_, otrzymujemy redukcje M N  (λxA)N → A[N/x]  V ._,

1Pierwotna wersja tego materia lu powsta la we wsp´o lpracy z M. Zielenkiewiczem.

2Structural Operational Semantics

Lemat 0.2 Je˙zeli M  M⁰ ⇓ V , to M ⇓ V .

Dow´od: Dow´od jest przez indukcje ze wzgl_, edu na d lugo´_, s´c ciagu redukcji M  M_, ⁰. Oczy- wi´scie najwa˙zniejszy jest przypadek jednego kroku. Niech wiec M → M_, ⁰. U˙zyjemy indukcji ze wzgledu na definicj_, e relacji →._,

Przypadek 1: M = (λx A)B → A[B/x] = M⁰ ⇓ V . Mamy wtedy takie wyprowadzenie:

λx A ⇓ λx A A[B/x] ⇓ V M ⇓ V

Przypadek 2: M = AC → BC ⇓ V , bo A → B. Chcemy pokaza´c AC ⇓ V . Skoro BC ⇓ V , to B ⇓ λx D oraz D[C/x] ⇓ V . Z

”wewnetrznego” za lo˙zenia indukcyjnego dla A → B,_, wnioskujemy, ˙ze A ⇓ λx D, a poniewa˙z D[C/x] ⇓ V , wiec AC ⇓ V ._,

Wniosek 0.3 Dla dowolnych M i V , warunki M ⇓ V i M  V sa r´_, ownowa˙zne.

Uproszczona maszyna Krivine’a

Maszyna abstrakcyjna opisana poni˙zej r´o˙zni sie troch_, e od oryginalnej maszyny J.-L. Krivine’a._, G l´ownie dlatego, ˙ze pomijamy tu ca lkowicie sprawe reprezentacji term´_, ow i otocze´n. Tymcza- sem ”prawdziwa” maszyna Krivine’a pos luguje sie termami w notacji De Bruijna (indeksy_, zamiast zmiennych), obejmuje konkretna implementacj_, e otocze´_, n i algorytmy ich obs lugi.

W definicji maszyny wystepuj_, a dwa poj_, ecia zdefiniowane przez wzajemn_, a rekursj_, e:_,

• Otoczenie, to funkcja cze´_,sciowa, kt´ora zmiennym przypisuje domkniecia._,

• Domkniecie, zwane te˙z klozur_, a (ang. closure), to para hM, Ei, gdzie x jest zmienn_, a,_, oraz E jest takim otoczeniem, ˙ze FV(M ) ⊆ Dom(E).

Ta definicja jest poprawna (dobrze ufundowana), bo otoczenie mo˙ze by´c puste.

Konfiguracja maszyny Krivine’a to niepusta lista domknie´_,c, kt´ora mo˙ze by´c widziana jako tr´ojka postaci hM, Ei :: S. Mamy tu term M do ewaluacji w otoczeniu E, i

”stos” S. Konfi- guracja poczatkowa ma posta´_, c hM, ∅i :: nil, gdzie M jest termem zamknietym, a konfiguracja_, ko´ncowa powinna by´c postaci hV, Ei :: nil .

Ewaluacja aplikacji odbywa sie metod_, a_,

”push-enter”, tj. polega na od lo˙zeniu argumentu na stos (push) i wej´sciu w ewaluacje operatora (enter). Maszyna ma takie instrukcje:_,

hx, Ei :: S ⇒ E(x) :: S;

hM N, Ei :: S ⇒ hM, Ei :: hN, Ei :: S;

hλx M, Ei :: ∆ :: S ⇒ hM, E[x 7→ ∆]i :: S.

Zdefiniujemy teraz znaczenie domkniecia (M, E), czyli znaczenie termu M w otoczeniu E._, Real(M, E) = M [Real(E(y))/y]_y∈Dom(E)

Powy˙zej chodzi oczywi´scie o jednoczesne podstawienie na wszystkie zmienne y ∈ Dom(E).

Definicja M^E ma sens tak˙ze wtedy, gdy (M, E) nie jest domknieciem, tj. E(y) nie jest_, okre´slone dla jakiego´s y ∈ FV(M ). Taka zmienna y pozostaje wtedy wolna w M^E.

Lemat 0.4 (Poprawno´s´c maszyny) Je´sli M^E ⇓ V , to hM, Ei :: S  hW, F i :: S, gdzie W jest warto´scia i W_, ^F = M^E.

Dow´od: Indukcja ze wzgledu na definicj_, e relacji ⇓. Szczeg´_, o ly pomijamy.

W dowodzie nastepnego lematu u˙zyjemy pomocniczej relacji ⇓_, k, kt´ora jest zdefiniowana tak:

V ⇓₀V M ⇓_kλx A A[N/x] ⇓_`V

M N ⇓_k+`V

Je´sli M ⇓_iV dla pewnego i ≤ k, to napiszemy M ⇓_k. W przeciwnym razie M 6⇓_k.

Lemat 0.5 Je´sli M^E 6⇓_k, to maszyna uruchomiona w stanie hM, Ei :: nil wykonuje wiecej_, ni˙z k krok´ow.

Dow´od: Indukcja ze wzgledu na k. Szczeg´_, o ly pomijamy.

Wniosek 0.6 Je´sli M jest termem zamknietym, to M ⇓ V wtedy i tylko wtedy, gdy maszyna_, Krivine’a ma obliczenie hM, ∅i  hW, Ei, gdzie W^E = V .

Rachunek lambda w wersji CBV

W rachunku leniwym przekazywanie parametr´ow odbywa sie_,

”przez nazwe”, tj. parametr_, aktualny jest przekazywany do procedury bez ewaluacji. W rzeczywistych jezykach cz_, esto_, mamy do czynienia z przekazywaniem parametr´ow

”przez warto´s´c”. Wtedy parametr aktualny musi sam by´c warto´scia. Tak_, a strategi_, e ewaluacji modeluje rachunek lambda w wersji CBV._, Oto regu ly semantyki du˙zych krok´ow dla takiego rachunku:

V ⇓ V M ⇓ λx A N ⇓ W A[W/x] ⇓ V

M N ⇓ V Symbole V i W oznaczaja tu warto´_, sci, czyli abstrakcje.

Definicja semantyki ma lych krok´ow dla CBV wymaga pojecia kontekstu ewaluacyjnego. Kon-_, tekst ewaluacyjny E[ ], z jedna_,

”dziura” oznaczan_, a przez [ ], mo˙ze by´_, c postaci:

[ ] V E[ ] E[ ]M ,

Fakt 0.7 Ka˙zdy term zamkniety M , kt´_, ory nie jest warto´scia, mo˙zna w dok ladnie jeden_, spos´ob przedstawi´c w postaci M = E[R], gdzie E jest kontekstem ewaluacyjnym, a R jest beta-redeksem.

Dow´od: Cwiczenie.´

Dzieki jednoznaczno´_, sci rozk ladu, poni˙zsze regu ly ewaluacji

”przez warto´s´c” okre´slaja deter-_, ministyczna strategi_, e redukcji:_,

(λx A)V → A[V /x] A → B

E[A] → E[B]

Fakt 0.8 Warunki M ⇓ V i M  V sa r´_, ownowa˙zne.

Dow´od: Podobny do dowodu Wniosku 0.3.

Maszyna SECD

Maszyna SECD zosta la opisana przez P.J. Landina w roku 1965 i jest jedna z najstarszych_, maszyn abstrakcyjnych. Stan maszyny opisywany jest przez czw´orke hS, E, C, Di, a nazwy_, sk ladowych Stack , Environment , Code i Dump, t lumacza jednocze´_, snie znaczenie skr´otu.

Mamy wiec:_,

• Stack – czyli list

e domkni, e´_,c postaci hV, Ei;

• Environment – czyli otoczenie;

• Code – czyli liste_,

”operator´ow” (operatorami sa termy i symbol @);_,

• Dump – czyli liste tr´_, ojek postaci hS, E, Ci.

Idea jest taka: Wyra˙zenie przeznaczone do ewaluacji w otoczeniu E, umieszczone poczatkowo_, w C, jest rozk ladane na cze´_,sci (od prawej). Ka˙zda cze´_,s´c w postaci domkniecia jest umieszczana_, na stosie. Kiedy na poczatku listy C pojawi si_, e symbol @, maszyna ewaluuje operator_, z poczatku stosu, u˙zywaj_, ac nast_, epnego domkni_, ecia ze stosu jako argumentu. Odbywa si_, e_, to przez rekurencyjne wywo lanie ca lego procesu (po to jest sk ladowa D). Ta metoda ewalu- acji nazywana jest

”eval-apply”. Instrukcje maszyny sa takie:_, hS, E, x :: C, Di ⇒ hE(x) :: S, E, C, Di hS, E, λxM :: C, Di ⇒ hhλxM, Ei :: S, E, C, Di

hS, E, M N :: C, Di ⇒ hS, E, N :: M :: @ :: C, Di

hhλxM, Ei :: ∆ :: S, E⁰, @ :: C, Di ⇒ hnil, E[x 7→ ∆], M :: nil, hS, E⁰, Ci :: Di h∆ :: S, E⁰, nil, hS⁰, E⁰, C⁰i :: Di ⇒ h∆ :: S⁰, E⁰, C⁰, Di

Konfiguracja poczatkowa ma posta´_, c hnil, ∅, M :: nil, nili, a ko´ncowa h∆ :: nil, ∅, nil, nili. Mamy teraz dwa lematy podobne do lemat´ow 0.4 i 0.5.

Lemat 0.9 Je´sli M^E ⇓ V , to hS, E, M :: C, Di  hhW, F i :: S, E, C, Di, gdzie W^F = V . Lemat 0.10 Je´sli M 6⇓_k to maszyna SECD, uruchomiona w konfiguracji hS, E, M :: C, Di, wykonuje co najmniej k krok´ow.

Wniosek 0.11 Je´sli M jest termem zamknietym, to M ⇓ V wtedy i tylko wtedy, gdy maszyna_, SECD ma obliczenie hnil, ∅, M :: nil, nili  hhW, F i, ∅, nil, nili.

Semantyka denotacyjna dla CBN i CBV

Modelami standardowej teorii rachunku lambda sa zupe lne porz_, adki cz_, e´_,sciowe spe lniajace_,

”r´ownanie” postaci D ∼= [D → D]. W przypadku rachunku CBN jest troche inaczej, bo_,

nie ka˙zdy element dziedziny powinien by´c interpretowany jako funkcja. Na przyk lad trzeba rozr´o˙znia´c termy Ω i λx Ω. Pierwszy chcemy interpretowa´c jako element najmniejszy ⊥, a drugi jako funkcje sta l_, a λλd. ⊥. Interesuje wi_, ec nas rozwi_, azanie innego r´_, ownania, a miano- wicie D ∼= [D → D]⊥, gdzie A⊥ oznacza zbi´or A z dodatkowym elementem najmniejszym ⊥.

(Dotychczasowy element najmniejszy w A przestaje pe lni´c te funkcj_, e.) Rozwi_, azanie takiego_, r´ownania mo˙zna uzyska´c powtarzajac konstrukcj_, e modelu D_, ∞z odpowiednimi modyfikacjami (zaczynamy od jednoelementowego zbioru D₀ i definiujemy D_n+1 jako [D_n → D_n]⊥). Tak otrzymany model nie jest jednak w pe lni abstrakcyjny ze wzgledu na obserwacyjn_, a r´_, ownowa˙z- no´s´c odpowiednia dla CBV (tak_, a gdzie zamiast o istnienie czo lowej postaci normalnej pytamy_, o redukcje do warto´_, sci.) Modele w pe lni abstrakcyjne mo˙zna uzyska´c w grach.

W przypadku rachunku CBV, opr´ocz rozr´o˙znienia Ω i λx Ω trzeba jeszcze uwzgledni´_, c koniecz- no´s´c ewaluacji argumentu. Nie interesuja nas wi_, ec dowolne funkcje ci_, ag le, ale tylko_,

”rzetelne”, tj. funkcje o w lasno´sci f (⊥) = ⊥. Je´sli [D →⊥ D] oznacza przestrze´n funkcji rzetelnych, to r´ownanie dziedzinowe przyjmuje posta´c D ∼= [D →⊥D]⊥. Metoda Scotta otrzymamy dobry_, model, kt´ory znowu nie bedzie w pe lni abstrakcyjny._,

Cwiczenia:´

1. Zdefiniowa´c maszyne SECD w wersji CBV._,

2. Czy wnioski 0.6 i 0.11 mo˙zna wzmocni´c ˙zadaj_, ac aby W = V i F = ∅?_, 3. Zdefiniowa´c projekcje z [D → D]_{, ⊥} na D oraz metode_,

”podnoszenia” projekcji (i, j) z D⁰ na D do projekcji z [D⁰→ D⁰]_⊥ na [D → D]_⊥.