9 Rachunek kombinator´ ow

Zdefiniujemy teraz system CL (beztypowego) rachunku kombinator´ow, zwany tak˙ze (z przy-czyn historycznych) logika kombinatoryczn_, a, chocia˙z ta druga nazwa jest nieco myl_, aca. Zbi´_, or term´ow C definiujemy jako najmniejszy zbi´or o w lasno´sciach:

• Zmienne przedmiotowe nale˙z a do C;,

• Sta le K i S nale˙za do C;_,

• Je´sli F, G ∈ C, to (F G) ∈ C.

Konwencje nawiasowe sa takie same jak dla term´_, ow rachunku lambda. Podstawienie w CL definiujemy podobnie jak dla rachunku lambda, ale latwiej, bo nie ma zmiennych zwiazanych._,

• x[x := F ] = F oraz y[x := F ] = y dla y 6= x;

• K[x := F ] = K oraz S[x := F ] = S;

• GH[x := F ] = G[x := F ]H[x := F ].

Relacje s labej redukcji w zbiorze C definiujemy jako najmniejsz_, a relacj_, e →_{, w} o w lasno´sciach:

• KAB →_w A dla dowolnych A, B;

• SABC →_w AC(BC) dla dowolnych A, B, C;

• Je´sli A →_w B, to AC →_w BC oraz CA →_w CB, dla dowolnych A, B, C.

Jak zwykle, symbol w oznacza domkniecie przechodnio-zwrotne relacji →_{, w}, a =_w (s laba r´owno´s´c), to najmniejsza relacja r´ownowa˙zno´sci zawierajaca →_{, w}. Termy rachunku kombi-nator´ow, kt´ore nie zawieraja zmiennych, nazywamy oczywi´_, scie kombinatorami . Zamkniete_, termy rachunku lambda przeje ly t_, e nazw_, e od swoich odpowiednik´_, ow w C. Oto kilka wa˙znych kombinator´ow i zwiazane z nimi redukcje:_,

• Niech I = SKK. Wtedy IF →_wKF (KF ) →_w F dla dowolnego F .

• Term Ω = SII(SII) redukuje sie sam do siebie._,

• Niech W = SS(KI). Wtedy WF G w F GG dla dowolnych F, G.

• Niech B = S(KS)K. Wtedy BF GH w F (GH), dla dowolnych F, G, H.

• Niech C = S(BBS)(KK). Wtedy CF GH wF HG dla dowolnych F, G, H.

• Niech B⁰= CB. Wtedy B⁰F GH w G(F H).

• Niech D = C(BC(B(CI)K)). Wtedy DF GH w H(KG)F .

• Niech 2 = SB(SB(KI)). Wtedy 2F G w F (F G).

Uwaga: Termy K, S, KS, SK, I, B, 2, W sa w postaci w-normalnej, a termy B_, ⁰, C nie sa._, Czasem wszystkie te kombinatory sa jednak traktowane jak sta le._,

System CL, jako system redukcyjny, ma w lasno´sci podobne do rachunku lambda. Na przy-k lad prawdziwe jest twierdzenie Churcha-Rossera, a taprzy-kie w lasno´sci jak normalizacja, silna normalizacja, czy r´owno´s´c, sa nierozstrzygalne. System CL ma bowiem podobn_, a si l_, e wyrazu_,

— mo˙zna w nim na przyk lad zdefiniowa´c liczebniki i reprezentowa´c funkcje cze´_,sciowo rekuren-cyjne. W istocie, logika kombinatoryczna zosta la wynaleziona przez Curry’ego i Sch¨onfinkela niezale˙znie od rachunku lambda i mniej wiecej w tym samym czasie, ale w gruncie rzeczy_, w podobnym celu.

Podobie´nstwo pomiedzy CL i rachunkiem lambda mo˙zna wyrazi´_, c definiujac translacje_, ( )_Λ: C → Λ ( )C : Λ → C

Pierwsza z nich jest latwa:

• (x)_Λ = x dla x ∈ V ;

• (K)_Λ = λxy.x;

• (S)_Λ= λxyz.xz(yz);

• (F G)_Λ= (F )_Λ(G)_Λ.

Nastepuj_, acy latwy fakt wyra˙za poprawno´_, s´c tej translacji ze wzgledu na redukcje._, Fakt 9.1

• Je´sli F w G, to (F )_Λβ (G)_Λ.

• Je´sli F =_w G, to (F )_Λ=_β (G)_Λ.

Fakt 9.1 mo˙zna odczyta´c tak: translacje ( )_, Λ mo˙zna uwa˙za´c za przekszta lcenie z C/=w

do Λ/=_β, czyli za morfizm z teorii r´owno´sciowej CL do teorii r´owno´sciowej Λ.

Aby okre´sli´c translacje ( )_, C: Λ → C musimy przede wszystkim zdefiniowa´c w CL konstrukcje_, (zwana kombinatoryczn_, a abstrakcj_, a), kt´_, ora zachowuje sie tak jak abstrakcja. Mo˙zna to zrobi´_, c na kilka sposob´ow, na przyk lad tak:

• λ^∗x.F = KF , gdy x 6∈FV(F );

• λ^∗x.x = I;

• λ^∗x.F G = S(λ^∗x.F )(λ^∗x.G), w przeciwnym przypadku.

Dow´od poni˙zszego faktu pozostawiamy jako ´cwiczenie.

Fakt 9.2 (λ^∗x.F )G w F [x := G].

Wniosek 9.3 (kombinatoryczna zupe lno´s´c) Dla dowolnych x i F istnieje takie H, ˙ze dla dowolnego G zachodzi HG wF [x := G].

Teraz mo˙zemy zdefiniowa´c translacje ( )_, C: Λ → C.

• (x)_C = x dla x ∈ V ;

• (M N )_C= (M )C(N )C;

• (λx.M )_C = λ^∗x.(M )C.

Fakt 9.4 Dla dowolnego M ∈ Λ zachodzi ((M )C)_Λ =_β M .

Dow´od: Najpierw nale˙zy pokaza´c (λ^∗x.F )_Λ=_β λx (F )_Λ, przez indukcje ze wzgl_, edu na F ._, Potem te˙z indukcja ze wzgledu na M ._,

A zatem translacja ( )_Λ wyznacza przekszta lcenie

”na” z ilorazu C/=w do Λ/=_β. Poni˙zszy wniosek stwierdza, ˙ze termy K i S stanowia baz_, e dla rachunku lambda._,

Wniosek 9.5 Ka˙zdy zamkniety lambda-term mo˙zna otrzyma´_, c (z dok ladno´scia do =_{, β}) z ter-m´ow K i S przez stosowanie aplikacji.

Dow´od: Natychmiast z Faktu 9.4.

Niestety, operacja ( )C nie ma tak dobrych w lasno´sci jak translacja ( )Λ. Nie mo˙zna jej uwa˙za´c za morfizm teorii r´owno´sciowych.

Fakt 9.6

• Z lo˙zenie (( )_Λ)C nie jest identyczno´scia. Na przyk lad ((K_{, Λ})C = S(KK)I 6=_wK.

• Z r´owno´sci M =β N nie wynika (M )C =w (N )C. Na przyk lad λx.KIx →β λx I, ale (λx.KIx)C= S(K(S(KK)II))I =w S(K(KI))I 6=w KI = (λx I)C.

A zatem

”s laba” r´owno´s´c jest w istocie silniejsza ni˙z =β. Przyczyna tego jest to, ˙ze kombina-_, toryczna abstrakcja λ^∗ nie spe lnia warunku s labej ekstensjonalno´sci ze wzgledu na =_{, w}:

M = N

λx.M = λx.N , (ξ)

W istocie

λ^∗x.KIx = S(K(KI))I 6=_w KI = λ^∗x.I,

chocia˙z KIx →w I. Mo˙zna to poprawi´c kosztem wprowadzenia ekstensjonalno´sci. Niech =ext

bedzie najmniejsza relacj_, a r´_, ownowa˙zno´sci w C, taka ˙ze:_,

• Je´sli G =_w H, to G =_ext H;

• Je´sli Gx =_ext Hx i x 6∈FV(G) ∪FV(H), to G =ext H;

• Je´sli G =_ext G⁰, to GH =_ext G⁰H i HG =_ext HG⁰.

Fakt 9.7

• Dla dowolnych G, H ∈ C, warunki G =_ext H i (G)_Λ=_βη (H)_Λ sa r´_, ownowa˙zne.

• Dla dowolnych M, N ∈ Λ, warunki M =_βηN i (M )C =ext (N )C sa r´_, ownowa˙zne.

• R´ownanie ((G)_Λ)C=ext G zachodzi dla dowolnego G ∈ C.

Paradoks Curry’ego

Skoro lambda-abstrakcja mo˙ze by´c zdefiniowana w rachunku CL, to si la wyrazu rachunku kombinator´ow jest podobna do si ly wyrazu rachunku lambda. Mo˙zemy na przyk lad zdefinio-wa´c kombinatory punktu sta lego:

Y = WS(BWB) Θ = WI(B(SI)(WI)).

Dlatego rachunek kombinator´ow jest zbyt silny na to, aby m´og l by´c prawdziwa logik_, a kombi-_, natoryczna. Zobaczmy jak dodanie logiki do systemu CL mo˙ze prowadzi´_, c do sprzeczno´sci.

Zdefiniujemy system NCL

”naiwnej logiki kombinatorycznej”, dodajac do sk ladni now_, a sta l_, a P,_, kt´ora ma przedstawia´c implikacje. Zamiast PF G b_, edziemy pisa´_, c F ⇒ G. W ten spos´ob dowolna zdaniow_, a formu l_, e implikacyjn_, a mo˙zna uwa˙za´_, c za term rachunku kombinator´ow.

Aby mo˙zna by lo udowodni´c taka formu l_, e, regu ly wnioskowania systemu NCL pozwalaj_, a_, wyprowadza´c nie tylko r´owno´sci miedzy termami, ale te˙z same termy._, System ma trzy schematy aksjomat´ow:

Ostatnia regu la to dobrze znana regu la odrywania. Opr´ocz niej mamy dwa niewinne aksjo-maty rachunku zda´n i dosy´c oczywiste w lasno´sci r´owna´n, w tym regu le konwersji: zdanie_, r´owne zdaniu udowodnionemu nale˙zy uwa˙za´c za udowodnione. Niestety,

Fakt 9.8 (Paradoks Curry’ego) System NCL jest logicznie sprzeczny: ka˙zdy term (w tym ka˙zda formu la) ma dow´od.

Dow´od: We´zmy dowolny term F i niech N = Y(λ^∗x. x ⇒ F ). Nietrudno sprawdzi´c, ˙ze r´ownanie N = N ⇒ F ma dow´od w systemie NCL (term Y to kombinator punktu sta lego).

Zatem N ⇒ (N ⇒ F ) = N ⇒ N w NCL, a poniewa˙z N ⇒ N jest aksjomatem, wiec stosuj_, ac_, regu le (Conv) udowodnimy, ˙ze N ⇒ (N ⇒ F )._, U˙zywajac (MP) i trzeciego aksjomatu,_, wyprowadzimy stad N ⇒ F , ale przecie˙z mamy ju˙z N = N ⇒ F , wi_, ec udowodnili´_, smy tak˙ze N . Ale z N ⇒ F i N wynika F przez modus ponens, a F by lo dowolnym termem.

Cwiczenia´

1. Niech B = λxyz.x(yz) i niech C = λxyz.xzy. Pokaza´c, ˙ze ka˙zdy λI-term mo˙zna otrzyma´c (z dok ladno´scia do =_{, β}) z term´ow S, B, C, I, poprzez stosowanie aplikacji. Wskaz´owka: zdefi-niowa´c konstrukcje λ_, ^◦x.F w ten spos´ob, ˙ze:

• λ^◦x.F G = C(λ^◦x.F )G, gdy x ∈ FV(F ) oraz x 6∈ FV(G);

• λ^◦x.F G = BF (λ^◦x.G), gdy x 6∈ FV(F ) oraz x ∈ FV(G).

2. Term nazwiemy afinicznym, gdy ka˙zdy jego podterm postaci λx.M zawiera co najwy˙zej jedno wolne wystapienie zmiennej x._, Pokaza´c, ˙ze ka˙zdy afiniczny lambda-term mo˙zna otrzyma´c (z dok ladno´scia do =_{, β}) z term´ow B, C, K poprzez stosowanie aplikacji.

3. Term nazwiemy liniowym, gdy ka˙zdy jego podterm postaci λx.M zawiera dok ladnie jedno wolne wystapienie zmiennej x. Pokaza´_, c, ˙ze ka˙zdy liniowy lambda-term mo˙zna otrzyma´c (z dok ladno´ s-cia do =_{, β}) z term´ow B, C, I poprzez stosowanie aplikacji.

Problem otwarty:

Zdefiniowa´c taka (obliczaln_, a) translacj_, e T : Λ → C, ˙ze_,

M =βN ⇐⇒ T (M ) =wT (N ).

10 Modele

Zaczniemy od pewnej og´olnej teorii, potrzebnej dla u´sci´slenia pojecia modelu dla rachunku_, lambda. Naszym zamiarem jest interpretacja ka˙zdego lambda-termu M w pewnej konkretnej dziedzinie A, jako pewnego elementu [[M ]] ∈ A. Poniewa˙z mamy w termach zmienne wolne, wiec nasza interpretacja mo˙ze zale˙ze´_, c od warto´sciowania v : V → A (gdzie V oznacza zbi´or wszystkich zmiennych), co zaznaczymy piszac [[M ]]_{, v}. Indeks_v pomijamy, gdy v jest znane, lub M nie ma zmiennych wolnych. Poni˙zsza definicja formu luje nasze podstawowe oczekiwania w stosunku do takiej interpretacji.

Niech · bedzie dwuargumentow_, a operacj_, a w zbiorze A i niech [[ ]] : Λ × A_, ^V → A. Struk-ture A = hA, ·, [[ ]] i nazywamy lambda-interpretacj_, a, je˙zeli spe lnione s_, a warunki (a) – (d)_, poni˙zej. Stosujemy notacje [[M ]]_, v na oznaczenie warto´sci [[ ]](M, v). Symbol v[x 7→ a] oznacza warto´sciowanie r´o˙zniace si_, e od v tylko tym, ˙ze v[x 7→ a](x) = a._,

(a) Je´sli x jest zmienna, to [[x]]_{, v} = v(x);

(b) [[P Q]]v = [[P ]]v· [[Q]]_v;

(c) [[λx.P ]]v· a = [[P ]]_v[x7→a], dla dowolnego a ∈ A;

(d) Je´sli v|_{FV(P )}= u|_{FV(P )}, to [[P ]]_v = [[P ]]_u.

Na pierwszy rzut oka mo˙ze sie wydawa´_, c, ˙ze warunki (a) – (d) stanowia indukcyjn_, a definicj_, e_, funkcji [[ ]]. Tak nie jest, bo warunek (c) nie okre´sla kt´orym elementem modelu jest [[λx.P ]]_v a postuluje tylko jego zachowanie przy aplikacji. (Elementu, kt´ory tak sie zachowuje, mo˙ze_, w og´ole nie by´c.)

Je´sli a, b ∈ A, to napiszemy a ≈ b, gdy dla dowolnego c ∈ A zachodzi r´owno´s´c a · c = b · c.

Oznacza to, ˙ze zachowanie a i b jako funkcji jest takie samo. Interpretacja jest ekstensjonalna wtedy i tylko wtedy, gdy z warunku a ≈ b wynika a = b.

Lambda-interpretacje A = hA, ·, [[ ]] i nazywamy_,

• lambda-algebra, gdy warunek M =_{, β} N implikuje [[M ]]_v= [[N ]]_v dla dowolnego v (co zapiszemy A |= M = N );

• lambda-modelem, gdy warunek [[λx.M ]]_v ≈ [[λx.N ]]_v implikuje [[λx.M ]]_v = [[λx.N ]]_v. A wiec lambda-algebra to poprawna interpretacja beta-r´_, owno´sci. Natomiast lambda-model to interpretacja s labo ekstensjonalna, tj. taka, w kt´orej ekstensjonalno´s´c zachodzi dla abstrakcji.

Aby zrozumie´c o co chodzi, zauwa˙zmy tu, ˙ze [[λx.M ]]v ≈ [[λx.N ]]_v oznacza tyle samo co [[M ]]_v[x7→a]= [[N ]]_v[x7→a]dla wszystkich a. A zatem warunek s labej ekstensjonalno´sci w definicji

lambda-modelu m´owi, ˙ze znaczenie abstrakcji [[λx.M ]]_v jest zdeterminowane przez funkcje,_, kt´ora ka˙zdemu a przypisuje element [[M ]]_v[x7→a]. Nieformalnie: warto´s´c [[λx.M ]] zale˙zy tylko od warto´sci [[M ]], podobnie jak [[M N ]] zale˙zy tylko od [[M ]] i [[N ]]. Oznacza to tyle, ˙ze abstrakcja jest operacja semantyczn_, a (ma sens w modelu, niezale˙zny od sk ladni) tak samo jak aplikacja._, Przyk lad 10.1 Szczeg´olnym przypadkiem interpretacji jest interpretacja zbudowana z sa-mych term´ow. Niech M(λ) = hΛ/=_β, ·, [[ ]] i, gdzie [M ]_β · [N ]_β = [M N ]_β oraz [[M ]]v jest (z dok ladno´scia do =_{, β}) wynikiem jednoczesnego podstawienia termu v(x) na ka˙zda zmienn_, a_, wolna x termu M . Przez M_, ⁰(λ) oznaczymy analogiczna interpretacj_, e, kt´_, orej dziedzine tworz_, a_, klasy term´ow zamknietych. Podobnie M(λη) i M_, ⁰(λη) oznacza struktury w kt´orych zbi´or term´ow (odp. zbi´or kombinator´ow) podzielono przez =_βη. Wszystkie te struktury sa lambda-_, algebrami, ale M⁰(λ) i M⁰(λη) nie sa lambda-modelami._,

Nastepuj_, acy lemat m´_, owi o w lasno´sci, kt´orej oczekujemy od ka˙zdej sensownej semantyki.

Znaczenie podstawienia M [x := N ] powinno by´c takie samo jak znaczenie termu M przy odpowiednio zmienionym warto´sciowaniu.

Lemat 10.2 W dowolnym lambda-modelu zachodzi to˙zsamo´s´c [[M [x := N ]]]v = [[M ]]v[x7→[[N ]]v].

Dow´od: Udowodnimy najpierw, ˙ze teza zachodzi przy dodatkowym za lo˙zeniu x 6∈FV(N ).

Postepujemy przez indukcj_, e ze wzgl_, edu na M . Przypadki zmiennej i aplikacji s_, a latwe, niech_, wiec M = λy P , gdzie x 6= y 6∈_, FV(N ). Korzystajac ze s labej ekstensjonalno´_, sci udowodnimy r´owno´s´c [[λy. P [x := N ]]]v = [[λy P ]]v[x7→[[N ]]v]. Latwiej bedzie, je´_, sli po obu stronach r´ owna-nia wystapi to samo warto´_, sciowanie. Ale [[λy. P [x := N ]]]_v = [[λy. P [x := N ]]]v[x7→[[N ]]v], bo za lo˙zyli´smy, ˙ze x 6∈FV(N ).

Dla dowolnego a, korzystajac z za lo˙zenia indukcyjnego o termie P , dostaniemy teraz_, [[λy. P [x := N ]]]v[x7→[[N ]]v]· a = [[λy.P [x := N ]]]_v· a = [[P [x := N ]]]_v[y7→a] =

= [[P ]]v[y7→a][x7→[[N ]]v]= [[P ]]v[y7→a][x7→[[N ]]v]= [[λy. P ]]v[x7→[[N ]]v]· a.

Poniewa˙z mamy do czynienia z lambda-modelem, wiec z tego wynika_,

[[λy. P [x := N ]]]v = [[λy. P [x := N ]]]v[x7→[[N ]]v]= [[λy P ]]v[x7→[[N ]]v].

Niech teraz x ∈FV(N ). Ustalmy nowa zmienn_, a z (tj. tak_, a, ˙ze x 6= z 6∈_, FV(M ),FV(N )) i niech w = v[z 7→ [[N ]]v]. Wtedy z Wniosku 1.5 mamy M [x := N ] = M [x := z][z := N ], a poniewa˙z z 6∈FV(N ) i x 6∈FV(z), wiec z pierwszej cz_, e´_,sci wynika

[[M [x := N ]]]_v = [[M [x := z]]]_w = [[M ]]_{w[x7→[[z]]w]}= [[M ]]_{v[x7→[[z]]w]}= [[M ]]v[x7→[[N ]]v]. Przedostatnia r´owno´s´c bierze sie st_, ad, ˙ze z 6∈_, FV(M ).

Fakt 10.3 Ka˙zdy lambda-model jest lambda-algebra._,

Dow´od: Przez indukcje ze wzgl_, edu na definicj_, e beta-r´_, owno´sci pokazujemy ˙ze je´sli M =_β N , to [[M ]]_v = [[N ]]_v.

Najpierw zauwa˙zmy, ˙ze [[(λx.P )Q]]_v= [[λx.P ]]_v· [[Q]]_v = [[P ]]_{v[x7→[[Q]]v]}= [[P [x := Q]]]_v na mocy lematu 10.2.

Niech teraz M = λx.P i N = λx.Q, gdzie P =_β Q. Z za lo˙zenia indukcyjnego wynika, ˙ze [[P ]]_u = [[Q]]_u, przy ka˙zdym u, w szczeg´olno´sci gdy u = v[x 7→ a]. A zatem [[M ]]_v · a = [[P ]]_v[x7→a] = [[Q]]_v[x7→a]= [[N ]]v· a dla dowolnego a. Stad [[M ]]_, v= [[N ]]v.

Pozosta le przypadki sa rutynowe._,

Twierdzenie 10.4 (o pe lno´sci) Nastepuj_, ace warunki s_, a r´_, ownowa˙zne:

1) M =_β N ;

2) A |= M = N dla dowolnej lambda-algebry A;

3) A |= M = N dla dowolnego lambda-modelu A.

Dow´od: Implikacja (1) ⇒ (2) wynika wprost z definicji, a implikacja (2) ⇒ (3) z Lema-tu 10.3. Natomiast implikacja (3) ⇒ (1) wynika stad, ˙ze M(λ) jest lambda-modelem, a termy_, r´owne w M(λ) musza by´_, c β-r´owne (rozpatrzmy trywialne warto´sciowanie v(x) = x).

Modele cze´_,sciowo uporzadkowane_,

Na poczatek przypomnijmy kilka definicji. Niech hA, ≤i b_, edzie porz_, adkiem cz_, e´_,sciowym.

• Podzbi´or B zbioru A jest skierowany wtedy i tylko wtedy, gdy dla dowolnych a, b ∈ B istnieje takie c ∈ B, ˙ze a, b ≤ c.

• Zbi´or A jest zupe lnym porzadkiem cz_, e´_,sciowym (cpo) wtedy i tylko wtedy, gdy ka˙zdy jego skierowany podzbi´or ma kres g´orny.

Oczywi´scie ka˙zdy la´ncuch jest zbiorem skierowanym. W szczeg´olno´sci elementy dowolnego ciagu wst_, epuj_, acego a_{, 0} ≤ a₁ ≤ a₂ ≤ . . . tworza zbi´_, or skierowany. Tak˙ze zbi´or pusty jest zbiorem skierowanym. Z definicji porzadku zupe lnego wynika wi_, ec istnienie elementu naj-_, mniejszego sup ∅, tradycyjnie oznaczanego przez ⊥.

Niech teraz hA, ≤i i hB, ≤i bed_, a porz_, adkami cz_, e´_,sciowymi.

• Funkcja f : A → B jest monotoniczna wtedy i tylko wtedy, gdy dla dowolnych x, y ∈ A nier´owno´s´c x ≤ y implikuje f (x) ≤ f (y).

• Je´sli hA, ≤i i hB, ≤i sa zupe lnymi porz_, adkami cz_, e´_,sciowymi to funkcja f : A → B jest ciag la wtedy i tylko wtedy, gdy f zachowuje kresy g´_, orne niepustych zbior´ow skierowa-nych, tj. dla dowolnego skierowanego i niepustego podzbioru X ⊆ A istnieje sup f (X) i zachodzi r´owno´s´c f (sup X) = sup f (X).

Fakt 10.5 (´cwiczenie)

1) Ka˙zda funkcja ciag la jest monotoniczna._, 2) Z lo˙zenie funkcji ciag lych jest ci_, ag le._,

Zbi´or wszystkich funkcji ciag lych z A do B oznaczamy przez [A → B]. Ten zbi´_, or, uporzad-_, kowany warunkiem:

f ≤ g wtedy i tylko wtedy, gdy ∀a ∈ A(f (a) ≤ g(a)),

jest zupe lnym porzadkiem cz_, e´_,sciowym. Podobnie mo˙zna nada´c strukture cpo zbiorowi A × B_, za pomoca zwyk lego uporz_, adkowania_,

”po wsp´o lrzednych”:_,

ha, bi ≤ ha⁰, b⁰i wtedy i tylko wtedy, gdy a ≤ a⁰ i b ≤ b⁰. Lemat 10.6 Funkcja f : D₁ × D₂ → D jest ci

ag la wtedy i tylko wtedy gdy jest ci, ag la_, ze wzgledu na obie wsp´_, o lrzedne, tj. dla dowolnych a ∈ D_, 1 i b ∈ D2 oraz dowolnych skierowa-nych A ⊆ D1 i B ⊆ D2 zachodzi f (sup A, b) = sup f (A, b) oraz f (a, sup B) = sup f (a, B).

Dow´od: Implikacja z lewej do prawej jest oczywista. Dla dowodu implikacji odwrotnej rozpatrzmy niepusty skierowany zbi´or X ⊆ D₁× D₂ i niech A = π₁(X) oraz B = π₂(X).

Oczywi´scie X ⊆ A × B, chocia˙z niekoniecznie na odwr´ot. Ale je´sli ha, bi ∈ A × B, to zawsze istnieje takie ha⁰, b⁰i ∈ X, ˙ze ha, bi ≤ ha⁰, b⁰i. Istotnie, mamy wtedy pary ha, b⁰⁰i, ha⁰⁰, bi ∈ X.

Skoro zbi´or X jest skierowany, to ha, b⁰⁰i, ha⁰⁰, bi ≤ ha⁰, b⁰i dla pewnego ha⁰, b⁰i ∈ X. Porz adek,

jest po wsp´o lrzednych, wi_, ec ha, bi ≤ ha_, ⁰, b⁰i.

Nietrudno zauwa˙zy´c, ˙ze sup X = sup(A × B) = hsup A, sup Bi. Niech ha₀, b₀i bedzie tym_, kresem. Nale˙zy sprawdzi´c, ˙ze f (a₀, b₀) = sup f (X). Oczywi´scie f (a₀, b₀) ≥ sup f (X), przy-pu´s´cmy wiec, ˙ze c ≥ f (a, b) dla wszystkich (a, b) ∈ X. Wtedy tak˙ze c ≥ f (a, b) dla wszystkich_, (a, b) ∈ A × B. Je´sli ustalimy dowolne b ∈ B, to na mocy ciag lo´_, sci ze wzgledu na pierwsz_, a_, wsp´o lrzedn_, a, otrzymamy c ≥ f (a_{, 0}, b) = sup f (A, b). Dalej z ciag lo´_, sci ze wzgledu na drug_, a_, wsp´o lrzedn_, a wynika tak˙ze c ≥ f (a_, 0, b0).

Lemat 10.7 Operacja aplikacji Ap : D1×[D₁ → D₂] → D2, okre´slona przez Ap(d, f ) = f (d), jest funkcja ci_, ag l_, a._,

Dow´od: Na mocy lematu 10.6 wystarczy sprawdzi´c ciag lo´_, s´c ze wzgledu na wsp´_, o lrzedne._, Dla skierowanego A ⊆ D1 i ustalonego f mamy sup Ap(A, f ) = sup f (A) = f (sup A) = Ap(sup A, f ), bo f jest ciag la. A je´_, sli F ⊆ [D1 → D₂] jest skierowany oraz a ∈ D1 to sup Ap(a, F ) = sup{f (a) | f ∈ F } = (sup F )(a) = Ap(a, sup F ) z definicji sup F .

Lemat 10.8 Operacja abstrakcji Abs : [(D₁ × D₂) → D] → [D₁ → [D₂ → D]], dana przez Abs(f )(d)(e) = f (d, e), jest dobrze okre´slona i ciag la._,

Dow´od: Dla dowolnego d, funkcja Abs(f )(d) jest z lo˙zeniem funkcji ciag lej f z funkcj_, a_, ciag l_, a g(e) = hd, ei, zatem jest ci_, ag la._,

Dla A ⊆ D₁ mamy Abs(f )(sup A)(e) = f (sup A, e) = sup f (A, e) = sup Abs(f )(A)(e) czyli Abs(f )(sup A) = sup Abs(f )(A), co oznacza, ˙ze funkcja Abs(f ) jest ciag la._,

Wreszcie gdy F jest skierowanym podzbiorem [(D1 × D₂) → D], to Abs(sup F )(d)(e) = (sup F )(d, e) = sup{f (d, e) | f ∈ F } = sup{Abs(f )(d)(e) | f ∈ F } = sup Abs(F )(d)(e), czyli sama funkcja Abs te˙z jest ciag la._,

Refleksywne cpo

Kluczowa definicja jest taka. Zupe lny porzadek cz_, e´_,sciowy D jest refleksywny, gdy przestrze´n funkcyjna [D → D] jest retraktem D, tj. gdy istnieja przekszta lcenia ci_, ag le F : D → [D → D]_, i G : [D → D] → D, takie, ˙ze F ◦ G = id_[D→D]. Zauwa˙zmy, ˙ze wtedy [D → D] jest izomorficzne z pewnym podzbiorem D (obrazem funkcji G).

Na takim cpo mo˙zemy okre´sli´c lambda-interpretacje D = hD, ·, [[ ]] i, gdzie dla a, b ∈ D_, a · b = F (a)(b),

a znaczenie term´ow jest okre´slone tak:

• Je´sli x jest zmienna, to [[x]]_, v = v(x);

• [[P Q]]_v = [[P ]]_v· [[Q]]_v;

• [[λx.P ]]_v = G(ξ_P^v,x).

Powy˙zej, symbol ξ^v,x_P oznacza funkcje okre´_, slona r´_, ownaniem ξ_P^v,x(a) = [[P ]]_v[x7→a], kt´ora niefor-_, malnie mo˙zemy zapisa´c tak λλa.[[P ]]_v[x7→a].

Nietrudno zauwa˙zy´c, ˙ze wtedy zachodza nast_, epuj_, ace warunki:_,

• G(f ) · a = f (a), dla dowolnego f ∈ [D → D] i a ∈ D;

• [[λx.P ]]_v· a = [[P ]]_v[x7→a], dla dowolnego a ∈ D;

• Je´sli v|_{FV(P )}= u|_{FV(P )}, to [[P ]]v = [[P ]]u,

a zatem faktycznie mamy lambda-interpretacje. Nietrudno te˙z przeoczy´_, c pewien drobiazg:

poprawno´s´c powy˙zszej definicji nie jest wcale oczywista i wymaga dowodu. Operacja G jest bowiem okre´slona tylko dla funkcji ciag lych._,

Lemat 10.9 Dla dowolnych M i v, funkcja ξ_M^v,x (czyli λλa.[[M ]]_v[x7→a]) jest ciag la._,

Dow´od: Indukcja ze wzgledu na M . Dla M = P Q, funkcja ξ_{, M}^v,x = λλa.[[M ]]_v[x7→a] jest z lo˙zeniem postaci Ap ◦ h, gdzie funkcja h dana wzorem h(a) = hF (ξ_P^v,x(a)), ξ_Q^v,x(a)i jest ciag la. Je´_, sli M = λy N to z za lo˙zenia indukcyjnego funkcja f , kt´ora parze ha, bi przypisuje warto´s´c [[N ]]v[x7→a][y7→b] jest ciag la ze wzgl_, edu na obie wsp´_, o lrzedne, a zatem ci_, ag la, na mocy_, lematu 10.6. Natomiast funkcja ξ^v,x_M = λλa.G(λλb.[[N ]]v[x7→a][y7→b]) jest z lo˙zeniem G ◦ Abs(f ).

Twierdzenie 10.10 Je´sli D jest refleksywnym cpo, to lambda-interpretacja D = hD, ·, [[ ]] i jest lambda-modelem.

Dow´od: Pozostaje sprawdzi´c, ˙ze mamy s laba ekstensjonalno´_, s´c. Wystarczy w tym celu zauwa˙zy´c, ˙ze warunek [[λx.M ]]v≈ [[λx.N ]]_v implikuje ξ^v,x_M = ξ_N^v,x.

Fakt 10.11 Model jak wy˙zej jest ekstensjonalny wtedy i tylko wtedy, gdy G ◦ F = id_D. Cwiczenia´

1. Pokaza´c, ˙ze M⁰(λ), M(λ), M(λη) i M⁰(λη) sa lambda-algebrami._, 2. Pokaza´c, ˙ze M(λ) i M(λη) sa lambda-modelami._,

3. Znale´z´c w ksia˙zce Barendregta, ˙ze M_, ⁰(λ) ani M⁰(λη) nie sa lambda-modelami._,

4. (Meyer) Niech 1 = [[1]]. Pokaza´c, ˙ze lambda-algebra jest lambda-modelem wtedy i tylko wtedy, gdy z warunku a ≈ b wynika 1 · a = 1 · b.

5. Czy z tego, ˙ze A |= λx.M x = M dla wszystkich M wynika ekstensjonalno´s´c interpretacji A?

Inaczej: czy interpretacja βη-konwersji musi by´c ekstensjonalna? Wskaz´owka: U˙zy´c zadania 3.

6. Pokaza´c, ˙ze je´sli D jest refleksywnym cpo i f : D → D jest ciag la, to istnieje takie a ∈ D, ˙ze_, f (x) = a · x dla dowolnego x.

7. Czy funkcja odwrotna do ciag lej bijekcji musi by´_, c ciag la?_,

8. Je´sli FV(M ) = {x₁, ..., x_n}, to [[M ]] mo˙zna uwa˙za´c za funkcje z D_, ⁿdo D. Pokaza´c, ˙ze ta funkcja jest zawsze ciagla.

11 Model D

_∞

Skonstruujemy teraz konkretny przyk lad modelu — pewne refleksywne cpo, zwane modelem Scotta D∞. Zacznijmy od prostej definicji.

Niech A i B bed_, a cpo. Projekcj_, a z B na A nazywamy par_, e funkcji ci_, ag lych_, ϕ : A → B i ψ : B → A,

spe lniajac_, a warunki_,

ψ ◦ ϕ = id_A oraz ϕ ◦ ψ ≤ id_B.

Zauwa˙zmy, ˙ze wtedy ϕ(⊥A) = ⊥B, bo ϕ(⊥A) ≤ ϕ(ψ(⊥B)) ≤ ⊥B.⁸ Gdy mamy taka projekcj_, e,_, to w szczeg´olno´sci A jest retraktem B. Identyfikujac element d ∈ A z jego obrazem ϕ(d),_, mo˙zemy wtedy uwa˙za´c zbi´or A za podzbi´or B. Przyk ladem projekcji jest para funkcji

ϕ0 : D → [D → D] i ψ0 : [D → D] → D, okre´slona tak:

ϕ0(d)(a) = d, oraz ψ0(f ) = f (⊥)

dla dowolnych a, d ∈ D i f ∈ [D → D]. Mamy tu zanurzenie zbioru D w przestrze´n funkcyjna,_, przy kt´orym ka˙zdy element D jest uto˙zsamiany z funkcja sta l_, a._,

8Og´olniej: ϕ(x) to najmniejszy element y o w lasno´sci ψ(y) = x.

Je´sli mamy projekcje (ϕ, ψ) z B na A, to mo˙zemy_,

”podnie´s´c” te projekcj_, e na poziom funkcji,_, czyli okre´sli´c nowa projekcj_, e (ϕ_, ^∗, ψ^∗) z przestrzeni [B → B] na [A → A]. Dla f : A → A i g : B → B przyjmujemy

ϕ^∗(f ) = ϕ ◦ f ◦ ψ oraz ψ^∗(g) = ψ ◦ g ◦ ϕ, co ilustruje obrazek:

A ^{ϕ //}B A



ϕ //B

g



A

f

OO

ψ B

oo OO

A B

ψ

oo

Lemat 11.1 Je´sli (ϕ, ψ) jest projekcja z B na A, to para (ϕ_, ^∗, ψ^∗) jest projekcja z [B → B]_, na [A → A].

Dow´od: Cwiczenie.´

Przypu´s´cmy teraz, ˙ze mamy jakiekolwiek cpo D. Okre´slimy ciag zbior´_, ow Dn zaczynajac od_, D₀ = D i indukcyjnie przyjmujac D_{, n+1}= [D_n→ D_n]. Oczywi´scie wszystkie D_n sa cpo._, Dalej definiujemy przez indukcje ci_, ag projekcji (ϕ_{, n}, ψ_n) z D_n+1 na D_n, przyjmujac_,

(ϕn+1, ψn+1) = (ϕ^∗_n, ψ^∗_n).

Mamy wiec transmisj_, e w obie strony:_,

D₀−→ D^ϕ0 ₁−→ D^ϕ1 ₂ −→ · · ·^ϕ2 D₀←− D^ψ0 ₁←− D^ψ1 ₂ ←− · · ·^ψ2

Ka˙zdy ciag (x_{, n})_n∈N z lo˙zony z element´ow x_n ∈ D_n i spe lniajacy dla dowolnego n warunek_, xn= ψn(xn+1) nazywamy nicia. Tak wygl_, ada ni´_, c:

x₀←− x^ψ0 ₁←− x^ψ1 ₂←− · · ·^ψ2 Dla nici stosujemy notacje x = (x_, n)_n∈N.

Zbi´or wszystkich nici oznaczamy przez D∞. Mo˙zna go uporzadkowa´_, c po wsp´o lrzednych:_, x ≤ y wtedy i tylko wtedy, gdy ∀n ∈ N(xn≤ y_n).

Lemat 11.2 Zbi´or D∞ jest zupe lnym porzadkiem cz_, e´_,sciowym.

Dow´od: Je´sli X ⊆ D∞ jest skierowany, to ka˙zdy ze zbior´ow Xn = {xn | x ∈ X} jest skierowany, zatem istnieja kresy y_{, n}= sup X_n. Wtedy dla dowolnego n:

ψ_n(y_n+1) = ψ_n(sup X_n+1) = sup ψ_n(X_n+1) = sup X_n= y_n,

bo funkcja ψ_n jest ciag la oraz ψ_{, n}(X_n+1) = X_n. A zatem ciag y = (y_{, n})_n∈N jest nicia (nale˙zy_, do D∞). Pozostaje latwe sprawdzenie, ˙ze y = sup X.

Dla dowolnych n ≤ m, mamy oczywi´scie projekcje (ϕ_, nm, ψnm) z Dm na Dn, czyli z lo˙zenie ϕnm = ϕm−1◦ · · · ◦ ϕ_n, ψnm= ψn◦ · · · ◦ ψ_m−1.

Lemat 11.3 Dla n ≤ m zachodzi ϕ^∗_nm= ϕn+1,m+1 oraz ψ^∗_nm= ψn+1,m+1. Mo˙zna te˙z okre´sli´c projekcje (ϕn∞, ψn∞) z D∞ na Dn. Dla x ∈ Dn i y ∈ D∞:

(ϕn∞(x))i =







ψ_in(x), gdy i < n;

x, gdy i = n;

ϕni(x), gdy i > n.

ψn∞(y) = yn. Od tej pory mo˙zemy uwa˙za´c, ˙ze zachodza inkluzje_,

D₀ ⊆ D₁ ⊆ D₂⊆ · · · ⊆ D_∞,

zadane przez powy˙zsze projekcje. W szczeg´olno´sci ka˙zdy element x ∈ D_nuto˙zsamiamy z nicia_, prawie wszedzie r´_, owna x:_,

x₀ ←− x^ψ0 ₁ ←− x^ψ1 ₂ ←− · · ·^{ψ2 ψ}←− xⁿ⁻² _n−1 ^ψ←− xⁿ⁻¹ ←− x^{ψn ψ}←− x^{n+1 ψ}←− · · ·ⁿ⁺²

bo przecie˙z x uwa˙zamy za element wszystkich D_m dla m ≥ n. Zauwa˙zmy, ˙ze mamy tu nier´owno´sci x0 ≤ x₁ ≤ x₂≤ · · · ≤ x_n−1≤ x_n= x.

Lemat 11.4

1. Ka˙zda ni´c x jest ciagiem wst_, epuj_, acym (x_{, 0} ≤ x₁≤ x₂≤ . . .) i przy tym x = sup x_n; 2. Najmniejszy element jest zawsze ten sam: ⊥_D0 = ⊥_Dn = ⊥_D∞.

Dow´od: Cwiczenie.´

Lemat 11.5 Aplikacja w D∞ okre´slona wzorem

x · y = sup{xn+1(yn) | n ∈ N}

jest operacja ci_, ag l_, a._,

Dow´od: Najpierw trzeba pokaza´c, ˙ze kres istnieje, elementy x_n+1(y_n) ∈ D_n nie musza_, bowiem tworzy´c nici. Jest to jednak ciag wst_, epuj_, acy, co wynika z takich zwi_, azk´_, ow pomiedzy_, elementami zbioru Dn:

ϕ_n−1(x_n(y_n−1)) = ϕ_n−1(ψ_n−1(x_n+1(ϕ_n−1(y_n−1))) ≤

xn+1(ϕn−1(yn−1)) = xn+1(ϕn−1(ψn−1(yn))) ≤ xn+1(yn).

Dow´od ciag lo´_, sci korzysta z lematu 10.6. Ciag lo´_, s´c ze wzgledu na x liczymy tak: Z jednej_, strony sup_x∈Xx · y = sup_x∈Xsup_n∈Nx_n+1(y_n), a z drugiej strony

(sup X) · y = sup_n∈N(sup X)_n+1(y_n) = sup_n∈N(sup X_n+1)(y_n) = sup_n∈Nsup_x∈Xx_n+1(y_n), gdzie Xn+1 = {xn+1 | x ∈ X}. A przecie˙z to jest to samo. Ciag lo´_, s´c ze wzgledu na y jest_, nawet latwiejsza. Mamy bowiem x · sup Y = sup_n(x_n+1(sup Y )) = sup_nsup_yx_n+1(y) oraz sup(x · Y ) = sup_ysup_nx_n+1(y).

Teraz troche o tym, jak dzia la aplikacja._, Lemat 11.6

1. Je´sli x ∈ D_n+1, to x · y = x(y_n), a je´sli dodatkowo y ∈ D_n, to x · y = x(y);

2. Je´sli y ∈ Dn to (x · y)n= xn+1(y).

3. Zawsze (x · ⊥)₀ = x₀.

4. Je´sli x ∈ D0, to x · y = x = x · ⊥.

Dow´od: 1. W cze´_,sci pierwszej nale˙zy pokaza´c, ˙ze x · y = sup_mxm+1(ym) = xn+1(yn).

W tym celu zauwa˙zmy, ˙ze dla m < n mamy

x_m+1(y_m) = ψ_m+1,n+1(x)(ψ_mn(y)) = ψ_mn^∗ (x_n+1)(ψ_mn(y_n)) ≤ ψ_mn(x_n+1(y_n)), bo xn+1= x, yn= y, oraz ψ^∗_mn(xn+1) = ψmn◦ x_n+1◦ ϕ_mn. Natomiast dla m ≥ n

x_m+1(y_m) = ϕ_n+1,m+1(x)(y_m) = ϕ^∗_nm(x)(y_m) = (ϕ_n,m◦ x ◦ ψ_n,m)(y_m) = ϕ_n,m(x(y_n)) bo ϕ^∗_nm(x) = ϕ_nm◦ x ◦ ψ_nm oraz ψ_n,m(y_m) = y_n.

2. W cze´_,sci drugiej, dla dowolnego i ≥ n mamy yi+1= ϕ(yi), wiec x_, i+1(yi) = ψi(xi+2(yi+1)), co implikuje (xi+2(yi+1))n= (xi+1(yi))n= xn+1(y). A wszystko to wida´c na takim obrazku:

y_i∈ D_i ^{oo ψ}_ϕⁱ

i

//

xi+1



y_i+1∈ D_i+1

xi+2



Dn Di

ψni

oo oo ^ψi Di+1

3. Cze´_,s´c trzecia wynika z drugiej, dla y = ⊥ ∈ D0, a cze´_,s´c czwarta wprost z definicji.

Lemat 11.7 Aplikacja w D∞ jest ekstensjonalna: je´sli x · z = y · z zachodzi dla dowolnego z, to elementy x i y sa r´_, owne.

Dow´od: W istocie zachodzi implikacja

je´sli ∀z ∈ D∞(x · z ≤ y · z), to x ≤ y.

Nier´owno´s´c x₀ ≤ y₀ wynika z lematu 11.6(3), bo mamy x · ⊥ ≤ y · ⊥. Dalej, z lematu 11.6(2),

x_n+1(z) = (x · z)_n≤ (y · z)_n= y_n+1(z), dla dowolnego n i dowolnego z ∈ Dn, a wiec x_, n+1≤ y_n+1.

Lemat 11.8 Niech f ∈ Dn+1 i g ∈ Dn+2 bed_, a takie, ˙ze ϕ_, n(f (a)) ≤ g(ϕn(a)) dla a ∈ Dn. Wtedy f ≤ g w zbiorze D∞.

Dow´od: Nale˙zy sprawdzi´c, jakie nici wyznaczaja f i g. Poniewa˙z ϕ_{, n}(f (a)) ≤ g(ϕ_n(a)) wiec f (a) = ψ_, n(ϕn(f (a))) ≤ ψn(g(ϕn(a)) = ψn+1(g)(a), czyli f ≤ ψn+1(g) w zbiorze Dn+1. Inaczej m´owiac (f )_{, n+1} ≤ (g)_n+1, a reszta wynika z monotoniczno´sci funkcji ϕ_i i ψ_i.

Twierdzenie 11.9 Zbi´or D∞ jest refleksywnym cpo, co wiecej, jest on izomorficzny z prze-_, strzenia funkcyjn_, a [D_, ∞→ D∞].

Dow´od: Funkcja F : D∞→ [D_∞→ D_∞] jest okre´slona w oczywisty spos´ob:

F (x)(y) = x · y.

Z lemat´ow 11.5 i 11.7 wynika, ˙ze F jest ciag la i r´_, o˙znowarto´sciowa. Aby sprawdzi´c, ˙ze jest to surjekcja, we´zmy dowolna funkcj_, e f ∈ [D_, ∞ → D∞] i niech f⁽ⁿ⁾ : Dn → D_n bedzie jej_,

”aproksymacja” do D_, n, tj. niech f⁽ⁿ⁾(y) = f (y)n dla y ∈ Dn.

Ciag f_, ⁽ⁿ⁾nie musi by´c nicia, ale jest wst_, epuj_, acy. Istotnie, zauwa˙zmy ˙ze elementy y ∈ D_{, n}oraz ϕn(y) ∈ Dn+1 wyznaczaja t_, e sam_, a ni´_, c, zatem z punktu widzenia D∞ sa po prostu r´_, owne.

A wiec f (y) = f (ϕ_, n(y)) w D∞skad f_, ⁽ⁿ⁾(y) = f (y)n≤ f (ϕ_n(y))n+1= f⁽ⁿ⁺¹⁾(ϕn(y)) zachodzi dla y ∈ D_n. ´Sci´slej, mamy nier´owno´s´c ϕ_n(f⁽ⁿ⁾(y)) ≤ f⁽ⁿ⁺¹⁾(ϕ_n(y)) pomiedzy elementami_, zbioru Dn+1, co na mocy lematu 11.8 oznacza f⁽ⁿ⁾≤ f⁽ⁿ⁺¹⁾.

Skoro ciag f_, ⁽ⁿ⁾ jest wstepuj_, acy, to ma kres a = sup_{, n}f⁽ⁿ⁾. Trzeba teraz sprawdzi´c, ˙ze F (a) = f . We´zmy dowolne y ∈ D∞. Poniewa˙z ciagi f_, ⁽ⁿ⁾ i y_n sa wst_, epuj_, ace, wi_, ec_,

F (a)(y) = a · y = (sup_nf⁽ⁿ⁾) · y = sup_n(f⁽ⁿ⁾· y) = sup_nf⁽ⁿ⁾(y_n) = sup_nf (y_n)_n= f (y) Je´sli f, g ∈ [D∞→ D_∞] oraz f ≤ g to oczywi´scie tak˙ze sup_nf⁽ⁿ⁾≤ sup_ng⁽ⁿ⁾. Oznacza to, ˙ze funkcja G : [D∞ → D_∞] → D∞, odwrotna do F jest monotoniczna. A zatem funkcja F jest izomorfizmem porzadk´_, ow, w szczeg´olno´sci F i G sa ci_, ag le._,

Wniosek 11.10 Zbi´or D∞ wyznacza ekstensjonalny lambda-model D∞= hD∞, ·, [[ ]]i.

Twierdzenie 11.11 (Hyland, Wadsworth) Termy M i N sa obserwacyjnie r´_, ownowa˙zne wtedy i tylko wtedy, gdy D∞|= M = N .

Dow´od: Mo˙zna go znale´z´c w ksia˙zce Barendregta._,

Cwiczenia´

1. Uzupe lni´c szczeg´o ly dowod´ow.

2. Jakie nici sa interpretacjami term´_, ow K, ω, itd. w modelu D∞?

2. Jakie nici sa interpretacjami term´_, ow K, ω, itd. w modelu D∞?

W dokumencie 1 Sk ladnia rachunku lambda (Stron 35-51)