Przez logike drugiego rz, edu zazwyczaj rozumie si, e system powsta ly przez rozszerzenie ra-, chunku predykat´ow (logiki pierwszego rzedu) o kwantyfikatory przebiegaj, ace zbiory i relacje., Z konstruktywnego punktu widzenia, celowo´s´c takiego rozszerzenia jest watpliwa. Interpre-, tacja BHK nadaje bowiem taki sens kwantyfikatorowi og´olnemu:
Konstrukcja (dowodem) formu ly ∀R W (R) jest metoda przekszta lcenia dowolnego, znaczenia R zmiennej R w konstrukcje stwierdzenia W (R).,
Aby jednak wykona´c konstrukcje dla W (R) trzeba na og´, o l zna´c sam zbi´or R, tj. umie´c go zdefiniowa´c, a to nie zawsze jest mo˙zliwe, bo ka˙zda niesko´nczona dziedzina ma nieprzeliczalnie wiele podzbior´ow. Dlatego konstruktywne rozumienie kwantyfikatora drugiego rzedu jest inne:, zmienna relacyjna przebiega predykaty definiowalne formu lami. W intuicjonistycznej logice drugiego rzedu przyjmuje si, e wi, ec (z grubsza, 24) takie regu ly:
Γ ` ∀X ϕ(X) Γ ` ϕ(σ)
Γ ` ϕ(X) Γ ` ∀X ϕ(X)
(X nie ma w Γ)
Uwaga: Systemy klasycznej logiki drugiego rzedu, w kt´, orych kwantyfikatory przebiegaja, dowolne zbiory, nie sa efektywnie aksjomatyzowalne. Tak nie jest w przypadku intuicjonistycz-, nej logiki drugiego rzedu, kt´, ora jest aksjomatyzowalna i dlatego rekurencyjnie przeliczalna.
Jak powiedzieli´smy, w logice drugiego rzedu obok kwantyfikator´, ow relacyjnych wystepuj, a, tak˙ze elementy zwyk lego rachunku predykat´ow: wyra˙zenia i kwantyfikatory indywiduowe.
Okazuje sie jednak, ˙ze te ostatnie nie zawsze s, a istotne, a wiele w lasno´, sci logiki drugiego rzedu mo˙zna bada´, c w oderwaniu od jej aspektu indywiduowego. Je˙zeli w formu lach rachunku predykat´ow drugiego rzedu zaniedba´, c wszystko to, co odnosi sie do indywidu´, ow, to otrzy-mamy formu ly zdaniowe z kwantyfikatorami. Na przyk lad rozpatrzmy formu le N (x), kt´, ora definiuje liczby naturalne:
∀R(∀z(R(z) → R(sz)) → R(0) → R(x))
Usuniecie z niej informacji o indywiduach daje kwantyfikowan, a formu l, e zdaniow, a:,
∀R((R → R) → R → R),
w kt´orej jednoargumentowa zmienna relacyjna R zosta la zastapiona zmienn, a zdaniow, a. W po-, dobny spos´ob mo˙zna ka˙zda formu l, e przekszta lci´, c w formu le zdaniow, a z kwantyfikatorami., Okazuje sie, ˙ze ten zabieg, znacznie upraszczaj, ac sk ladni, e, nie zmienia wielu istotnych w las-, no´sci naszej logiki.
Zdaniowa logika drugiego rzedu,
Na razie zatem bedziemy si, e zajmowa´, c tylko zdaniowa logik, a drugiego rz, edu, i to wy l, acz-, nie fragmentem implikacyjno-uniwersalnym. Zaczynamy od sk ladni. Formu lami nazywamy zmienne zdaniowe p, q, r, . . . i wyra˙zenia (σ → τ ), ∀p σ, gdzie σ i τ sa formu lami. Przez, FVT(ϕ) oznaczamy zbi´or zmiennych zdaniowych wystepuj, acych wolno w formule ϕ. Definiujemy go, tak: FVT(p) = {p}, FVT(σ → τ ) = FVT(σ) ∪FVT(τ ), oraz FVT(∀p σ) = FVT(σ) − {p}.
Podstawienie formu ly σ do formu ly ϕ w miejsce wolnych wystapie´, n zmiennej p oznaczamy przez ϕ[p := σ] (lub przez ϕ[σ/p]). Podstawienie jest definiowane przez indukcje:,
• p[p := σ] = σ oraz q[p := σ] = q;
• (ψ → τ )[p := σ] = ψ[p := σ] → τ [p := σ];
• (∀p ψ)[p := σ] = ∀p ψ;
24Pomijamy tu ´scis la definicj, e wyra˙zenia ϕ(σ).,
• (∀q ψ)[p := σ] = ∀q ψ[p := σ], gdy q 6∈FVT(σ);
Uto˙zsamiamy (alfa-konwersja) formu ly r´o˙zniace si, e tylko wyborem zmiennych zwi, azanych., Regu ly naturalnej dedukcji dla naszej logiki sa takie:,
(Ax) Γ, ϕ ` ϕ (→ I) Γ, ϕ ` ψ
Γ ` ϕ → ψ
(→ E) Γ ` ϕ → ψ Γ ` ϕ Γ ` ψ (∀I) Γ ` ϕ
Γ ` ∀p ϕ
(p 6∈FVT(Γ)) (∀E) Γ ` ∀p ϕ Γ ` ϕ[p := ϑ]
Uwaga: Znaczeniem zmiennej zdaniowej mo˙ze by´c dowolna formu la, zob. regu le (∀E). T, e, w lasno´s´c czasem nazywa sie full comprehension. Znaczenie formu ly ϕ = ∀p ψ jest wyznaczo-, ne przez wszystkie mo˙zliwe podstawienia ψ[p := σ]. Ale poniewa˙z w roli σ mo˙ze wystapi´, c samo ϕ, wiec znaczenie formu ly w spos´, ob uwik lany zale˙zy od niej samej. Inaczej m´owiac,, nasza logika jest impredykatywna. Konsekwencja tej w lasno´, sci jest utrudnione definiowanie i dowodzenie w lasno´sci przez zwyk la indukcj, e ze wzgl, edu na,
”budowe formu ly”.,
Twierdzenie 22.1 (L¨ob, Gabbay/Sobolew) Intuicjonistyczna logika zdaniowa drugiego rzedu jest nierozstrzygalna (nierozstrzygalne jest pytanie czy dana formu la jest twierdzeniem)., Powy˙zszy wynik kontrastuje ze znanym twierdzeniem z teorii z lo˙zono´sci: klasyczna logika kwantyfikowanych formu l boole’owskich jest PSPACE-zupe lna. Zauwa˙zmy jednak, ˙ze w logice klasycznej, opartej na zerojedynkowej semantyce, ka˙zdy kwantyfikator mo˙zna wyeliminowa´c (kosztem wyk ladniczego wyd lu˙zenia formu ly). Klasyczny rachunek zda´n jest funkcjonalnie zupe lny: ka˙zda funkcj, e zerojedynkow, a mo˙zna zdefiniowa´, c formu la. W przypadku intuicjonis-, tycznym tak nie jest. Na przyk lad formu ly p → ∀q(q ∨ ¬q) i ¬¬p → ∃q((p → ¬q ∨ q) → p) nie sa r´, ownowa˙zne ˙zadnej formule zdaniowej ϕ(p) bez kwantyfikator´ow.
Cwiczenia´
1. Pokaza´c, ˙ze formu la ∀p(q ∨ ¬p) → q ∨ ∀p ¬p jest twierdzeniem zdaniowej logiki intuicjonistycznej drugiego rzedu (regu ly dla alternatywy s, a takie same jak zwykle)., Czy ka˙zda formu la postaci
∀p(q ∨ ϕ(p)) → q ∨ ∀p ϕ(p) bedzie twierdzeniem?,
2. Pokaza´c, ˙ze formu la ∀r((p → r) → (q → r) → r) jest w zdaniowej logice intuicjonistycznej drugiego rzedu r´, ownowa˙zna alternatywie p ∨ q.
3. Jak zdefiniowa´c regu ly naturalnej dedukcji dla zdaniowego kwantyfikatora szczeg´o lowego?
23 System F
Zgodnie z interpretacja BHK, konstrukcj, a dla ∀p ϕ jest metoda, kt´, ora dla dowolnej formu ly σ pozwala otrzyma´c konstrukcje dla ϕ[p := σ]. Taka konstrukcja jest wi, ec funkcj, a okre´, slona,
na zbiorze formu l, ktora dla ka˙zdego σ przyjmuje warto´s´c ze zbioru konstrukcji ϕ[p := σ].
Zbi´or takich konstrukcji odpowiada (nieformalnie) produktowi Πp∈Propϕ[p := σ]. Je´sli wiec, uto˙zsamia´c formu ly i typy to formu la uniwersalna jest typem produktowym. Patrzac na to, z innej strony, mo˙zemy powiedzie´c, ˙ze term typu ∀p ϕ reprezentuje procedure polimorficzn, a, z (formalnym) parametrem typowym p. Przekazanie do takiej procedury parametru aktual-nego σ ustala typ bie˙zacej aktywacji jako ϕ[p := σ].,
System rachunku lambda, w kt´orym typy sa formu lami zdaniowymi drugiego rz, edu nazy-, wamy polimorficznym rachunkiem lambda, rachunkiem lambda drugiego rzedu, polimorficz-, nym rachunkiem lambda drugiego rzedu lub systemem F. Poni˙zsze regu ly s, a zar´, owno regu lami przypisania typ´ow, jak te˙z definicja sk ladni. Wyra˙zenie Γ ` M : σ czytamy,
”w otoczeniu Γ term M ma typ σ”, gdzie otoczenie jest rozumiane jak zwykle. Przez FVT(Γ) oznaczamy sume, S{FVT(γ) | (x : γ) ∈ Γ, dla pewnego x}.
(Var) Γ(x : ϕ) ` x : ϕ (Abs) Γ(x : ϕ) ` M : ψ
Γ ` (λx:ϕ M ) : ϕ → ψ
(App) Γ ` M : ϕ → ψ Γ ` N : ϕ Γ ` (M N ) : ψ (Gen) Γ ` M : ϕ
Γ ` (Λp M ) : ∀p ϕ
(p 6∈FVT(Γ)) (Inst) Γ ` M : ∀p ϕ Γ ` M σ : ϕ[p := σ]
Sk ladnie systemu F zdefiniowali´, smy w stylu Churcha, tj. tak, ˙ze typy stanowia integraln, a, cze´,s´c term´ow. Przy ustalonym otoczeniu, deklarujacym typy zmiennych wolnych, ka˙zdy term, ma dok ladnie jeden typ, kt´ory mo˙zna bez trudu ustali´c.
W termach moga wyst, epowa´, c zar´owno zmienne przedmiotowe jak typowe (zdaniowe). Ope-ratorami wia˙z, acymi zmienne s, a obie lambdy i kwantyfikator wyst, epuj, acy w typach. Symbol, FVT( ) odnosi sie do zmiennych wolnych zdaniowych, a symbol, FV do zmiennych wolnych przedmiotowych. Definicje sa indukcyjne:,
• FV(x) = {x};
• FV(λx:ϕ M ) =FV(M ) − {x};
• FV(M N ) =FV(M ) ∪FV(N );
• FV(Λp M ) =FV(M );
• FV(M σ) =FV(M );
• FVT(x) = ∅;
• FVT(λx:ϕ M ) =FVT(ϕ) ∪FVT(M );
• FVT(M N ) =FVT(M ) ∪FVT(N );
• FVT(Λp M ) =FVT(M ) − {p};
• FVT(M σ) =FVT(M ) ∪FVT(σ).
Operacja podstawienia wystepuje w dw´, och wersjach: podstawienie typu (formu ly) za zmienna, typowa (zdaniow, a) i podstawienie termu za zmienn, a przedmiotow, a. Definiujemy je, zak lada-, jac, ˙ze zmienne zwi, azane s, a tak dobrane, aby nie dosz lo do konfuzji, tj. stosujemy w razie, potrzeby domy´slna wymian, e zmiennej zwi, azanej.,
• x[x := P ] = P oraz y[x := P ] = y;
• (M N )[x := P ] = M [x := P ]N [x := P ];
• (λx:ϕ M )[x := P ] = λx:ϕ M ;
• (λy:ϕ M )[x := P ] = λy:ϕ. M [x := P ], gdzie y 6∈FV(P );
• (M τ )[x := P ] = M [x := P ]τ ;
• (Λp M )[x := P ] = Λp M [x := P ], gdzie p 6∈FVT(P );
• x[p := σ] = x;
• (M N )[p := σ] = M [p := σ]N [p := σ];
• (λx:ϕ M )[p := σ] = λx:ϕ[p := σ]. M [p := σ];
• (M τ )[p := σ] = M [p := σ]τ [p := σ];
• (Λp M )[p := σ] = Λp M ;
• (Λq M )[p := σ] = Λq M [p := σ], gdzie q 6∈FVT(σ).
Przez Γ[p := σ] oznaczymy otoczenie Γ, w kt´orym ka˙zda deklaracja (x : τ ) zosta la zastapiona, przez (x : τ [p := σ]).
Lemat 23.1
(1) Je´sli Γ ` M : ϕ, to Γ[p := σ] ` M [p := σ] : ϕ[p := σ].
(2) Je´sli Γ, x : τ ` M : ϕ oraz Γ ` P : τ to Γ ` M [x := P ] : ϕ.
Dow´od: Indukcja ze wzgledu na budow, e M . Cz, e´,s´c (2) wymaga lematu podobnego do lematu 13.1.
Poni˙zej mamy kilka przyk lad´ow term´ow i ich typ´ow (zamiast λx : τ piszemy czesto λx, τ):
• ` Λqλx∀p(p→p). x(q → q)(xq) : ∀q(∀p(p → p) → q → q);
• ` Λp.λfp→pλxp.f (f x) : ∀p((p → p) → (p → p));
• ` λf∀p(p→q→p)Λpλxp.f (q→p)(f px) : ∀p(p → q → p) → ∀p(p → q → q → p).
Twierdzenie 23.2 Dla dowolnego typu τ nastepuj, ace warunki s, a r´, ownowa˙zne:
1) Istnieje term zamkniety typu τ ;,
2) Formu la τ jest twierdzeniem intuicjonistycznej logiki zdaniowej drugiego rzedu.,
Dow´od: Oczywiste.
Definicja 23.3 Przez beta redukcje w systemie F rozumiemy najmniejsz, a relacj, e →, βw zbio-rze term´ow zawierajac, a:,
• (λx:τ.M )N −→β M [x := N ];
• (Λα.M )τ −→β M [α := τ ],
i zamkniet, a ze wzgl, edu na konteksty, tj. M →, β N implikuje M P →β N P , P M →β P N , λx:τ.M →β λx:τ.N , Λp M →β Λp N oraz M τ →β N τ , o ile odpowiednie wyra˙zenia sa, poprawnymi termami.
Jak zwykle w takich przypadkach, symbol βoznacza domkniecie przechodnio-zwrotne relacji, redukcji →β. Indeksβ czesto jest pomijany. Najwa˙zniejsze w lasno´, sci redukcji sa takie:,
Twierdzenie 23.4
1) Je´sli Γ ` M : τ oraz M β N to Γ ` N : τ .
2) W lasno´s´c Churcha-Rossera: Je˙zeli M β N1 oraz M β N2 to N1 β P i N2 β P , dla pewnego P .
3) Silna normalizacja: Nie istnieje niesko´nczony ciag redukcji rozpoczynaj, acy si, e od jakie-, gokolwiek (poprawnego) termu.
Dow´od: Cze´,s´c (1) wynika z lematu 23.1. Cze´,sci (2) i (3) zostawiamy na razie bez dowodu.
Uwaga: Dla term´ow systemu F mo˙zna te˙z rozwa˙za´c relacje eta-redukcji, zadan, a regu lami:,
• λx:τ.M x −→β M (gdy x 6∈FV(M ));
• Λp.M p −→β M (gdy p 6∈FVT(M )).
Liczby naturalne
Niech ω = ∀p((p → p) → (p → p)). Liczby naturalne sa reprezentowane przez termy, zamkniete typu ω.,
n = Λpλf : (p → p)λx : p.f (f (· · · f (x))) Na przyk lad 2 = Λp.λfp→pxp.f (f x).
M´owimy, ˙ze funkcja f : Nk → N jest definiowalna w systemie F, gdy istnieje taki term M : ωk→ ω, ˙ze dla dowolnych n1, · · · nk zachodzi M n1. . . nkβ f (n1, . . . , nk).
Na przyk lad dodawanie, mno˙zenie i potegowanie definiujemy tak:,
• Add = λmn.Λp.λf x.mpf (npf x);
• Mult = λmn.Λp.λf x.mp(npf )x;
• Exp = λmn.Λp.λf x.m(p → p)(np)f x.
Mo˙zna te˙z zdefiniowa´c poprzednik i to typu ω → ω. A wiec odejmowanie i r´, owno´s´c te˙z sa, definiowalne (por. wniosek 17.14).
Sp´ojniki zdaniowe
W logice zdaniowej drugiego rzedu fa lsz mo˙zna zdefiniowa´, c tak:
⊥ = ∀p p
Nietrudno zauwa˙zy´c, ˙ze z fa lszu wszystko wynika. Je´sli M : ⊥, to M τ : τ .
Mo˙zna te˙z zdefiniowa´c pozosta le sp´ojniki zdaniowe. Przypomnijmy odpowiednie regu ly natu-ralnej dedukcji wraz z przypisaniem term´ow:
Koniunkcja: Γ ` M : ϕ Γ ` N : ψ
Γ ` hM, N i : ϕ ∧ ψ (I∧) Γ ` M : ϕ ∧ ψ
Γ ` π1(M ) : ϕ (E∧) Γ ` M : ϕ ∧ ψ Γ ` π2(M ) : ψ
Alternatywa: Γ ` M : ϕ
Γ ` inlϕ∨ψ(M ) : ϕ ∨ ψ (I∨) Γ ` M : ψ Γ ` inrϕ∨ψ(M ) : ϕ ∨ ψ Γ ` M : ϕ ∨ ψ Γ(x : ϕ) ` P : ϑ Γ(y : ψ) ` Q : ϑ
Γ ` case M of [x]P, [y]Q : ϑ (E∨) Redukcje zwiazane z koniunkcj, a i alternatyw, a s, a nast, epuj, ace:,
π1(hM, N i) → M , π2(hM, N i) → N ;
case inl(P ) of [x]M, [y]N → M [x := P ];
case inr(Q) of [x]M, [y]N → N [y := Q].
Definicje alternatywy w systemie F otrzymamy, je´, sli spr´obujemy wyrazi´c w logice drugiego rzedu poj, ecie sumy jako najmniejszego zbioru zawieraj, acego oba sk ladniki:,
x ∈ A ∪ B ⇔ ∀P (A ⊆ P → B ⊆ P → x ∈ P ), lub inaczej:
(A ∪ B)(x) ⇔ ∀P (∀y(A(y) → P (y)) → ∀y(B(y) → P (y)) → P (x)).
Po usunieciu informacji o indywiduach otrzymujemy definicj, e alternatywy:, σ ∨ τ = ∀p((σ → p) → (τ → p) → p),
gdzie zmienna p jest nowa, tj. p 6∈FVT(σ) ∪FVT(τ ). Pozostaje sprawdzi´c, ˙ze nasza definicja jest dobra. Wystarczy w tym celu zdefiniowa´c inl, inr i case w taki spos´ob, ˙zeby regu ly (I∨) i (E∨) by ly poprawne. Robimy to tak:
• inlσ∨τM = Λpλuσ→pλvτ →p.uM ;
• inrσ∨τM = Λpλuσ→pλvτ →p.vM ;
• case M of [x]Pϑ, [y]Qϑ= M ϑ(λxσ.P )(λyτQ).
Nietrudno sprawdzi´c, ˙ze typowanie jest poprawne, co w szczeg´olno´sci oznacza, ˙ze nasza defini-cja spe lnia regu ly wnioskowania dla alternatywy. W istocie spe lniony jest silniejszy warunek:
tak˙ze redukcje sa zgodne z oczekiwaniami, chocia˙z mog, a wymaga´, c wiecej ni˙z jednego kroku:, case inl(P ) of [x]M, [y]N M [x := P ];
case inr(Q) of [x]M, [y]N N [y := Q].
Koniunkcje definiujemy tak:,
σ ∧ τ = ∀p((σ → τ → p) → p), gdzie zmienna p jest nowa (patrz wy˙zej), a pare i rzuty tak:,
• hM, N i = Λpλyσ→τ →p.yM N ;
• Π1(M ) = M σ(λxσλyτ.x);
• Π2(M ) = M τ (λxσλyτ.y).
Definicja koniunkcji jest wzorowana na r´ownowa˙zno´sci:
x ∈ A ∩ B ⇔ ∀P (∀y(y ∈ A → y ∈ B → y ∈ P ) → x ∈ P ).
Latwo widzie´c, ˙ze ta definicja spe lnia zar´owno regu ly typowania jak i redukcji.
Kwantyfikator szczeg´o lowy
Zdaniowy kwantyfikator szczeg´o lowy drugiego rzedu ma takie regu ly naturalnej dedukcji:,
(∃I) Γ ` σ[p := τ ] Γ ` ∃p. σ
(∃E) Γ ` ∃p. σ Γ ` ρ
Γ, σ ` ρ (p 6∈FVT(Γ) ∪FVT(ρ))
Interpretujemy go tak: typ ∃p. σ jest typem abstrakcyjnym, w kt´orym zmienna p reprezentuje typ prywatny. Na przyk lad, je´sli
stos(p) = p × (p → p) × (p → ω) × (ω × p → p),
to typ ∃p stos(p) jest abstrakcyjnym typem struktury stosowej, w kt´orej mamy stos pusty jako sta la oraz operacje pop, top i push.),
Operacja pack tworzy obiekt typu abstrakcyjnego ukrywajac prywatn, a cz, e´,s´c typu:
(pack) Γ ` M : σ[p := τ ] Γ ` pack M, τ to ∃p. σ : ∃p. σ
Taki obiekt mo˙ze by´c u˙zyty tam, gdzie implementacja typu prywatnego nie ma znaczenia:
(unpack) Γ ` M : ∃p. σ Γ(x : σ) ` N : ρ Γ ` let M be x, p in N : ρ
(p 6∈FVT(Γ) ∪FVT(ρ))
Nastepuj, aca regu la redukcji m´, owi o tym, co sie wtedy dzieje:,
let (pack M, τ to ∃p. σ) be x, p in N −→β N [p := τ ][x := M ].
Definicja kwantyfikatora szczeg´o lowego w systemie F przypomina definicje alternatywy, i mo˙ze, by´c obja´sniona w podobny spos´ob. Mamy tu
”wytarcie” definicji sumy uog´olnionej wyra˙zonej w jezyku drugiego rz, edu. Taka suma to najmniejszy zbi´, or zawierajacy wszystkie sk ladniki., Poni˙zej, zmienna q musi by´c nowa, tj. q 6∈FVT(σ) ∪ {p}.
∃p σ = ∀q(∀p(σ → q) → q).
Zauwa˙zmy, ˙ze powy˙zsza definicja jest wzmocnieniem definicji klasycznej przez prawo de Mor-gana:
¬∀p¬σ = ∀p(σ → ⊥) → ⊥ Teraz mo˙zemy zdefiniowa´c pack i let:
• pack M, τ to ∃p. σ = Λqλz∀p(σ→q).zτ M ;
• let M be x, p in Nρ= M ρ(Λpλxσ.N ).
i sprawdzi´c, ˙ze wszystko dzia la jak trzeba.
Cwiczenia´
1. Zdefiniowa´c w systemie F funkcje wyk ladnicz, a, poprzednik, dzielenie ca lkowite, etc., 2. Zdefiniowa´c w systemie F funkcje Ackermanna.,
3. Czy da sie zdefiniowa´, c ka˙zda funkcj, e obliczaln, a?,