• Nie Znaleziono Wyników

Rachunek lambda CBN i CBV

N/A
N/A
Protected

Academic year: 2021

Share "Rachunek lambda CBN i CBV"

Copied!
5
0
0

Pełen tekst

(1)

P. Urzyczyn: Materia ly do wyk ladu z semantyki1

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 (SOS2), 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

(2)

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

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

Przypadek 1: M = (λx A)B → A[B/x] = M0 ⇓ 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 ME 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 ME.

(3)

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

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 ⇓0V 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 ME 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 WE = 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]

(4)

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,,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, E0, @ :: C, Di ⇒ hnil, E[x 7→ ∆], M :: nil, hS, E0, Ci :: Di h∆ :: S, E0, nil, hS0, E0, C0i :: Di ⇒ h∆ :: S0, E0, C0, 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 ME ⇓ V , to hS, E, M :: C, Di  hhW, F i :: S, E, C, Di, gdzie WF = 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,,sciowe spe lniajace,

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

(5)

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 D0 i definiujemy Dn+1 jako [Dn → Dn]). 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 D0 na D do projekcji z [D0→ D0] na [D → D].

Cytaty

Powiązane dokumenty

Takie typy czasem się

For every number n of a type derivation for a lambda-term M there exists m such that every number of a finite reduction sequence of M is less

For every number n of a type derivation for a lambda-term M there exists m such that every number of a finite reduction sequence of M is less than m... Strong Normalization.. For

Uwaga: Klasyczny rachunek zdań jest.. Statman): Inhabitation in simple types is decidable and P SPACE -complete.?. Wniosek: To samo dotyczy minimalnego

(Potem zredukujemy J do typu bool → word.).. Typy proste: semantyka.. Schubert’97):.. Nierozstrzygalność drugiego rzędu nawet wtedy, gdy niewiadome nie są

I Validity/provability in second-order classical propositional logic (known as the QBF problem) is P SPACE -complete.. I Provability in second-order intuitionistic propositional

Twierdzenie ( Löb, 1976, Gabbay, 1974, Sobolew, 1977) Problem inhabitacji:.. Dany typ τ , czy istnieje term zamknięty M

I Przedmiotem dziaªania mo»e by¢ cokolwiek, zatem.. funkcja nie ma a priori