Dodatek C: System T

System G¨odla T to w istocie rachunek lambda z typami prostymi, rozszerzony o typ int liczb naturalnych (wraz z

”gotowymi” liczebnikami) oraz operator rekursji. ´Sci´slej:

• Typy systemu T to sta la typowa int i typy postaci (τ → σ), gdzie τ i σ s

a typami., ³⁰

• Termy sa jak w rachunku z typami prostymi w stylu Churcha, ale mog_, a zawiera´_, c sta le:

– 0 : int;

– s : int → int;

– R_τ : (int → τ → τ ) → τ → (int → τ ), dla dowolnego τ .

• Opr´ocz zwyk lej beta-redukcji w systemie sa dwie regu ly dla rekursora:_, – R_τM N (sP ) ⇒ M P (R_τM N P );

– RτM N 0 ⇒ N .

Relacje redukcji oznaczamy przez →_, T, znaki T i =T rozumiemy jak zwykle.

Liczebniki konstruujemy za pomoca sta lych 0 i s: przez n oznaczamy term s(s(· · · s(0) · · · )),_, w kt´orym s u˙zyte zosta lo n razy. Mo˙zemy teraz m´owi´c o definiowaniu funkcji. Powiemy, ˙ze funkcja f : N^k → N jest definiowalna w systemie T, je˙zeli istnieje kombinator F : int^k→ int, taki ˙ze dla f (n1, . . . , nk) = m zachodzi F n1. . . nk=T m.

Jako pierwszy przyk lad rozpatrzmy zastosowanie rekursora R_int do termu M = λxz.sz. Dla dowolnych m, n otrzymamy R_intM nm Tn + m. Oto kilka dalszych przyk lad´ow:

• Funkcja warunkowa if x = 0 then y else z jest definiowalna wyra˙zeniem R_int(λuv.z)yx.

• Funkcja poprzednika jest definiowalna wyra˙zeniem λx.R_int(λuv.u)0x.

• Niech funkcja f bedzie okre´_, slona przez rekursje prost_, a_, f (0, n₁, . . . , n_k) = g(n₁, . . . , n_k);

f (s(m), n1, . . . , nk) = h(m, n1, . . . , nk, f (m, n1, . . . , nk)),

gdzie g, h sa definiowalne odpowiednio przez termy G i H. Wtedy f jest definiowalne_, termem F = λx~y.Rint(λuv.Hu~yv)(G~y)x. Jak wida´c, u˙zycie rekursora Rint odpowiada zwyk lej rekursji prostej.

• Niech f₀(n) = n + 1 i niech fk+1(n) = f_kⁿ(n), dla dowolnych k i n. Wszystkie funkcje fk

sa definiowalne. Rzeczywi´_, scie, niech M = λf xy.R_int(λuv.f v)yx. Je´sli teraz F_kdefiniuje funkcje f_{, k} to term F_k+1 = λx.M F_kxx definiuje f_k+1.

• Wreszcie niech f_ω(n) = f_n(n). Funkcja f_ωjest pewnym wariantem funkcji Ackermanna.

Nie jest to funkcja pierwotnie rekurencyjna. Niemniej, jest definiowalna w systemie T za pomoca termu F_, ω = λx.R_int→int(λφy.M φyy)sxx. Istotnie, operator λφy.M φyy przy lo˙zony do F_k daje F_k+1. Iterujemy go n-krotnie, a wynik aplikujemy do n.

30Mo˙zna doda´c zmienne typowe, sa nieszkodliwe, ale w tym kontek´_, scie ma lo przydatne.

• Rozpatrzmy pozasko´nczony ciag funkcji f_{, α}, w kt´orym f_α+1(n) = f_αⁿ(n), a dla liczby gra-nicznej β przyjmujemy fβ(n) = f_β[n](n), gdzie β[n] jest odpowiednio dobranym ciagiem_, rosnacym, takim ˙ze sup β[n] = β. Na przyk lad f_{, ω}^ω(n) = f_ωⁿ(n). Ta definicja ma sens dla α < ₀, gdzie ₀ jest najmniejsza liczb_, a porz_, adkow_, a o w lasno´_, sci ω^0 = ₀, czyli granica ci_, agu α_, 0 = ω, αn+1 = ω^αn. Ka˙zda z funkcji fα jest definiowalna w T, ale ju˙z dla α = ω^ω potrzebny jest rekursor R(int→int)→(int→int).

Arytmetyka pierwszego rzedu: Dzi´_, s mo˙zna powiedzie´c, ˙ze system T to pewien specyficzny jezyk programowania. Ale wymy´_, slono go po to, ˙zeby udowodni´c niesprzeczno´s´c arytmetyki Peana. Bo zwiazek systemu T z arytmetyk_, a pierwszego rz_, edu jest bardzo ´_, scis ly. ˙Zeby go zauwa˙zy´c, przypomnijmy sobie aksjomaty arytmetyki Peana w ich

”tradycyjnej” postaci:

• A₁: int(0).

• A₂: ∀x(int(x) → int(sx)).

• A₃: ∀x(int(x) → int(y) → sx = sy → x = y).

• A₄: ∀x(int(x) → ¬(sx = 0)).

• A^ϕ₅ : ∀x(int(x) → ϕ(x) → ϕ(sx)) → ϕ(0) → ∀x(int(x) → ϕ(x)).

Tutaj int(x) jest jednoargumentowym predykatem, kt´ory czytamy “x jest liczba naturaln_, a”._, Aksjomaty A1 i A2jawnie wprowadzaja kanoniczne obiekty typu int: zero i nastepniki obiek-_, t´ow typu int. Aksjomaty A3 i A4 gwarantuja, ˙ze ka˙zdorazowe zastosowanie operacji nast_, ep-_, nika tworzy nowa liczb_, e naturaln_, a, r´_, o˙zna od wszystkich poprzednich. Wreszcie aksjomat A_{, 5} to w istocie nie jeden aksjomat, ale schemat indukcji. Te same aksjomaty przyjmujemy dla intuicjonistycznej arytmetyki, kt´ora nazywamy arytmetyk_, a Heytinga. Jedynym aksjomatem_, zawierajacym negacj_, e jest A_{, 4}, czasem zastepowany przez nieco s labsz_, a_,

”pozytywna” wersj_, e:_,

• A⁰₄: ∀x(int(x) → sx = 0 → ∀y(int(y) → y = 0)).

Poniewa˙z og´olnie nie lubimy formu l negatywnych, wiec my te˙z poprzesta´_, nmy na A⁰₄. Nie tracimy na tym nic istotnego, jak d lugo zajmujemy sie formu lami pozytywnymi._,

Wycieranie zale ˙zno´sci: Dla takiego pozytywnego jezyka arytmetyki okre´_, slimy operator wycierania zale˙zno´sci κ, kt´ory dowolnej formule ϕ arytmetyki pierwszego rzedu przypisuje_, formu le zdaniow_, a κ(ϕ). Otrzymujemy j_, a z ϕ przez_,

”wytarcie” wyra˙ze´n i kwanyfikator´ow in-dywiduowych. Przy tym predykat int staje sie po prostu wyr´_, o˙znionym symbolem zdaniowym (sta la typow_, a), a r´_, owno´s´c t lumaczymy na sta la logiczn_, a > (typ jednostkowy). Je´_, sli bowiem ignorujemy indywidua, powinni´smy te˙z ignorowa´c r´ownania pomiedzy nimi._,

• κ(int(t)) = int.

• κ(t = s) = >.

• κ(ϕ → ψ) = κ(ϕ) → κ(ψ).

• κ(∀xϕ) = κ(∃xϕ) = κ(ϕ).

Koniunkcje i alternatyw_, e pomin_, eli´_, smy, ˙zeby nie komplikowa´c sprawy. Zobaczmy co zostaje z aksjomat´ow Peana po wytarciu zale˙zno´sci:

• κ(A₁) : int.

• κ(A₂) : int → int.

• κ(A₃) : int → int → > → >).

• κ(A⁰₄) : (int → >) → (int → >).

• κ(A^ϕ₅) : (int → τ → τ ) → τ → int → τ , gdzie τ = κ(ϕ):

Formu ly-typy κ(A₃) i κ(A⁰₄) nie sa zbyt ciekawe: ka˙zda ma tylko trywialne inhabitanty. Ale_, typy pozosta lych aksjomat´ow to dok ladnie typy sta lych systemu T. A skad si_, e wzi_, e ly re-_, gu ly redukcji dla rekursora? Skoro rekursor ma taki typ jak aksjomat indukcji, to w my´sl izomorfizmu Curry’ego-Howarda, u˙zycie rekursora reprezentuje dow´od przez indukcje._, Dow´od indukcyjny tezy ∀x(int(x) → ϕ(x)) sk lada sie z dw´_, och cze´_,sci: kroku bazowego D₀ (dowodu formu ly ϕ(0)) i kroku indukcyjnego D1 (dowodu dla ∀x(int(x) → ϕ(x) → ϕ(sx))).

Mo˙zemy tu napisa´c D₀ : ϕ(0) i D₁ : ∀x(int(x) → ϕ(x) → ϕ(sx)), a ca ly dow´od indukcyjny oznaczy´c jako A^ϕ₅D₁D₀ : ∀x(int(x) → ϕ(x)). Mo˙zliwy spos´ob u˙zycia takiego dowodu to zaaplikowanie go do konkretnej liczby naturalnej, a ´sci´slej do wyra˙zenia arytmetycznego t oraz (uwaga!) dowodu P : int(t), uzasadniajacego, ˙ze t przedstawia liczb_, e naturaln_, a. Dostajemy_, wtedy dow´od A^ϕ₅D₁D₀tP : int(t). W tej konwencji, dowodem formu ly ϕ(0) jest A^ϕ₅D₁D₀0A₁, a dowodem formu ly ϕ(2) jest A^ϕ₅D1D0(s(sx))A21(A20(A1)), bo przecie˙z 1 = s0 i 2 = s(s0).

Ale z takich dowod´ow indukcja mo˙ze by´c wyeliminowana. Na przyk lad, nie ma potrzeby dowodzi´c ∀x(int(x) → ϕ(x)), je´sli tak naprawde mamy wyprowadzi´_, c ϕ(0). To znaczy, ˙ze powinni´smy mie´c regu le upraszczania dowod´_, ow

A^ϕ₅D1D00A1 ⇒ D₀.

Oczywi´scie mo˙zna tak˙ze wyeliminowa´c np. z dowodu formu ly ϕ(4). Mo˙zna ja zast_, api´_, c czte-rokrotna aplikacj_, a kroku indukcyjnego do kroku bazowego._, Taki dow´od jest d lu˙zszy, ale niewatpliwie bardziej elementarny. Oto regu la, kt´_, ora takie uproszczenie umo˙zliwia:

A^ϕ₅D₁D₀(st)(A₂tP^int(t))^int(st)⇒ D₁tP (A^ϕ₅D₁D₀tP ) : ϕ(st)

Skoro mo˙zna wyciera´c zale˙zno´sci z formu l, mo˙zna je te˙z wyciera´c z dowod´ow. Usu´nmy z powy˙zszych regu l wszystko to co indywiduowe, a dla lepszego efektu zamie´nmy A1, A2, A5

odpowiednio na 0, s, R. Co dostajemy? Tak, regu ly redukcji dla rekursora!

Mora l: Termy systemu T to

”schematy” czy

”szkielety” (konstruktywnych) dowod´ow w jezyku_, arytmetyki, a regu ly redukcji w T modeluja normalizacj_, e dowod´_, ow w arytmetyce.³¹

Silna normalizacja

Dow´od silnej normalizacji systemu T przeprowadzimy metoda Taita, tak jak dow´_, od twierdze-nia 14.11. Definicja stabilno´sci jest w zasadzie taka sama.

• [[int]] := SN;

• [[τ → σ]] := {M : τ → σ | ∀N (N ∈ [[τ ]] → M N ∈ [[σ]])}.

31Ale zauwa˙zmy, ˙ze liczebnik n = s(s(· · · s(0) · · · )) nie powstaje z wyra˙zenia arytmetycznego s(s(. . . (0) . . .)), ale z dowodu A2n−1(A2n−2(· · · A2(0A1) · · · )) stwierdzajacego, ˙ze term n przedstawia liczb_, e naturaln_, a._,

Tre´s´c i dowody lemat´ow 14.7–14.9 pozostaja bez zmian. Potrzebujemy jeszcze jednego._,

Lemat C.9 Sta le systemu T sa stabilne w odpowiednich typach:_, 1. 0 ∈ [[int]];

2. s ∈ [[int → int]];

3. Rτ ∈ [[(int → τ → τ ) → τ → (int → τ )]]

Dow´od: (3) Wystarczy udowodni´c, ˙ze je´sli termy M , N , P sa stabilne w odpowiednich_, typach, to term R_τM N P jest stabilny w typie τ . Poniewa˙z P jest stabilny, to ma posta´c normalna P_, 0 = sⁿ(P1), gdzie n ≥ 0, a term P1 nie zaczyna sie od nast_, epnika. Dzia lamy_, przez indukcje ze wzgl_, edu na n. Je´_, sli τ = τ₁ → · · · → τ_k → int, to wystarczy pokaza´c, ˙ze R_τM N P N₁. . . N_k jest silnie normalizowalny, je´sli tylko N₁, . . . N_k sa stabilne._,

Rozpatrzmy dowolny ciag redukcji zaczynaj_, acy si_, e od R_, τM N P N1. . . Nk. Z powodu sil-nej normalizacji wszystkich sk ladowych, musi sie w tym ci_, agu pojawi´_, c redeks, tj. mamy R_τM N P N₁. . . N_k T R_τM⁰N⁰P⁰N₁⁰. . . N_k⁰, gdzie P⁰ jest zerem lub zaczyna sie od nastep-_, nika. Je´sli P⁰= 0, to dalsza redukcja prowadzi do N⁰N₁⁰. . . N_k⁰. Ten term mo˙zna te˙z otrzyma´c przez redukowanie stabilnego termu N N1. . . N_k, a wiec nale˙zy on do SN. Jesli za´_, s P⁰ = sP⁰⁰ to otrzymujemy term X = M⁰P⁰⁰(R_τM⁰N⁰P⁰⁰)N₁⁰. . . N_k⁰. Aby pokaza´c, ˙ze X ∈ SN wystarczy sprawdzi´c silna normalizacj_, e termu Z = M P_, ⁰⁰(RτM N P⁰⁰)N1. . . Nk, kt´ory te˙z redukuje sie_, do X. To wynika z za lo˙zenia indukcyjnego. Bo po pierwsze P⁰  sP⁰⁰ wiec P_, ⁰⁰ ∈ SN = [[int]].

A po drugie posta´c normalna P⁰⁰ ma na poczatku tylko n − 1 nast_, epnik´_, ow.

A wiec w ka˙zdym przypadku redukcja R_, τM N P N1. . . Nk prowadzi do termu w SN.

Z powy˙zszego wynika, ˙ze lemat 14.10 pozostaje prawdziwy dla systemu T, a zatem dostajemy:

Twierdzenie C.10 System T ma w lasno´s´c silnej normalizacji.

Twierdzenie C.11 System T ma w lasno´s´c Churcha-Rossera.

Dow´od: Mo˙zna to udowodni´c korzystajac z Twierdzenia C.10 i z Lematu Newmana._, System T i arytmetyka: Korzystajac z twierdzenia o silnej normalizacji dla systemu T_, mo˙zna udowodni´c, ˙ze ka˙zde twierdzenie arytmetyki Heytinga ma dow´od w postaci normal-nej , tj. dow´od o szczeg´olnie prostej strukturze. Pomijajac wyja´_, snienia co to dok ladnie znaczy, powiedzmy tylko, ˙ze jedynym normalnym dowodem r´owno´sci pomiedzy dwoma liczebnikami,_, tj. r´owno´sci postaci s(s(. . . s(0) . . .)) = s(s(. . . s(0) . . .)) jest aksjomat A1, co oznacza w szcze-g´olno´sci, ˙ze po obu stronach musi by´c ten sam liczebnik. Nie ma wiec dowodu formu ly_, 0 = s(0), a zatem intuicjonistyczna arytmetyka jest niesprzeczna. Klasyczna arytmetyka Peana te˙z musi by´c niesprzeczna, bo mo˙zna ja_,

”zanurzy´c” w arytmetyce Heytinga za pomoca_, tzw. translacji Ko lmogorowa. Pamietamy jednak z logiki, ˙ze niesprzeczno´_, sci arytmetyki Peana nie da sie udowodni´_, c w arytmetyce Peana. Okazuje sie, ˙ze jedyn_, a cz_, e´_,scia naszkicowanego_,

wy˙zej dowodu niesprzeczno´sci, kt´ora nie daje sie sformalizowa´_, c w jezyku arytmetyki, jest_, w la´snie twierdzenie C.10.

W lasno´s´c silnej normalizacji systemu T mo˙zna wypowiedzie´c tak: Dla ka˙zdego termu M istnieje takie n, ˙ze ka˙zdy sko´nczony ciag redukcji rozpoczynaj_, acy si_, e od M ma d lugo´_, s´c co naj-wy˙zej n. Je´sli um´owimy sie, ˙ze termy i ich sko´_, nczone ciagi s_, a reprezentowane jako liczby natu-_, ralne za pomoca jakiego´_, s ustalonego kodowania, to powy˙zsze zdanie mo˙zna wyrazi´c w jezyku_, arytmetyki. Mamy wiec konkretny przyk lad zdania w j_, ezyku arytmetyki, kt´_, ore jest od niej niezale˙zne. Jakiego aparatu logicznego wymaga wiec dow´_, od twierdzenia C.10?

W dowodzie definiowali´smy dwuargumentowy predykat M ∈ [[τ ]], przez indukcje ze wzgl_, edu_, na typ τ . Definicja indukcyjna to jednak definicja

”uwik lana”. Nie umiemy natomiast zdefi-niowa´c tego predykatu

”wprost”, tj. nie umiemy napisa´c formu ly ϕ(M, τ ) r´ownowa˙znej warun-kowi M ∈ [[τ ]]. Je´sli wiec chcemy w j_, ezyku logiki formalnej zapisa´_, c np. tre´s´c lematu 14.7(1) to musimy pos lu˙zy´c sie tak_, a konstrukcj_, a: Dla dowolnego dwuargumentowego predykatu X,_, spe lniajacego warunki_,

• ∀M (X(M, int) ⇔ M ∈ SN);

• ∀M ∀τ ∀σ(X(M, τ → σ) ⇔ ∀N (X(N, τ ) ⇒ X(M N, σ))},

zachodzi ∀M ∀τ (X(M, τ ) ⇒ M ∈ SN). Ta konstrukcja u˙zywa jednak kwantyfikatora ∀X, gdzie X przebiega relacje, a nie indywidua. Takie kwantyfikatory sa dozwolone w logice_, i arytmetyce drugiego rzedu. I tego si_, e nie da poprawi´_, c: arytmetyka pierwszego rzedu nie_, wystarczy.

Twierdzenie C.12 Twierdzenie o silnej normalizacji systemu T jest niezale˙zne od aryt-metyki Peana.

Podziekowania_,

Dziekuj_, e Pani Ma lgorzacie Maciejewskiej i Panom Tomaszowi Doma´_, nskiemu, Stanis lawowi Findeisenowi, Krzysztofowi Gerasowi, Danielowi Hansowi, Szczepanowi Hummelowi, Woj-ciechowi Jaworskiemu, Szymonowi Kitowskiemu, Micha lowi Kotowskiemu, Rados lawowi Ku-jawie, Micha lowi Misiakowi, Filipowi Murlakowi, Lukaszowi Osipiukowi, Paw lowi Parysowi, Jakubowi Pochrybniakowi, Micha lowi Rutkowskiemu, Aleksemu Schubertowi, Adamowi Slas-kiemu i Mateuszowi ZakrzewsSlas-kiemu za wykrycie rozmaitych b led´_, ow we wcze´sniejszych wers-jach tych notatek.