Zgodnie z izomorfizmem Curry’ego-Howarda, twierdzenia intuicjonistycznej logiki implika-cyjnej to dok ladnie typy zamknietych term´, ow rachunku lambda (lub logiki kombinatorycznej).
Poniewa˙z ka˙zdy term typowalny ma posta´c normalna, wi, ec dla ustalenia, czy istnieje term, danego typu wystarczy szuka´c takiego termu w postaci normalnej. Prowadzi to do nastepu-, jacego algorytmu Ben-Yellesa, kt´, ory rozwiazuje nieco og´, olniej postawione zadanie:
• Dane sa otoczenie Γ i typ τ ;,
• Szukamy takiego termu M , ˙ze Γ ` M : τ ; Zadanie to mo˙zna rozbi´c na dwa przypadki:
(1) Je´sli τ = τ1 → τ2, to mo˙zna zak lada´c, ˙ze M musi by´c abstrakcja postaci λx.M, 0. (Je´sli term M nie jest abstrakcja, to zamiast M mo˙zna wzi, a´,c term λx.M x, gdzie x jest nowe.) Nale˙zy wiec znale´, z´c taki term M0 aby Γ, x : τ1` M0: τ2.
(2) Je´sli τ jest zmienna typow, a s, to term M musi by´, c aplikacja postaci xM, 1. . . Mk, gdzie Γ(x) = σ1 → · · · → σk → s. Nale˙zy wiec znale´, z´c termy M1, . . . , Mk spe lniajace warunki, Γ ` M1: σ1, . . . , Γ ` Mk : σk.
Poniewa˙z w przypadku (2) mo˙zemy mie´c do wyboru wiecej ni˙z jedn, a zmienn, a o typie ko´, ncza-, cym sie na s, wi, ec nasz algorytm jest w istocie niedeterministycznym algorytmem rekuren-, cyjnym, lub jak kto woli — algorytmem alternujacym., 14
Oczywi´scie, je´sli
”inhabitant” typu τ istnieje, to predzej czy p´, o´zniej znajdziemy go ta metod, a., Ale mo˙ze by´c tak, ˙ze nasz algorytm sie zap, etli — we´, zmy na przyk lad typ (s → s) → s, albo ((s → t) → t) → s → t. Je´sli wiec rozwi, azanie zadania dla danych Γ i τ prowadzi ponownie do, tego samego zadania, przerywamy obliczenie z wynikiem negatywnym. Aby unikna´,c sytuacji, w kt´orej pojawia sie niesko´, nczenie wiele r´o˙znych zada´n, musimy te˙z nieco poprawi´c dzia lanie algorytmu w przypadku (1).
(1a) Je´sli τ = τ1 → τ2, oraz w otoczeniu Γ nie ma zmiennej typu τ1, to szukamy takiego M0 aby Γ, x : τ1 ` M0 : τ2.
(1b) Je´sli τ = τ1→ τ2, oraz w otoczeniu Γ jest zmienna typu τ1, to szukamy takiego M0 aby Γ ` M0 : τ2.
Poprawno´s´c przypadku (1b) wynika z nastepuj, acej prostej obserwacji:, Je´sli Γ(y) = τ1 oraz Γ, x : τ1 ` M0 : τ2, to Γ ` M0[x := y] : τ2.
Inaczej m´owiac, wystarczy po jednej zmiennej ka˙zdego typu., Liczba typ´ow, kt´ore moga, sie pojawi´, c w obliczeniu jest proporcjonalna do rozmiaru zadania, a otoczenie stale ro´snie.
Zatem g leboko´, s´c rekursji jest wielomianowa (kwadratowa), a stad wynika, ˙ze ca ly algorytm, jest w klasie Pspace. I nie da sie go istotnie ulepszy´, c.
Twierdzenie 16.1 (Statman) Implikacyjna logika intuicjonistyczna jest Pspace-zupe lna.
A zatem problem niepusto´sci dla typ´ow prostych jest te˙z Pspace-zupe lny.
Dow´od: Redukujemy problem kwantyfikowanych formu l Boole’owskich (QBF), czyli kla-syczna logik, e zdaniow, a drugiego rz, edu, do intuicjonistycznego implikacyjnego rachunku zda´, n.15 Niech Φ bedzie formu l, a w j, ezyku QBF. Bez straty og´, olno´sci mo˙zemy za lo˙zy´c, ˙ze jest to zdanie, i ˙ze negacja wystepuje w Φ tylko w kontekstach postaci ¬p, gdzie p jest zmienn, a zdaniow, a., Dla higieny za l´o˙zmy jeszcze, ˙ze wszystkie zmienne zwiazane w Φ s, a r´, o˙zne.
Dla dowolnej zmiennej zdaniowej p, kt´ora wystepuje w formule Φ, niech s, p i s¬pbed, a nowymi, zmiennymi typowymi. Podobnie, dla ka˙zdej podformu ly ϕ formu ly Φ wybierzmy nowe zmien-ne typowe sϕ i s¬ϕ. Przez ΓΦ oznaczmy zbi´or z lo˙zony z nastepuj, acych formu l:,
• (sp → sψ) → (s¬p→ sψ) → sϕ, dla ka˙zdej podformu ly ϕ postaci ∀pψ;
• (sp → sψ) → sϕ i (s¬p→ sψ) → sϕ, dla ka˙zdej podformu ly ϕ postaci ∃pψ;
• sψ → sϑ→ sϕ, dla ka˙zdej podformu ly ϕ postaci ψ ∧ ϑ;
14Krok egzystencjalny to wyb´or zmiennej x, krok uniwersalny to wyb´or jednego z term´ow Mi.
15Jak wida´c, logika minimalna wcale nie jest taka minimalna.
• sψ → sϕ i sϑ→ sϕ, dla ka˙zdej podformu ly ϕ postaci ψ ∨ ϑ.
Je´sli teraz v jest warto´sciowaniem zerojedynkowym o sko´nczonej dziedzinie, to Γv oznacza ΓΦ rozszerzone, dla wszystkich p ∈ Dom(v), o zmienne
• sp, gdy v(p) = 1;
• s¬p, gdy v(p) = 0,
Teraz przez latwa indukcj, e ze wzgl, edu na d lugo´, s´c podformu ly ϕ, dowodzimy, ˙ze Γv ` sϕ wtedy i tylko wtedy, gdy v(ϕ) = 1,
je´sli v jest okre´slone na zmiennych wolnych (ale nie zwiazanych) formu ly ϕ. W szczeg´, olno´sci formu la Φ jest prawdziwa wtedy i tylko wtedy, gdy ΓΦ ` sΦ. Pozostaje zauwa˙zy´c, ˙ze warunek ΓΦ ` sΦ to to samo co γ1 → · · · → γn → sΦ dla odpowiednich γi, oraz, ˙ze ca la konstrukcj, e, mo˙zna przeprowadzi´c w pamieci logarytmicznej.,
Rekonstrukcja typu
Oczywi´scie nie ka˙zdy term jest typowalny w systemie λ→, nawet je´sli jest w postaci normal-nej. Przyk ladem jest cho´cby λx.xx. Problemem typowalno´sci (typability) (albo problemem rekonstrukcji typu) dla danego systemu przypisania typ´ow nazywamy taki problem decyzyjny:
Czy dany term M jest typowalny?
Zbli˙zonym zagadnieniem jest problem sprawdzenia typu (type checking):
Dane sa M , Γ i τ . Czy Γ ` M : τ ?,
Problem typowalno´sci dla rachunku z typami prostymi jest r´ownowa˙zny (ze wzgledu na re-, dukcje w Logspace) problemowi unifikacji dla jezyka pierwszego rz, edu z jedn, a operacj, a, binarna →, i dlatego mamy nast, epuj, acy fakt:,
Twierdzenie 16.2 Problem typowalno´sci dla λ→ jest zupe lny w klasie P.
Problem sprawdzenia typu dla λ→ te˙z jest w klasie P. Inny dow´od rozstrzygalno´sci obu pro-blem´ow polega na sprowadzeniu ich do szukania cyklu w pewnym sko´nczonym grafie.
Konsekwencja redukcji typowania do unifikacji jest nast, epuj, aca w lasno´, s´c typu g l´ownego.
Powiemy, ˙ze para (Γ, τ ) jest instancja pary (Γ, 0, τ0), gdy (Γ, τ ) jest otrzymane z (Γ0, τ0) przez podstawienie pewnych typ´ow w miejsce zmiennych typowych.
Twierdzenie 16.3 Je´sli term M jest typowalny, to istnieje takie otoczenie Γ0 i typ τ0, ˙ze dla dowolnych Γ, τ :
Γ ` M : τ ⇔ para (Γ, τ ) jest instancja pary (Γ, 0, τ0).
Para (Γ0, τ0), o kt´orej mowa w twierdzeniu, jest nazywana para g l´, owna dla M , a typ τ, 0 to oczywi´scie typ g l´owny tego termu.
R´owno´s´c
Rozpatrzmy term 2 · · · 2xy, w kt´orym wystepuje n dw´, ojek. Nietrudno sie przekona´, c, ˙ze postacia normaln, a tego termu jest x(x(· · · (xy) · · · )), gdzie liczb, a wyst, apie´, n zmiennej x jest
2
2··
·2) n
Najprostszy algorytm sprawdzajacy, czy dwa termy tego samego typu s, a beta-r´, owne, polega na obliczeniu i por´ownaniu ich postaci normalnych. Jak wida´c z powy˙zszego przyk ladu rozmiar postaci normalnej mo˙ze by´c bardzo du˙zy w stosunku do rozmiaru danego termu.
Nawet je´sli uwzglednimy rozmiary u˙zytych typ´, ow sytuacja zmieni sie niewiele. Zauwa˙zmy, bowiem, ˙ze typy, kt´orych potrzebujemy aby wywnioskowa´c
x : t → t, y : t ` 2 · · · 2xy : t sa,
”zaledwie” wyk ladniczego rozmiaru (ka˙zda kolejna dw´ojka ma dwa razy d lu˙zszy typ). A za-tem nasz naiwny algorytm ma nieelementarna z lo˙zono´, s´c. Co gorsza, nie mo˙zna go istotnie poprawi´c.
Twierdzenie 16.4 (Statman) Problem r´owno´sci term´ow w rachunku lambda z typami pros-tymi nie jest problemem elementarnym (nie istnieje algorytm rozwiazuj, acy ten problem w cza-, sie 22··
·2no
k dla ˙zadnego ustalonego k).
Co innego jednak por´owna´c dwa termy, a co innego znale´z´c term, lub termy spe lniajace, zadane r´ownanie. Rozwiazywanie r´, owna´n z niewiadomymi dowolnych typ´ow sko´nczonych nazywamy unifikacja wy˙zszego rz, edu. Aby ´, sci´sle sformu lowa´c problem unifikacji przyjmijmy,
˙ze dane jest otoczenie Γ i para term´ow (M, N ), kt´ore w tym otoczeniu maja ten sam typ., W´sr´od zmiennych deklarowanych w Γ wyr´o˙znimy niewiadome x1, . . . , xka wszystkie pozosta le zmienne nazwiemy parametrami . Rozwiazaniem r´, ownania M = N o niewiadomych x1, . . . , xk
nazywamy dowolne termy P1, . . . , Pk spe lniajace warunki,
• Γ ` Pi : Γ(xi) dla i = 1, . . . , k;
• M [x1 := P1, . . . , xk:= Pk] =βη N [x1 := P1, . . . , xk:= Pk].
Problem unifikacji wy˙zszego rzedu to nast, epuj, acy problem decyzyjny: czy istnieje rozwi, azanie, danego r´ownania? Zwykle zak lada sie, ˙ze wszystkie typy wyst, epuj, ace w zadaniu s, a zbudowane, z jednego atomu. Nie zmienia to istotnie stopnie trudno´sci zadania. Je´sli typy wszystkich niewiadomych sa postaci t → t → · · · → t → t lub t, gdzie t jest typem atomowym, to, m´owimy o unifikacji drugiego rzedu. Zwyk l, a unifikacj, e nazywamy te˙z unifikacj, a pierwszego, rzedu (niewiadome maj, a typ atomowy).,
Przyk lad 16.5
Oto dwa przyk lady unifikacji drugiego rzedu z parametrami f : t → t → t, a : t, b : t, i niewiadomymi G : t → t → t, F : t → t.
• Ga(f ba) = f a(Gab);
• f a(F a) = F (f aa).
Pierwszy przyk lad nie ma rozwiazania, drugi ma ich niesko´, nczenie wiele. Rozwiazaniami s, a, wszystkie termy postaci λx.f a(f a(f a(· · · (f ax) · · · ))).
Twierdzenie 16.6 (Goldfarb) Unifikacja drugiego rzedu jest nierozstrzygalna.,
Dow´od twierdzenia Goldfarba polega na redukcji Dziesiatego Problemu Hilberta do unifikacji, drugiego rzedu. Dla dowolnego wielomianu konstruuje si, e takie r´, ownanie unifikacyjne, kt´ore ma rozwiazanie wtedy i tylko wtedy, gdy dany wielomian ma zero ca lkowite.,
Szczeg´olnym przypadkiem unifikacji jest dopasowanie (matching). Problem dopasowania wy˙zszego rzedu polega na rozwiazaniu r´, ownania, w kt´orym niewiadome wystepuja tylko po, lewej stronie. Do niedawna wiadomo by lo tylko, ˙ze dopasowanie rzedu czwartego jest rozstrzy-, galne, ale ostatnio C. Stirling og losi l, ˙ze problem jest rozstrzygalny. Je´sli w zadaniu dopa-sowania zmieni´c =βη na =β, to problem okazuje sie by´, c nierozstrzygalny. Udowodni l to kilka...
(ju˙z kilkana´scie!) lat temu Ralph Loader.
Funkcje definiowalne
Jak pamietamy, w beztypowym rachunku lambda mo˙zna reprezentowa´, c wszystkie funkcje rekurencyjne, a nawet cze´,sciowo rekurencyjne (twierdzenie 7.9). W rachunku lambda z typami prostymi nie nale˙zy sie spodziewa´, c podobnego wyniku, bo r´owno´s´c term´ow jest rozstrzygalna.
W istocie klasa funkcji definiowalnych w rachunku λ→ jest do´s´c uboga. Ale musimy zacza´,c od odpowiedniej definicji.
Niech σ bedzie dowolnym typem. Przez ω, σ oznaczamy typ (σ → σ) → σ → σ. Je´sli σ jest nieistotne (zwykle jest to ustalony atom), to piszemy po prostu ω. Oczywi´scie wszystkie liczebniki Churcha maja typ ω, wi, ec naturalna jest nast, epuj, aca definicja:,
Funkcja f : Nk → N jest β-definiowalna (lub po prostu definiowalna) w rachunku lambda z typami prostymi, w typie ωσ, je˙zeli istnieje term zamkniety F , spe lniaj, acy nast, epuj, ace, warunki:
• ` F : ωσ → · · · → ωσ → ωσ;
• Dla dowolnych n1, . . . , nk∈ N, je˙zeli f(n1, . . . , nk) = m to F n1. . . nk=β m.
Zamieniajac w powy˙zszej definicji znak =, βna =βηotrzymujemy klase funkcji βη-definiowalnych., Nastepnik, dodawanie i mno˙zenie s, a przyk ladami funkcji definiowalnych w λ, → (zob. przy-k lad 7.3). Mo˙zemy te˙z zdefiniowa´c funkcje warunkow, a,
ifzero(p, q, r) =
q, je´sli p = 0;
r, w przeciwnym przypadku.
za pomoca termu,
ifzero = λpqrλf x.p(λy.rf x)(qf x).
Je´sli zostaniemy przy r´owno´sci β to wiecej zdefiniowa´, c nam sie nie uda.,
Twierdzenie 16.7 (Schwichtenberg) Dla dowolnego σ klasa funkcji β-definiowalnych w λ→
w typie ωσ to dok ladnie klasa wielomian´ow warunkowych, tj. najmniejsza klasa funkcji nad N, zamknieta ze wzgl, edu na sk ladanie i zawieraj, aca:,
• rzutowania;
• dodawanie;
• mno˙zenie;
• funkcje sta le 0 i 1;
• funkcje warunkow, a ifzero.,
Z twierdzenia Schwichtenberga wynika, w szczeg´olno´sci, ˙ze wyb´or typu σ nie ma znaczenia.
Dotad uwa˙zano, ˙ze tak samo jest w przypadku βη-definiowalno´, sci, ale Mateusz Zakrzewski niedawno pokaza l, ˙ze np. funkcja
ifeven(p, q, r) =
q, je´sli p jest parzyste;
r, w przeciwnym przypadku,
kt´ora nie jest wielomianem warunkowym, jest βη-definiowalna (gdy liczebniki interpretujemy w odpowiednio dobranym typie ωσ). Patrz ´cwiczenie 10.
Nawet jednak z u˙zyciem βη-konwersji, tak proste funkcje jak poprzednik, odejmowanie i pote-, gowanie nie sa definiowalne. Poprzednik i pot, eg, e uda nam si, e zdefiniowa´, c je´sli jeszcze bardziej os labimy nasze wymagania. Powiemy, ˙ze funkcja f : Nk→ N jest sko´snie definiowalna w λ→, je´sli istnieje term F spe lniajacy warunki:,
• ` F : ωσ1 → · · · → ωσk → ωσ;
• Dla dowolnych n1, . . . , nk∈ N, je˙zeli f(n1, . . . , nk) = m to F n1. . . nk=β m.
Okazuje sie, ˙ze poprzednik i pot, egowanie s, a definiowalne sko´, snie, ale ju˙z odejmowanie nie jest.
Klase funkcji arytmetycznych definiowalnych w sko´, nczonych typach mo˙ze istotnie powiekszy´c dopiero dodanie do systemu
”prawdziwego” operatora iteracji. W ten spos´ob otrzymujemy tzw. System T G¨odla.
Cwiczenia´
1. Czy za lo˙zenie o higienicznym rozdzieleniu zmiennych wolnych i zwiazanych jest istotne w dowodzie, twierdzenia 16.1?
2. Udowodni´c twierdzenie 16.2.
3. Niech τ bedzie typem, w kt´, orym wystepuj, a tylko zmienne typowe s, 1, . . . , sn i niech Γ bedzie, takim otoczeniem, ˙ze Γ(xi) = si dla i = 1, . . . n. Skonstruowa´c taki term Mτ, ˙ze Γ ` M : σ wtedy i tylko wtedy, gdy σ = τ .
4. Niech E = {τ1 = σ1, . . . τk = σk} bedzie instancj, a problemu unifikacji dla j, ezyka pierwszego, rzedu z jedn, a operacj, a binarn, a → o niewiadomych s, 1, . . . , sn. Skonstruowa´c (w pamieci loga-rytmicznej) taki term M , kt´ory jest typowalny wtedy i tylko wtedy, gdy E ma rozwiazanie., Wskaz´owka: Skorzysta´c z poprzedniego zadania.
5. Zbada´c rozwiazalno´, s´c unifikacji z przyk ladu 16.5.
6. ( Latwe) Niech cn = λx.f a(f a(f a(· · · (f ax) · · · ))), gdzie f wystepuje n razy. Skonstruowa´c takie r´ownanie drugiego rzedu, kt´, orego rozwiazaniami s, a dok ladnie tr´, ojki term´ow postaci cn, cm, cn+m. 7. (Trudne) Skonstruowa´c takie r´ownanie drugiego rzedu, kt´, orego rozwiazaniami s, a dok ladnie tr´, ojki
term´ow postaci cn, cm, cn·m.
8. ( Latwe, je´sli umiemy rozwiaza´, c poprzednie dwa zadania.) Udowodni´c twierdzenie 16.6.
9. Udowodni´c, ˙ze poprzednik i potegowanie s, a niejednostajnie definiowalne w sko´, nczonych typach.
Dlaczego sa k lopoty z odejmowaniem?,
10. Niech F = λnf xa1a2a3. n(λyz1z2z3. yz2z3z1)(λz1z2z3. z1)(xa1a2a3)(f xa1a2a3)(f (f x)a1a2a3).
Pokaza´c, ˙ze F : ωτ→ ωτ dla pewnego τ . Jaka funkcj, e z N do N definiuje term F ?, 11. Wzorujac si, e na poprzednim ´, cwiczeniu, zdefiniowa´c funkcje n 7→ min(n, 3).,