Typy proste mo˙zna uto˙zsamia´c z formu lami zdaniowymi zbudowanymi z atom´ow (zmien-nych zdaniowych) za pomoca samej implikacji. Ta analogia nie jest przypadkowa, bo regu ly, wyprowadzania typ´ow odpowiadaja regu lom wnioskowania:,
(Ax) Γ, σ ` σ
(W→) Γ, σ ` τ Γ ` σ → τ
(E→) Γ ` σ → τ Γ ` σ Γ ` τ
Regu ly te otrzymali´smy przez wytarcie z regu l systemu λ→ wszystkiego co dotyczy term´ow i pozostawienie tylko informacji o typach. Oczywi´scie symbol Γ, wystepujacy w regu lach, wnioskowania, oznacza po prostu zbi´or formu l. Logika okre´slona tymi regu lami to minimalna logika implikacyjna.
Je´sli Γ jest otoczeniem typowym, to przez |Γ| oznaczymy zbi´or formu l {Γ(x) | x ∈ Dom(Γ)}.
Nastepuj, ace twierdzenie wyra˙za w uproszczeniu odpowiednio´, s´c nazywana cz, esto izomorfizmem, Curry’ego-Howarda.
Twierdzenie 15.12
• Je´sli Γ ` M : τ w systemie λ→, to |Γ| ` τ w logice minimalnej.
• Je´sli Γ ` τ w logice minimalnej, to istnieje takie otoczenie typowe ∆, ˙ze |∆| = Γ oraz
∆ ` M : τ dla pewnego M w systemie λ→.
Dow´od: Latwa indukcja.
W sensie og´olnym, izomorfizm Curry’ego-Howarda to w la´snie ´scis la odpowiednio´s´c pomiedzy,
• formu lami i typami;
• dowodami i termami (programami).
Powstaje pytanie czy logika minimalna to to samo co implikacyjny fragment logiki klasycznej.
Ot´o˙z nie. Nastepuj, aca klasyczna tautologia, zwana prawem Peirce’a, nie jest twierdzeniem, logiki minimalnej:
π = ((p → q) → p) → p
Mo˙zna to latwo stwierdzi´c, korzystajac z prostej obserwacji: je´, sli istnieje term M typu τ , to istnieje te˙z taki term w postaci normalnej. Pozostaje wiec zbada´, c, jak mo˙ze wyglada´, c zamkniety term typu π w postaci normalnej i przekona´, c sie, ˙ze nijak.,
Na czym polega r´o˙znica? Logika minimalna jest konstruktywna. Implikacja w tej logice jest traktowana jak typ pewnej funkcji. Dow´od formu ly postaci α → β musi polega´c na wskaza-niu metody przekszta lcenia ka˙zdego potencjalnego dowodu (“konstrukcji”) za lo˙zenia α w po-prawny dow´od formu ly β. Nie ma innego kryterium prawdy opr´ocz dowodu, w szczeg´olno´sci nie wystarczy odwo lanie do dwuwarto´sciowej semantyki.
Kombinatory z typami
Jak zauwa˙zyli´smy, termy rachunku lambda z typami prostymi odpowiadaja ´, sci´sle dowodom w minimalnej logice implikacyjnej. Chodzi tu o dowody w systemie naturalnej dedukcji . Pojecie dowodu formalnego cz, esto jednak kojarzy si, e nam nie z naturaln, a dedukcj, a, ale z po-, dej´sciem Hilberta. To podej´scie jest bowiem zwykle prezentowane w podrecznikach logiki. Dla,
klasycznego implikacyjnego rachunku zda´n, hilbertowski system dowodzenia mo˙zna oprze´c na jednej regule wnioskowania (modus ponens)
α, α → β β i trzech nastepuj, acych schematach aksjomat´, ow.
• α → β → α;
• (α → β → γ) → (α → β) → α → γ;
• ((α → β) → α) → α.
Jak ju˙z wiemy, trzeci z tych aksjomat´ow, prawo Peirce’a, nie jest twierdzeniem logiki mini-malnej, ale pierwsze dwa tak. Sa to mianowicie typy znanych nam term´, ow zamknietych:,
• K = λxy.x;
• S = λxyz.xz(yz).
Okazuje sie, ˙ze je´, sli z powy˙zszego systemu odrzucimy trzeci aksjomat a pozostawimy dwa pierwsze, to otrzymamy system r´ownowa˙zny logice minimalnej. Piszemy Γ `H ϕ gdy for-mu la ϕ ma dow´od w takim systemie Hilberta ze zbioru dodatkowych za lo˙ze´n Γ. R´ownowa˙zno´s´c naszego systemu Hilberta i naturalnej dedukcji wynika z nastepuj, acego twierdzenia:,
Twierdzenie 15.13 (o dedukcji) Warunki Γ `H ϕ → ψ i Γ, ϕ `H ψ sa r´, ownowa˙zne.
Dow´od: Oczywi´scie wszyscy znaja dow´, od twierdzenia o dedukcji, ale przypomnijmy go13 z powod´ow metodologicznych. Dow´od ten w swojej trudniejszej cze´,sci — z prawej do lewej
— przebiega przez indukcje ze wzgl, edu na d lugo´, s´c dowodu formu ly ψ ze zbioru za lo˙ze´n Γ, ϕ.
Rozpatrzmy najpierw kilka latwych przypadk´ow.
Pierwszy latwy przypadek mamy wtedy, gdy w dowodzie nie u˙zyto w og´ole za lo˙zenia ϕ. Tak jest w szczeg´olno´sci wtedy, kiedy ψ jest aksjomatem lub ψ ∈ Γ, a dow´od sk lada sie tylko, z tej jednej formu ly. Inaczej m´owiac mamy w istocie dow´, od Γ `H ψ. Wtedy dow´od formu ly ϕ → ψ jest otrzymany przez oderwanie ψ od aksjomatu ψ → (ϕ → ψ).
Je´sli ψ = ϕ, to wystarczy udowodni´c, ˙ze `H ϕ → ϕ, co zostawiamy jako ´cwiczenie.
Pozostaje g l´owny krok indukcyjny, gdy dow´od formu ly ψ ze zbioru Γ, ϕ otrzymano przez odrywanie. Znaczy to, ˙ze Γ, ϕ ` ϑ → ψ i Γ, ϕ ` ϑ dla pewnej formu ly ϑ, i ˙ze odpowiednie dowody sa kr´, otsze. Z za lo˙zenia indukcyjnego otrzymujemy, ˙ze formu ly ϕ → (ϑ → ψ) i ϕ → ϑ maja dowody ze zbioru Γ. Aby otrzyma´, c dow´od dla ϕ → ψ, nale˙zy te dwie formu ly kolejno oderwa´c od drugiego aksjomatu w postaci (ϕ → (ϑ → ψ)) → ((ϕ → ϑ) → (ϕ → ψ)).
13W istocie nasz dow´od nieznacznie r´o˙zni sie od tego, kt´, ory wystepuje w wiekszo´, sci podrecznik´, ow.
Wniosek 15.14 Osad Γ ` ϕ jest wyprowadzalny w systemie naturalnej dedukcji wtedy i tylko, wtedy, gdy Γ `H ϕ.
Dow´od: W obie strony mamy prosta indukcj, e. Twierdzenie 15.13 jest nam potrzebne, w dowodzie cze´,sci (⇒) w przypadku wprowadzania implikacji.
Dla wnioskowania w stylu Hilberta te˙z mo˙zna m´owi´c o odpowiednio´sci Curry’ego-Howarda, ale nie chodzi ju˙z teraz o rachunek lambda. Dowody w stylu Hilberta otrzymujemy wy lacznie, przez stosowanie regu ly modus ponens, kt´ora jak wiemy odpowiada aplikacji. Aksjomaty lo-giczne systemu hilbertowskiego mo˙zna uwa˙za´c za sta le odpowiednich typ´ow. Dok ladniej, dla dowolnych typ´ow α, β, γ mo˙zemy postulowa´c sta le Kαβ i Sαβγ, kt´orym przypisujemy w dowol-nym otoczeniu typy:
• ` Kαβ : α → β → α;
• ` Sαβγ : (α → β → γ) → (α → β) → α → γ.
Inna mo˙zliwo´s´c, to za lo˙zy´c, ˙ze w systemie sa tylko dwie sta le K i S, kt´, orym mo˙zna (w dowolnym otoczeniu) przypisa´c ka˙zdy z typ´ow odpowiedniej postaci. W ten spos´ob otrzymamy rachunek kombinator´ow z typami prostymi , a wniosek 15.14 bedziemy teraz mogli odczyta´, c tak:
(∗) Typy niepuste w rachunku lambda i rachunku kombinator´ow z typami prostymi sa takie same.,
Uderzajace jest podobie´, nstwo pomiedzy dowodem twierdzenia 15.13 i definicj, a kombinato-, rycznej abstrakcji λ∗ (´cwiczenie 8). Ciekawe jest to, ˙ze ta analogia siega znacznie dalej ni˙z, tylko zgodno´s´c typ´ow. Mo˙zna powiedzie´c, ˙ze twierdzenie o dedukcji ma sens wykraczajacy, poza jezyk formu l logicznych.,
Typologia og´olna: sp´ojniki logiczne
Odpowiednio´s´c pomiedzy formu lami i typami by laby niepe lna, gdyby nie rozci, aga la si, e na, sp´ojniki logiczne inne ni˙z implikacja. W istocie nietrudno jest zinterpretowa´c w tym duchu zar´owno koniunkcje jak i alternatyw, e. Zacznijmy od przypomnienia regu l naturalnej dedukcji, dla tych sp´ojnik´ow.
Γ ` ϕ Γ ` ψ
Γ ` ϕ ∧ ψ (W ∧) Γ ` ϕ ∧ ψ
Γ ` ϕ (E∧) Γ ` ϕ ∧ ψ Γ ` ψ Γ ` ϕ
Γ ` ϕ ∨ ψ (W ∨) Γ ` ψ Γ ` ϕ ∨ ψ
Γ ` ϕ ∨ ψ Γ, ϕ ` ϑ Γ, ψ ` ϑ
Γ ` ϑ (E∨)
Regu ly te mo˙zemy obja´snia´c w my´sl tzw. interpretacji BHK (od nazwisk: Brouwer, Heyting, Ko lmogorow).
• Dow´od koniunkcji sk lada sie z dowod´, ow jej sk ladowych, jest wiec (uporz, adkowan, a) par, a, dowod´ow;
• Dow´od alternatywy to dow´od jednego z jej cz lon´ow (ze wskazaniem kt´orego).
A zatem koniunkcja odpowiada iloczynowi kartezja´nskiemu (rekordowi) a alternatywa sumie prostej (wariantowi). Wprowadzanie koniunkcji to tworzenie pary, a eliminacja koniunkcji to rzutowanie.
Γ ` M : ϕ Γ ` N : ψ
Γ ` hM, N i : ϕ ∧ ψ (W ∧) Γ ` M : ϕ ∧ ψ
Γ ` π1(M ) : ϕ (E∧) Γ ` M : ϕ ∧ ψ Γ ` π2(M ) : ψ
Wprowadzanie alternatywy odpowiada tworzeniu obiektu wariantowego. Eliminacja alterna-tywy to instrukcja wyboru.
Γ ` M : ϕ
Γ ` inl(M ) : ϕ ∨ ψ (W ∨) Γ ` M : ψ Γ ` inr(M ) : ϕ ∨ ψ Γ ` M : ϕ ∨ ψ Γ(x : ϕ) ` P : ϑ Γ(y : ψ) ` Q : ϑ
Γ ` case M of [x]P, [y]Q : ϑ (E∨) Dla tak rozszerzonego jezyka mo˙zemy teraz postulowa´c nastepuj, ace redukcje., Beta redukcje:
π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].
Eta redukcje:
hπ1(M ), π2(M )i → M ; (case M of [x]inl x, [y]inr y) → M .
M´owimy tu o beta i eta redukcjach przez analogie z redukcjami dla implikacji. Beta redeks, odpowiada wprowadzeniu sp´ojnika, po kt´orym natychmiast nastepuje jego eliminacja. Na-, tomiast postulat eta-redukcji odpowiada za lo˙zeniu, ˙ze ka˙zde wyra˙zenie danego typu opisuje pewien kanoniczny obiekt tego typu (funkcje, par, e, wariant — og´, olnie rezultat operacji wpro-wadzenia).
Pozostaje sprawa negacji, kt´ora jednak mo˙zemy zinterpretowa´, c jako specyficzna implikacj, e:,
¬α = α → ⊥
Symbol ⊥ oznacza fa lsz, kt´ory oczywi´scie nie mo˙ze mie´c dowodu. Nie ma wiec kanonicznych, obiekt´ow typu ⊥ — jest to typ pusty. Mamy jednak regu le eliminacji fa lszu:,
Γ ` M : ⊥
Γ ` εϕ(M ) : ϕ (E⊥)
Symbol εϕoznacza cud typu ϕ. Skoro mamy rzecz, kt´orej nie ma, to znaczy, ˙ze mo˙zemy z niej zrobi´c co zechcemy.
Regu ly wprowadzania i eliminacji sp´ojnik´ow tworza system naturalnej dedukcji dla zdaniowej, logiki intuicjonistycznej . Logika minimalna to jej fragment implikacyjny. Zauwa˙zmy, ˙ze nie ma w´sr´od naszych regu l zasady wnioskowania przez zaprzeczenie, np. takiej:
Γ, ¬ϕ ` ⊥ Γ ` ϕ
Dlatego twierdzeniami logiki intuicjonistycznej nie jest ˙zadna z formu l postaci p∨¬p, ¬¬p → p, (¬p → ¬q) → q → p, prawo Peirce’a, ani wiele innych praw logiki klasycznej.
Cwiczenia´
1. Udowodni´c twierdzenie 15.12.
2. Udowodni´c ˙ze nie istnieje kombinator typu π = ((p → q) → p) → p.
3. Pokaza´c, ˙ze K jest jedynym termem zamknietym w postaci normalnej, kt´, ory ma typ s → t → s (gdzie s i t sa zmiennymi typowymi). Pokaza´, c analogiczna w lasno´, s´c dla S.
4. Wyprowadzi´c `Hα → α. Wskaz´owka: Zbudowa´c ze sta lych K i S term takiego typu.
5. Sformu lowa´c regu ly przypisania typ´ow dla rachunku kombinator´ow z typami prostymi i udowod-ni´c stwierdzenie (*).
6. Udowodni´c silna normalizacj, e dla rachunku kombinator´, ow z typami prostymi.
7. Znale´z´c typy dla kombinator´ow W, B, B0 i C.
8. Udowodni´c, ˙ze w rachunku kombinator´ow z typami prostymi warunek Γ, x : τ ` M : σ implikuje Γ ` λ∗x.M : τ → σ.