Polimorficzne osłabianie bez aksjomatu rozdzielności

Jacek Chrząszcz

Streszczenie

Relacja osłabiania polimorficznego w rachunku λ drugiego rzędu (system F), wprowadzona przez J. C. Mitchella, zdefiniowana jest przez cztery aksjomaty: zwrotności, instancjacji, generalizacji i rozdzielności oraz reguły przechodniości i domknięcia przez kontekst. Wiadomo, że relacja ta jest nierozstrzygalna, jednak wszystkie znane dotychczas dowody tego faktu istotnie wykorzystywały aksjomat rozdzielności.

Praca niniejsza pokazuje nierozstrzygalność relacji osłabiania polimorficznego, gdy usuniemy z jej definicji ten aksjomat. Ponadto przedstawiona jest również pełna równościowa charakteryzacja relacji równoważności indukowanej przez nową relację osłabiania.

Praca magisterska z informatyki

Wydział Matematyki, Informatyki i Mechaniki Uniwersystet Warszawski

Promotor: Paweł Urzyczyn

Warszawa, 10 września 1997

Podziękowania. Gorące podziękowania należą się mojemu promotorowi, Pawłowi Urzyczynowi, bez pomocy którego praca niniejsza nie mogłaby powstać. Jego słowa mobilizujące do pracy oraz cenne rady dochodziły do mnie nawet gdy dzieliły nas tysiące kilometrów. Pragnę również podziękować wszystkim członkom Zakładu Logiki Stosowanej za przyjacielską atmosferę i za to, że zawsze mogłem na nich liczyć. Wielką i bezcenną pomocą było również ciepło, którym otoczyli mnie moi najbliżsi. Dziękuję.

Spis rzeczy

1 Wprowadzenie 2 2 Notacja 6 3 Relacja osłabiania 7 4 Wyprowadzanie nierówności przez przepisywanie 7 5 Wyprowadzenia normalne 9 6 Typy bikoercyjne 12 7 Derywacje uporządkowane 17 8 Wymuszanie nierówności 19 9 Nierozstrzygalność relacji osłabiania 21 10 Podsumowanie 24

1 Wprowadzenie

Polimorficzne typy danych i polimorficzne procedury pojawiają się coraz częściej w dzisiejszej praktyce programowania. Zwykle jest to polimorfizm związany z programowaniem obiektowym, ale można znaleźć również konstrukcje do tworzenia typów i funkcji polimorficznych w sensie parametrycznym. Przykładem może być choćby znana z języka C++ konstrukcja template<par>Typ.

Oczywiście polimorfizm parametryczny występuje również w językach funkcyjnych, takich jak ML czy Haskell. Można znaleźć tam polimorficzne typy predefiniowane jak np. listy czy pary oraz konstrukcje do definiowania własnych algebraicznych typów z parametrami. Parametry w typach oznaczane są zmiennymi, a dla podkreślenia, że mogą one przyjmować dowolne wartości typowe, typy polimorficzne poprzedzane są jeszcze kwantyfikatorami. Wspomniany już polimorficzny typ listowy oznaczany jest ∀α (α list).

Jednak w systemie typów, używanym przez znane języki funkcyjne, mamy do czynienia z tzw. płytkim polimorfizmem. Oznacza to, że kwantyfikatory mogą występować w typach polimorficznych wyłącznie na najwyższym poziomie. Istnieją wprawdzie pewne eksperymentalne języki programowania, jak np. Quest autorstwa Giuseppe Longo i Luki Cardellego [CL91], które wyposażone są w polimorfizm wyższego rzędu, ale wszystkie popularne języki funkcyjne ograniczają sią do płytkiej wersji polimorfizmu. Inaczej jest w odmianie rachunku λ, zwanej systemem F (zob. np. [Gir89]), która uważana jest za model języka programowania z polimorficznymi typami wyższego rzędu. Typy są tu dowolnymi formułami logicznymi zbudowanymi ze zmiennych, symboli → oraz kwantyfikatorów.

System F ma jeszcze jedną ważną własność. W systemie tym, pomimo braku stałych typowych, można wyrazić wszystkie typy danych, a czyste λ-termy (również bez dodatkowych stałych) wyrażają niezbędne konstruktory. Na przykład wspomniany już typ listowy można zakodować w następujący sposób:

τ list = ∀γ (γ → (τ → γ → γ) → γ)

Konstruktory typu listowego: lista pusta nil : τ list oraz głowa listy cons : τ → τ list → τ list reprezentowane są przez następujące termy:

nil = Λγ.λn^{γ}.λc^{τ→γ→γ}.n
cons(h, t) = Λγ.λn^{γ}.λc^{τ→γ→γ}.c(h, tγ(n, c))

W tak rozbudowanym systemie narzuca się pytanie, czy termy danego typu σ nie mogą zastępować termow innego typu τ. Jeśli tak jest, mówimy, że typ σ jest bardziej ogólny od typu τ, lub że typ τ jest słabszy od typu σ. Oznaczamy to przez σ ⊑ τ. W klasycznym systemie F relację tę scharakteryzować można następującym aksjomatem:

∀α_{1} … α_{n} σ ⊑_{F} ∀β_{1} … β_{m} σ{α_{1} ↦ ρ_{1}, …, α_{n} ↦ ρ_{n}}  (1)

gdzie β_{1}, …, β_{m} nie są wolne w ∀α_{1} … α_{n} σ, a ρ_{1}, …, ρ_{n} są dowolnymi typami. Jednak relacji tej brakuje reguł kompozycjonalności. Nawet wiedząc, że σ ⊑_{F} σ′, nie można udowodnić, że τ → σ ⊑_{F} τ → σ′. John C. Mitchell w [Mit88] rozszerzył relację osłabiania do relacji ⊑_{M}, której definicja, oprócz aksjomatów podobnych do (1) zawiera również aksjomat rozdzielności kwantyfikatora oraz reguły domykania przez kontekst, z których najważniejszą jest reguła (→-kontekst) antymonotoniczna ze względu na pierwszy argument i monotoniczna ze względu na drugi, tzn.

σ_{1} → τ_{1} ⊑_{M} σ_{2} → τ_{2} jeśli σ_{2} ⊑_{M} σ_{1} oraz τ_{1} ⊑_{M} τ_{2}

Praca Mitchella zawiera również dowód pełności relacji ⊑_{M} względem semantyki osłabiania. Nierówność σ ⊑_{M} τ da się wyprowadzić wtedy i tylko wtedy, gdy we wszystkich prostych modelach inferencji^{1} zachodzi D_{⟦σ⟧} ⊆ D_{⟦τ⟧}, gdzie D_{⟦ρ⟧} jest zbiorem znaczeń wszystkich λ-termów typu ρ.

System F, wzbogacony o regułę osłabiania używającą nowej relacji ⊑_{M}

\frac{E ⊢ M : σ σ ⊑_{M} τ}{E ⊢ M : τ}

jest właściwym rozszerzeniem klasycznego systemu F. Istnieją nawet termy typowalne w nowym systemie, które nie są typowalne w systemie klasycznym. To samo rozszerzenie, jak dowodzi Mitchell, uzyskać można dodając do klasycznego systemu F regułę wnioskowania

(eta)  \frac{E ⊢ M : σ M ⟶_{η} N}{E ⊢ N : σ}

opartą o regułę redukcji λx.Mx ⟶_{η} M jeśli x nie występuje wolno w M.

Równoważność tych dwóch rozszerzeń wynika z faktu, że jeśli σ ⊑_{M} τ, to istnieje funkcja zmiany typu V : σ → τ, zwana koercją, taka że V jest ηredukowalne do identyczności, po wytarciu informacji typowych.

Główną wadą rozszerzonego systemu F_{η}, jak również klasycznego systemu F jest nierozstrzygalność większości ważnych problemów dotyczących tych systemów. I tak, dla systemu F, nierozstrzygalność problemów sprawdzania i rekonstrukcji typów została udowodniona przez Joe Wellsa w pracy [Wel94]. Pewną nadzieją dla systemu F_{η} była praca Trevora Jima [Jim95], który zbudował redukcję rekonstrukcji typów dla systemu F_{η} do nierówności ⊑_{M}. Niestety praca Jerzego Tiuryna i Pawła Urzyczyna [TU95] pokazuje nierozstrzygalność relacji ⊑_{M}, co implikuje również nierozstrzygalność sprawdzania typów. Na koniec Wells udowodnił w [Wel96], że rekonstrukcja typów również jest nierozstrzygalna.

Wspomniana praca Tiuryna i Urzyczyna [TU95] zawiera redukcję problemu stopu maszyny dwulicznikowej do nierówności ⊑_{M}. Jako element pośredni, autorzy definiują maszynę rejestrów stosowych. Jest to deterministyczna maszyna z jednym stanem i skończoną liczbą rejestrów, która działając zdejmuje instrukcje z pierwszego rejestru stosowego i wykonuje je modyfikując odpowiednio zawartość wszystkich rejestrów. Zatrzymuje się po przeczytaniu wyróżnionej instrukcji końcowej. Problem stopu tej maszyny jest nierozstrzygalny, gdyż może ona symulować dowolną deterministyczną maszynę dwulicznikową.

1ang. simple inference model

Autorzy prezentują kodowanie chwilowej konfiguracji maszyny w postaci dwóch typów σ i τ w taki sposób, że nierówność σ ⊑_{M} τ zachodzi wtedy i tylko wtedy, gdy konfiguracja ta prowadzi do zatrzymania maszyny. Dowód powyższego opiera się w ich pracy na pojęciu wagi nierówności zdefiniowanej na podstawie alternatywnego systemu wyprowadzania nierówności ⊑_{M}, zaproponowanego przez Longo, Milsted i Sołowiewa w pracy [LMS95]. Dzięki udowodnionym przez nich pewnym własnościom relacji ⊑_{M} oraz wyprowadzeń w systemie Longo-Milsted-Sołowiew, autorzy pokazują następujący lemat:

Niech σ_{1} i τ_{1} kodują daną chwilową konfigurację maszyny. Jeśli konfiguracja ta doprowadza do zatrzymania w jednym kroku, to trywialnie σ_{1} ⊑_{M} τ_{1}. W przeciwnym wypadku łatwo ustalić parę typów σ_{2} i τ_{2}, kodującą konfigurację po jednym kroku i to w taki sposób, że nierówność σ_{1} ⊑_{M} τ_{1} zachodzi wtedy i tylko wtedy, gdy σ_{2} ⊑_{M} τ_{2}. Ponadto, jeśli obie nierówności zachodzą, waga pierwszej jest ostro większa od wagi drugiej.

Z lematu tego wynika, że jeśli nierówność kodująca bieżącą konfigurację chwilową maszyny zachodzi, to ponieważ za każdym krokiem maszyny waga nierówności kodującej maleje, więc maszyna nie może działać w nieskończoność. W drugą stronę, jeśli maszyna zatrzymuje się, to skoro nierówność kodująca jest prawdziwa dla konfiguracji końcowej, to również dla wszystkich ją poprzedzających.

Istota tego dowodu nierozstrzygalności polega na tym, iż nie da się ograniczyć stopnia zagnieżdżenia instancjacji niezbędnych do udowodnienia nierówności kodujących konfiguracje prowadzące do zatrzymania maszyny. System Longo-Milsted-Sołowiew zawiera regułę (∀-lewy), która mówi, że aby udowodnić nierówność ∀α σ ⊑_{M} τ, wystarczy najpierw pokazać σ{α ↦ ξ} ⊑_{M} τ dla jakiegoś typu ξ.

Każdy krok maszyny, który intuicyjnie odpowiada pewnemu fragmentowi dowodu nierówności kodującej pierwotną konfigurację, powoduje konieczność użycia tej reguły. Ponadto przy kolejnym kroku maszyny, reguła ta będzie używana jak gdyby wewnątrz wstawionego typu ξ.

Inny dowód nierozstrzygalności relacji ⊑_{M} zawiera praca Wellsa [Wel95]. Tutaj niemożność decyzji, czy dane dwa typy są w relacji ⊑_{M}, wynika nie z faktu, że nie da się przewidzieć koniecznego stopnia zagnieżdżenia instancjacji, lecz z tego, że nie da się oszacować rozmiarów typów wstawianych (oznaczanych powyżej przez ξ). Wells używa problemu semi-unifikacji, który jest następujący:

Mając dane dwie pary termów σ_{1}, τ_{1} i σ_{2}, τ_{2}, zbudowanych ze zmiennych i symboli → rozstrzygnąć, czy istnieje podstawienie θ takie, że dla pewnych podstawień θ_{1} i θ_{2} zachodzą równości σ_{1}θθ_{1} = τ_{1}θ oraz σ_{2}θθ_{2} = τ_{2}θ.

Nierozstrzygalność tego problemu również wynika z nieprzewidywalności rozmiaru pierwszego podstawienia θ.

Redukcja polega na uniwersalnej konstrukcji typu Π(δ_{1}, ζ_{1}, δ_{2}, ζ_{2}) takiego, że jeśli γ⃗ są wszystkimi zmiennymi występującymi w σ_{1}, τ_{1}, σ_{2}, τ_{2}, to nierówność

∀β (Π(β, β, β, β) → ⊥) ⊑_{M} (∀γ⃗ Π(σ_{1}, τ_{1}, σ_{2}, τ_{2})) → ⊥  (2)

zachodzi wtedy i tylko wtedy, gdy czwórka σ_{1}, τ_{1}, σ_{2}, τ_{2} jest semi-unifikowalna.

Istota równoważności polega na tym, że wspólne podstawienie θ wymuszone jest przez wspólne kwantyfikowanie zmiennych wolnych γ⃗ we wszystkich czterech typach σ_{1}, τ_{1}, σ_{2}, τ_{2}. Następnie, dzięki aksjomatowi rozdzielności kwantyfkatora ∀α (ρ_{1} → ρ_{2}) ⊑_{M} ∀α ρ_{1} → ∀α ρ_{2}, podstawienia θ_{1} i θ_{2}, odpowiednio w σ_{1}θ i w σ_{2}θ, mogą być wykonane niezależnie. Dzięki odpowiedniemu ustawieniu typów σ_{1}, τ_{1}, σ_{2}, τ_{2} w Π(σ_{1}, τ_{1}, σ_{2}, τ_{2}) oraz dzięki nowemu systemowi wyprowadzania nierówności ⊑_{M}, wyrażenie (2) może być wyprowadzone tylko na jeden sposób.

Pomimo nierozstrzygalności relacji ⊑_{M}, w językach posiadających polimorficzne typy wyższego rzędu zachodzi potrzeba odpowiadania na pytanie, czy dany term U, posiadający typ σ może być użyty w miejscu, gdzie wymagany jest typ τ. Narzuca się więc problem znalezienia nietrywialnej rozstrzygalnej relacji osłabiania ⊑, zawartej w oryginalnej relacji osłabiania Mitchella. Pierwszą nieudaną próbą jest usunięcie z definicji ⊑_{M} najmniej intuicyjnie jasnego aksjomatu rozdzielności.

W kodowaniu semi-unifikacji Wellsa aksjomat ten jest kluczowy. Bez niego nie można, po wspólnym podstawieniu θ, dokonać dwóch niezależnych podstawień θ_{1} i θ_{2}. W pracy Tiuryna i Urzyczyna natomiast, aksjomat rozdzielności nie wydaje się niezbędnym w kodowaniu obliczeń maszyny, ale ponieważ jest on ukryty w systemie Longo-Milsted-Sołowiew, bez tego aksjomatu, dowód odpowiednich własności nowej relacji ⊑ należy przeprowadzić inaczej.

Dlatego niniejsza praca, oparta o kodowanie problemu stopu maszyny rejestrów stosowych z pracy [TU95], definiuje pojęcie wagi nierówności w oparciu o pewną klasę wyprowadzeń w systemie przepisywania typów, łatwo wynikającym z oryginalnych aksjomatów Mitchella. Pozostałe własności potrzebne w kodowaniu obliczeń maszyny, udowodnione są przy pomocy jeszcze węższej podklasy wyprowadzeń.

Po niniejszym wstępie, rozdział 2 wprowadza formalnie podstawowe pojęcia i oznaczenia, z których będziemy korzystać. Kolejne dwa rozdziały prezentują oryginalny system Mitchella, który po usunięciu aksjomatu rozdzielności, definiuje rozpatrywaną relację osłabiania ⊑ oraz blisko z nim związany system przepisywania typów.

W rozdziale 5 określony jest warunek, jaki muszą spełniać wyprowadzenia normalne w tym systemie, a następnie lemat 5.4 pokazuje, że klasa ta wystarcza do dowodzenia nierówności typowych i dlatego w oparciu o nią może być zdefiniowane pojęcie wagi nierówności.

Rozdział 6 poświęcony jest relacji równoważności związanej z quasi-porząd-kiem ⊑. Dowiedzione są wszystkie potrzebne w dalszym ciągu pracy własności tej relacji oraz dodatkowo podana jest jej pełna równościowa charakteryzacja, na wzór podanej przez Tiuryna w [Tiu95] charakteryzacji relacji równoważności ∼_{M} związanej z oryginalną relacją Mitchella.

W rozdziale 7 ze wszystkich normalnych wyprowadzeń wydzielone są wyprowadzenia uporządkowane, podklasa potrzebna w rozdziale 8 do dowiedzenia własności relacji ⊑ bezpośrednio wykorzystywanych w kodowaniu maszyny rejestrów stosowych. Szkic tego kodowania, na podstawie pracy [TU95], podany jest w rozdziale 9, po którym następuje podsumowanie.

2 Notacja

Będziemy pracować z typami polimorficznego rachunku λ (system F), zdefiniowanymi na podstawie przeliczalnego zbioru zmiennych V przez następującą gramatykę:

T ::= V | ∀V T | T → T

Zmienne występujące w typach oznaczane będą literami z początku alfabetu greckiego α, β, γ, ciągi zmiennych kwantyfikowanych δ⃗, ζ⃗, ϑ⃗, a typy innymi literami greckimi, jak σ, τ, ρ… Często typ ∀α∀β τ zapisywany będzie w skrócie jako ∀αβ τ. Przyjmujemy, że kwantyfikatory wiążą silniej niż operator → oraz że symbol ⊥ oznacza typ ∀α α.

Liczbę symboli → występującą w danym typie nazwiemy jego wagą. Definicja indukcyjna jest nastepująca:

waga(α) = 0
waga(∀α σ) = waga(σ)
waga(σ_{1} → σ_{2}) = waga(σ_{1}) + waga(σ_{2}) + 1

Ze względu na obecność kwantyfikatorów, zmienne występujące w danym typie dzielimy na zmienne związane oraz zmienne wolne, czyli nie związane przez żaden kwantyfikator. Dla danego typu σ, zbiór zmiennych wolnych występujących w tym typie oznaczany będzie przez F V (σ). Formalnie definiujemy:

F V (α) = {α}
F V (σ_{1} → σ_{2}) = F V (σ_{1}) ∪ F V (σ_{2})
F V (∀β σ) = F V (σ) \ {β}

Typy różniące się jedynie nazwami zmiennych związanych będziemy uznawać za równe. Będziemy również przyjmować, że w każdym typie zmienne wolne mają inne nazwy, niż zmienne związane oraz że nazwy różnych zmiennych związanych nie pokrywają się.

Funkcję częściową o skończonej dziedzinie ze zbioru zmiennych V w zbiór typów T nazywamy podstawieniem. Dowolne podstawienie θ przedłuża się w naturalny sposób do funkcji ze zbioru T w zbiór T . Wynikiem aplikacji podstawienia θ do typu σ, co będziemy oznaczać postfiksowo σθ będzie typ σ zmodyfikowany w taki sposób, że zamiast każdego wystąpienia zmiennej wolnej α należącej do dziedziny θ wystąpi wartość θ na tej zmiennej. Pozostałe zmienne wolne w σ oraz zmienne związane pozostają bez zmian. Ponadto dokonując niezbędnych przemianowań zmiennych związanych, gwarantujemy, że zmienne wolne w typach αθ pozostają wolne w typie σθ. Podstawienie θ o dziedzinie α_{1}, …, α_{n}, takie że α_{i}θ = τ_{i} dla każdego i, będzie również oznaczane {α_{1} ↦ τ_{1}, …, α_{n} ↦ τ_{n}}. W zapisie operacja podstawienia wiązać będzie silniej niż kwantyfikatory i dlatego w typie ∀β σ{α ↦ ξ} wolne wystąpienia zmiennej β w typie ξ znajdą się w zasięgu kwantyfikatora ∀β.

Typy polimorficzne możemy również utożsamiać z drzewami etykietowanymi. W liściach znajdują się zmienne, w węzłach wewnętrznych symbole →, oraz każdy wierzchołek jest etykietowany skończonym ciągiem kwantyfikatorów.

Zbiór pozycji w takim drzewie możemy zatem utorzsamiać ze skończonym zbiorem skończonych łańcuchów nad alfabetem {0, 1}. Pozycje, które mają parzystą liczbę zer nazywane są pozytywnymi, a te które maja nieparzystą liczbę zer, to pozycje negatywne. Łańcuch pusty będziemy oznaczali przez ϵ, a mając dane dwa łańcuchy p_{1} i p_{2} ich konkatenacja oznaczana będzie p_{1}p_{2}.

Pozycje będziemy porównywać między sobą przy pomocy dwóch różnych częściowych porządków. Porządek prefiksowy będzie oznaczany ≤, a zapis p ≹ r będzie oznaczać, że p i r są nieporównywalne. Drugim używanym porządkiem będzie porządek leksykograficzny, oznaczany ⪯, indukowany przez 0 ≺ 1.

Jeśli σ jest typem, a p pozycją w drzewie σ, przez σ|_{p} oznaczamy poddrzewo na pozycji p. Jeśli σ i ϱ są typami oraz p jest pozycją w drzewie σ, to σ[ϱ]_{p} oznacza typ σ z poddrzewem na pozycji p zastąpionym przez ϱ. W odróżnieniu od podstawienia, przy tej operacji niektóre zmienne wolne typu ϱ mogą znaleźć się w zasięgu kwantyfikatorów z σ.

3 Relacja osłabiania

Relacja osłabiania ⊑, której będziemy używać, zdefiniowana jest przez 3 aksjomaty i 3 reguły:

(zwr) σ ⊑ σ
(inst) ∀α σ ⊑ σ{α ↦ ρ}
(kwant) σ ⊑ ∀α σ jeśli α ∉ F V (σ)

Reguły:

(→-kontekst) \frac{σ_{2} ⊑ σ_{1} τ_{1} ⊑ τ_{2}}{σ_{1} → τ_{1} ⊑ σ_{2} → τ_{2}}
(∀-kontekst) \frac{σ ⊑ τ}{∀α σ ⊑ ∀α τ}
(przech) \frac{σ ⊑ ρ ρ ⊑ τ}{σ ⊑ τ}

W oryginalnej relacji osłabiania na typach polimorficznych, wprowadzonej przez Mitchella w [Mit88] był jeszcze aksjomat

(rozdz) ∀α(σ → τ) ⊑_{M} σ → ∀α τ jeśli α ∉ F V (σ)

4 Wyprowadzanie nierówności przez przepisywanie

Z przyczyn technicznych zamiast wyprowadzeń w powyższym systemie wygodniej nam będzie używać przepisywania termów zgodnie z podanymi niżej regułami:

\begin{aligned}C^{+}[∀α σ] & ⟹_{i}^{+} & C^{+}[σ\{α ↦ ρ\}] \\ C^{+}[σ] & ⟹_{q}^{+} & C^{+}[∀α σ] \\ & & jeśli α ∉ F V (σ) \end{aligned}  \begin{aligned}C^{−}[σ\{α ↦ ρ\}] & ⟹_{i}^{−} & C^{−}[∀α σ] \\ C^{−}[∀α σ] & ⟹_{q}^{−} & C^{−}[σ] \\ & & jeśli α ∉ F V (σ) \end{aligned}

gdzie C^{+}[ ] i C^{−}[ ] oznaczają dowolny kontekst z dziurą na pozycji dodatniej i, odpowiednio, ujemnej. Jeśli pozycja ta jest istotna, będziemy ją umieszczać nad strzałką, np. σ =^{p} ⟹_{q}^{+} τ i nazywać pozycją danego kroku. Oznaczmy teraz dowolny krok dodatni przez ⟹^{+} oraz dowolny krok ujemny przez ⟹^{−}. Niech ⟹ oznacza dowolny krok przepisywania oraz ⟹ ⟹ dowolną skończoną liczbę kroków. Wagą kroku σ ⟹ τ nazwiemy wartość bezwzględną z różnicy wag σ i τ, czyli intuicyjnie liczbę symboli → wprowadzonych przez ten krok.

Znaczenie wprowadzonego systemu przepisywania wyraża formalnie następujący prosty lemat:

Lemat 4.1 Dla dowolnych dwóch typów σ i τ zachodzi:

σ ⊑ τ wtedy i tylko wtedy, gdy σ ⟹ ⟹ τ

Dowód. Załóżmy, że σ ⊑ τ. Udowodnimy przez indukcję ze względu na budowę dowodu tego faktu, że σ ⟹ ⟹ τ. Przypadek bazowy, to zastosowanie aksjomatu. Jeśli był to aksjomat (zwr), to σ = τ, w przypadku pozostałych aksjomatów

σ =^{ϵ} ⟹^{+} τ.

Jeśli ostatnio zastosowaną regułą było (przech), to znaczy z założenia indukcyjnego, że istnieje ρ takie, że σ ⟹ ⟹ ρ oraz ρ ⟹ ⟹ τ. Wynika stąd natychmiast, że σ ⟹ ⟹ τ.

Jeśli zastosowano regułę (∀-kontekst), to znaczy, że σ = ∀α σ′, τ = ∀α τ′ oraz z indukcji, że σ′ ⟹ ⟹ τ′. Wynika z tego oczywiście, że ∀α σ′ ⟹ ⟹ ∀α τ′.

Zastosowanie reguły (→-kontekst) wymaga nieco więcej wyjaśnień. Wiemy, że σ = σ_{1} → σ_{2} i τ = τ_{1} → τ_{2}. Z założenia indukcyjnego wiemy również, że istnieją wyprowadzenia

τ_{1} =^{p_{1}} ⟹ ⋯ =^{p_{n}} ⟹ σ_{1}  oraz  σ_{2} =^{s_{1}} ⟹ ⋯ =^{s_{m}} ⟹ τ_{2}

Na podstawie tych dwóch wyprowadzeń, można skonstruować następujące:

σ_{1} → σ_{2} =^{0p_{n}} ⟹ ⋯ =^{0p_{1}} ⟹ τ_{1} → σ_{2} =^{1s_{1}} ⟹ ⋯ =^{1s_{m}} ⟹ τ_{1} → τ_{2}

Pierwszy ciąg, to kroki z wyprowadzenia τ_{1} =^{p_{1}} ⟹ ⋯ =^{p_{n}} ⟹ σ_{1} w których na skutek dodania ścieżkom początkowego symbolu 0 zmieniono znaki z + na − i odwrotnie. Kroki te ustawione są w odwrotnej kolejności i w odwrotnym kierunku.

Dla dowodu implikacji w drugą stronę, wystarczy pokazać, że jeśli σ ⟹ τ, to σ ⊑ τ. Przypuśćmy, że σ = C[σ′] =^{p} ⟹ C[τ′] = τ. Zastosujemy indukcję ze względu na budowę kontekstu C[ ]. Jeśli jest on pusty, to σ ⊑ τ dzięki aksjomatowi (kwant) lub (inst).

W przeciwnym przypadku są dwie możliwości. Jeżeli C[ ] = ∀α C′[ ], to z założenia indukcyjnego C′[σ′] ⊑ C′[τ′] i wówczas tezę dostajemy dzięki regule (∀-kontekst). Jeśli natomiast pierwszym symbolem w C[ ] jest →, to należy rozpatrzyć dwa przypadki. Jeśli p = 0p′ dla jakiegoś p′, to C[ ] = C_{0}[ ] → ρ

i wówczas C_{0}[τ′] =^{p′} ⟹ C_{0}[σ′], ponieważ znak p′ jest przeciwny do znaku p. Z założenia indukcyjnego C_{0}[τ′] ⊑ C_{0}[σ′] i, jako że ρ ⊑ ρ, na mocy reguły (→- kontekst),

C_{0}[σ′] → ρ ⊑ C_{0}[τ′] → ρ

Podobnie, jeśli p = 1p′, wówczas C[ ] = ρ → C_{1}[ ] i z indukcji C_{1}[σ′] ⊑ C_{1}[τ′]. Po zastosowaniu aksjomatu (zwr) do typu ρ i reguły (→-kontekst), dostajemy

ρ → C_{1}[σ′] ⊑ ρ → C_{1}[τ′]
■

5 Wyprowadzenia normalne

Celem niniejszego rozdziału jest pokazanie, że każdą nierówność da się udowodnić za pomocą wyprowadzenia normalnego, tj. sekwencji kroków dodatnich (które zwiększają rozmiar typu), po której następuje sekwencja kroków ujemnych.

Definicja 5.1 (wyprowadzenia normalne)

Wyprowadzenie σ ⟹ ⟹ τ nazywamy wyprowadzeniem normalnym, jeśli jest ono postaci σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ dla pewnego typu ρ.

Wagą wyprowadzenia normalnego σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ nazwiemy sumę wag poszczególnych kroków. Łatwo pokazać, że jest ona równa 2×waga(ρ)−waga(σ)− waga(τ).

Zanim pokażemy, jak doprowadzić dowolne wyprowadzenie do postaci normalnej, zdefiniujemy najpierw pojęcie bezpiecznych kroków.

Definicja 5.2 (bezpieczne kroki)

Krok σ ⟹ τ jest krokiem bezpiecznym, jeśli spełniony jest jeden z następujących warunków

1. jest to krok ⟹_{q};

2. jest to krok ⟹_{i}, w którym typem wstawianym jest ⊥;

3. jest to krok =^{p} ⟹_{i}, w którym typem wstawianym jest zmienna β, związana na pozycji p′ ≤ p, jeśli znak p′ jest ten sam, co znak p.

Do drugiego rodzaju kroków bezpiecznych zaliczymy w szczególności wszystkie instancjacje pustych kwantyfikatorów, to znaczy kroki C^{+}[∀α σ] ⟹_{i}^{+} C^{+}[σ] oraz odpowiednio C^{−}[σ] ⟹_{i}^{−} C^{−}[∀α σ] dla α ∉ F V (σ).

W ostatnim punkcie definicji bezpiecznych kroków, chodzi o sytuacje następujące:

C^{+}[∀β C^{+}[∀α σ]] ⟹_{i}^{+} C^{+}[∀β C^{+}[σ{α ↦ β}]]
C^{−}[∀β C^{+}[σ{α ↦ β}]] ⟹_{i}^{−} C^{−}[∀β C^{+}[∀α σ]]

Wszystkie kroki bezpieczne mają wagę 0. Ich nazwa wynika z faktu, że wsortowanie ich w normalne wyprowadzenie nie zmienia jego wagi. Formalne sformułowanie tej własności, jak również przykład kroku o wadze 0, który nie jest bezpieczny, zostaną podane na końcu niniejszego rozdziału.

Poniższy lemat pokazuje jak zamieniać miejscami kroki ujemne z dodatnimi,^{2} co jest niezbędne do przekształcania wyprowadzeń do postaci normalnej.

Lemat 5.3 (zamiana kroków ujemnych i dodatnich)

Niech σ i τ będą typami takimi, że σ ⟹^{−} ρ ⟹^{+} τ. Wtedy istnieje typ ρ′ taki, że σ ⟹^{+} ρ′ ⟹^{−} τ. Ponadto jeśli krok σ ⟹^{−} ρ był bezpieczny, to po zamianie krok ρ′ ⟹^{−} τ też będzie bezpieczny i podobnie jeśli krok ρ ⟹^{+} τ był bezpieczny, to krok σ ⟹^{+} ρ′ również taki będzie.

Dowód. Niech p i r będą odpowiednio ścieżkami pierwszego i drugiego kroku. W zależności od wzajemnego położenia tych pozycji oraz od rodzaju kroków wyróżniamy następujące przypadki :

• p ≹ r — wtedy zamiana kroków nie stanowi problemu, kroki bezpieczne zostają bezpiecznymi;

• p < r, r = p · s. Jeśli obydwa kroki są rodzaju ⟹_{q}, zmiana kolejności nie stanowi problemu. Jeśli pierwszy krok jest rodzaju ⟹_{i}, a drugi ⟹_{q}, to mamy następującą sytuację:

σ = σ[∀δ⃗ ϱ[∀ζ⃗ υ]_{s}{α ↦ ξ}]_{p}  =^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗ υ]_{s}]_{p}
=^{r} ⟹_{q}^{+} σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{s}]_{p} = τ

Ponieważ β jest nową zmienną, możemy przyjąć, że β nie występuje w F V (ξ), a więc i w F V (υ{α ↦ ξ}). Mamy zatem

σ = σ[∀δ⃗ ϱ[∀ζ⃗ υ]_{s}{α ↦ ξ}]_{p}  =^{r} ⟹_{q}^{+} σ[∀δ⃗ ϱ[∀ζ⃗β υ]_{s}{α ↦ ξ}]_{p}
=^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{s}]_{p} = τ

Jeśli zachodzi sytuacja odwrotna, tzn. pierwszy krok jest rodzaju ⟹_{q}, a drugi ⟹_{i}, mamy

σ = σ[∀δ⃗β ϱ[∀ζ⃗α υ]_{s}]_{p}  =^{p} ⟹_{q}^{−} σ[∀δ⃗ ϱ[∀ζ⃗α υ]_{s}]_{p}
=^{r} ⟹_{i}^{+} σ[∀δ⃗ ϱ[∀ζ⃗ υ{α ↦ ξ}]_{s}]_{p} = τ

Ponieważ β nie występuje w ϱ, możemy przyjąć, iż nie występuje również w ξ, a zatem β ∉ F V (ϱ[∀ζ⃗ υ{α ↦ ξ}]_{s}). Mamy więc

σ = σ[∀δ⃗β ϱ[∀ζ⃗α υ]_{s}]_{p}  =^{r} ⟹_{i}^{+} σ[∀δ⃗β ϱ[∀ζ⃗ υ{α ↦ ξ}]_{s}]_{p}
=^{p} ⟹_{q}^{−} σ[∀δ⃗ ϱ[∀ζ⃗ υ{α ↦ ξ}]_{s}]_{p} = τ

W obydwu powyższych sytuacjach typ podstawiany (oznaczany ξ) nie zmieniał się, zatem kroki bezpieczne pozostawały bezpiecznymi.

kroków ∀α α =^{ϵ} ⟹_{i}^{+} (β → β) → β =^{0} ⟹_{i}^{−} (∀α α) → β

2W drugą stronę zamiana nie zawsze jest możliwa. Nie da się np. odwrócić kolejności

Jeśli obydwa kroki są rodzaju ⟹_{i} mamy

σ = σ[∀δ⃗ ϱ[∀ζ⃗β υ]_{s}{α ↦ ξ_{α}}]_{p}  =^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{s}]_{p}
=^{r} ⟹_{i}^{+} σ[∀δ⃗α ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{s}]_{p} = τ

Wiemy, że β ∉ F V (ξ_{α}), ale α może wystąpić w ξ_{β}. Przyjmując ϱ̄ = ϱ{α ↦ ξ_{α}} oraz ῡ = υ{α ↦ ξ_{α}}, możemy zamienić te kroki w następujący sposób:

σ = σ[∀δ⃗ ϱ̄[∀ζ⃗β ῡ]_{s}]_{p}  =^{r} ⟹_{i}^{+} σ[∀δ⃗ ϱ̄[∀ζ⃗ ῡ{β ↦ ξ_{β}{α ↦ ξ_{α}}}]_{s}]_{p}
= σ[∀δ⃗ ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{s}{α ↦ ξ_{α}}]_{p}
=^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{s}]_{p} = τ

gdzie środkowa równość jest prostą własnością podstawienia. Jeśli krok ujemny był bezpieczny, to i takim pozostanie, ponieważ podstawiany typ (oznaczany ξ_{α}) nie zmienił się. Jeśli krok dodatni był bezpieczny, to ξ_{β} = ⊥ lub ξ_{β} = γ dla jakiejś zmiennej γ związanej na pozycji dodatniej; w obu przypadkach α ∉ F V (ξ_{β}), a więc ξ_{β}{α ↦ ξ_{α}} = ξ_{β};

• p > r. W tej sytuacji patrzymy na dowód dualny, tzn. jeśli

σ =^{p} ⟹^{−} ρ =^{r} ⟹^{+} τ

to również dualnie

τ → ⊥ =^{0r} ⟹^{−} ρ → ⊥ =^{0p} ⟹^{+} σ → ⊥

gdzie oczywiście 0r < 0p, więc możemy skorzystać z poprzedniego przypadku. ■

Lemat 5.4 Jeśli dane są dwa typy σ i τ, takie że σ ⊑ τ, to istnieje normalne wyprowadzenie σ ⟹ ⟹^{+} ⟹ ⟹^{−} τ.

Dowód. Ponieważ dla danych typów σ i τ istnieje jakieś wyprowadzenie, wystarczy użyć odpowiednią liczbę razy Lematu 5.3, otrzymując wyprowadzenie normalne. ■

Po dowiedzeniu powyższego bardzo istotnego faktu możemy zdefiniować wagę nierówności

Definicja 5.5 (waga nierówności)

Waga nierówności σ ⊑ τ to minimalna waga jej wyprowadzenia normalnego σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ.

Po podaniu powyższej definicji możemy formalnie wyjaśnić znaczenie nazwy kroków bezpiecznych

Stwierdzenie 5.6 Niech σ_{1} ⊑ τ i niech σ_{0} ⟹ σ_{1} będzie bezpiecznym krokiem. Wówczas waga nierówności σ_{0} ⊑ τ jest nie większa od wagi nierówności σ_{1} ⊑ τ.

Dowód. Stwierdzenie to wynika bezpośrednio z Lematu 5.3. ■

Podamy teraz przykład kroku o wadze 0, który nie jest bezpieczny. Rozpatrzmy następujące jednokrokowe wyprowadzenie o wadze waga(ξ):

∀α (∀β (⊥ → β) → α) =^{ϵ} ⟹_{i}^{+} ∀β (⊥ → β) → ξ

Jeśli poprzedzimy je krokiem o zerowej wadze

∀α ((⊥ → α) → α) = ∀α ((⊥ → β){β ↦ α} → α) =^{0} ⟹_{i}^{−} ∀α (∀β (⊥ → β) → α)

to dostaniemy wyprowadzenie, w którym krok ujemny poprzedza krok dodatni. Pierwszy krok nie jest bezpieczny, gdyż zmienna α jest związana na pozycji dodatniej ϵ, a nie ujemnej, tak jak zmienna β. Po zamianie tych kroków zgodnie z Lematem 5.3, otrzymujemy wyprowadzenie

∀α ((⊥ → α) → α) =^{ϵ} ⟹_{i}^{+} ((⊥ → ξ) → ξ) =^{0} ⟹_{i}^{−} ∀β (⊥ → β) → ξ

którego waga jest równa 3 × waga(ξ), czyli więcej niż waga pierwotnego kroku dodatniego, o ile tylko waga(ξ) > 0.

6 Typy bikoercyjne

Typy σ i τ określamy jako bikoercyjne, jeśli σ ⊑ τ i τ ⊑ σ. Pokażemy w niniejszym rozdziale, że relacja bikoercyjności może być utożsamiana z najmniejszą kongruencją zawierającą aksjomaty

(B1) ∀α∀β σ ∼ ∀β∀α σ

(B2) ∀α σ ∼ σ{α ↦ ⊥} (jeśli wszystkie wystąpienia α w σ są pozytywne)

Relacja równoważności związana z oryginalnym systemem Mitchella została scharakteryzowana przez Tiuryna w pracy [Tiu95]. Definiowana jest ona przez aksjomaty (B1), (B2) oraz aksjomat

(B3) ∀α (σ_{1} → σ_{2}) ∼_{M} σ_{1} → ∀α σ_{2} (jeśli α ∉ F V (σ_{1}))

który w naszym systemie nie jest prawdziwy.^{3} Dalsza część niniejszego rozdziału poświęcona jest dowodowi faktu, że relacja ∼ definiowana jako najmniejsza kongruencja zawierająca aksjomaty (B1) i (B2), jest relacją równoważności indukowaną przez quasi-porządek ⊑. Aby to udowodnić, wprowadzimy pojęcie kroków odwracalnych.

Definicja 6.1 (kroki odwracalne)

Pojedynczy krok redukcji σ ⟹ τ nazwiemy odwracalnym, jeśli τ ⊑ σ.

Lemat 6.2 Niech σ ⟹_{i}^{+} τ i niech p i r będą takie, że σ|_{pr} = ∀δ⃗α, gdzie α jest zmienną związaną na pozycji dodatniej p. Jeśli w τ na pozycji pr nie występuje zmienna związana na pozycji dodatniej, to krok σ ⟹_{i}^{+} τ nie jest odwracalny.

3Nie jest prawdą, że ∀α (β → (α → β)) ∼ β → ∀α (α → β)

Dowód. Załóżmy, że krok ten jest odwracalny, czyli że τ ⊑ σ. Istnieje zatem wyprowadzenie normalne, τ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ.

Jeśli τ|_{pr} = ∀δ⃗ζ⃗ β, gdzie β jest zmienną wolną lub związaną na pozycji ujemnej, to również ρ|_{pr} = ∀δ⃗ζ⃗ β, ponieważ w fazie dodatniej zmienne związane na pozycjach ujemnych nie są instancjowane, a zmienne wolne w ogóle nie mogą być instancjowane.

Jeśli natomiast τ|_{pr} = ∀δ⃗ζ⃗ (ξ_{1} → ξ_{2}), dla jakichś ξ_{1}, ξ_{2}, to podobnie ρ|_{pr} = ∀δ⃗ζ⃗ (ξ′_{1} → ξ′_{2}) (dla jakichś ξ′_{1}, ξ′_{2}), ponieważ w fazie dodatniej waga typu nie maleje, czyli symbol → nie może zostać zastąpiony zmienną.

Zatem ρ|_{pr} nie jest zmienną związaną na pozycji dodatniej. Wynika z tego również, że σ|_{pr} nie jest zmienną związaną na pozycji dodatniej, ponieważ kroki ⟹_{q}^{−} nie mają wpływu na wiązanie zmiennych, a kroki ⟹_{i}^{−} nie tworzą nowych zmiennych związanych na pozycji dodatniej. Sprzeczność. ■

W kolejnym lemacie skorzystamy z następującego oznaczenia. Niech σ będzie typem, w którym na pozycji s znajduje się zmienna α, związana przez kwantyfikator na pozycji p (oczywiście p ≤ s). Wówczas niech Π_{σ}(s) oznacza zbiór pozycji wszystkich wystąpień zmiennej α (związanej przez kwantyfikator ∀α z pozycji p) w typie σ. Jeśli z kontekstu będzie wynikało o jaki typ chodzi, indeks σ zostanie opuszczony.

Lemat 6.3 Niech σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ będzie dowolnym normalnym wyprowadzeniem nierówności σ ⊑ σ. Niech p będzie pozycją dodatnią, a r takie, że pr jest pozycją ujemną i σ|_{pr} = ∀ϑ⃗ α, gdzie α jest zmienną związaną na pozycji dodatniej p. Wówczas w każdym typie w wyprowadzeniu σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ na pozycji pr występuje zmienna związana przez kwantyfikator z pozycji p, a zbiór Π(pr) nie ulega zmianie.

Dowód. Wszystkie kroki w rozpatrywanym wyprowadzeniu

σ = σ_{0} ⟹^{+} σ_{1} ⟹^{+} ⋯ ⟹^{+} σ_{n} = ρ ⟹ ⟹^{−} σ

są oczywiście odwracalne, ponieważ wszystkie te typy należą do jednej klasy abstrakcji relacji równoważności indukowanej przez ⊑. Zgodnie z Lematem 6.2, dodatnie kroki odwracalne nie mogą zmieniać kształtu drzewa typu, ani znaku pozycji wiązania zmiennych. Zatem kształt typu oraz znaki pozycji wiązania zmiennych w typie ρ są takie same, jak w typie σ. Kroki ujemne ⟹_{i}^{−} mogą jedynie zmniejszać wagę typu oraz zamieniać zmienne wolne lub związane na pozycjach dodatnich w związane na pozycjach ujemnych. Wynika z tego, że w fazie ujemnej kształt drzewa typu, ani znaki pozycji wiązań zmiennych również nie mogą ulec zmianie.

Zbadajmy teraz, jaki wpływ na pozycję wiązania zmiennej α i zbiór Π(pr) może mieć pojedynczy krok dodatni =^{s} ⟹_{i}^{+}, dopuszczalny w myśl Lematu 6.2

• jeśli s ≹ p, to krok ten nie ma wpływu na zmienną α;

• jeśli s ≤ p i kwantyfikator ∀α na pozycji p jest w zasięgu instancjowanego kwantyfikatora, krok ten nie ma wpływu na pozycję wiązania zmiennej α, ani na zbiór Π(pr); • jeśli s = p i instancjowanym kwantyfikatorem jest ∀α, to pozycja wiązania

może zmienić się z p na inną pozycję dodatnią p′, gdzie p = p′r′ dla jakiegoś r′

σ_{i}[∀δ⃗β ϱ[∀ζ⃗α υ]_{r′}]_{p′} =^{p} ⟹_{i}^{+} σ_{i}[∀δ⃗β ϱ[∀ζ⃗υ{α ↦ ∀ϑ⃗ β}]_{r′}]_{p′} = σ_{i+1}

• jeśli s ≥ p i instancjowany kwantyfikator jest w zasięgu kwantyfikatora ∀α, to może zwiększyć się zbiór Π(pr) (przyjmujemy, że s = pr′′ dla jakiegoś r′′)

σ_{i}[∀ζ⃗α υ[∀δ⃗γ χ]_{r′′}]_{p} =^{s} ⟹_{i}^{+} σ_{i}[∀ζ⃗α υ[∀δ⃗ χ{γ ↦ ∀ϑ⃗ α}]_{r′′}]_{p} = σ_{i+1}

Nie można zatem zmniejszyć zbioru Π(pr) ani zmienić pozycji wiązania na większą w porządku <. W przypadku, gdy instancjowany jest kwantyfikator ∀α, zmiana jest odwracalna w dodatniej fazie derywacji tylko w sytuacji trywialnej, gdy p′ = p i β ∉ F V (ϱ). Druga zmiana, kiedy instancjowany kwantyfikator jest w zasięgu ∀α, jest odwracalna również wyłącznie w przypadku trywialnym, kiedy γ ∉ F V (χ).

Ponieważ ujemna faza derywacji nie może zmieniać dodatnich miejsc wiązania zmiennych, więc zmiany pozycji wiązania zmiennych mogą być tylko trywialne. ■

Lemat 6.4 Jeśli σ ⟹ τ jest krokiem odwracalnym, to wyrażenie σ ∼ τ da się wyprowadzić za pomocą aksjomatów (B1) i (B2).

Dowód. Jeśli krok σ ⟹ τ jest rodzaju ⟹_{q}, wystarczy użyć równości (B2). W przeciwnym przypadku jest to krok rodzaju ⟹_{i}. Załóżmy, że jest to krok dodatni

σ = σ[∀δ⃗α ϱ]_{p} =^{p} ⟹_{i}^{+} σ[∀δ⃗ϱ{α ↦ ξ}]_{p} = τ

Jeśli α ∉ F V (ϱ), możemy przyjąć, że ξ = ⊥ i σ ∼ τ na mocy aksjomatu (B2).

Załóżmy zatem, że α ∈ F V (ϱ). Z Lematu 6.2 wynika, że ξ = ∀α_{1} … α_{n} β, gdzie β jest albo jedną ze zmiennych α_{1}, …, α_{n}, albo inną zmienną związaną na pozycji dodatniej.

Jeśli β = α_{i} dla jakiegoś i, to z Lematu 6.2 wynika, iż zmienna α może występować w ϱ tylko na pozycjach dodatnich. W tym przypadku, wyrażenie σ ∼ τ wyprowadzamy używając aksjomatu (B2) na pozycji p, zastępując ∀α ϱ przez ϱ{α ↦ ⊥}, a następnie w każdym wystąpieniu zmiennej α w ϱ dostawiamy brakujące kwantyfikatory, zamieniając wszędzie ⊥ = ∀α_{i} α_{i} na ∀α_{1} … α_{n} α_{i} za pomocą (n − 1)-krotnego użycia aksjomatu (B2).

Jeśli β jest inną zmienną związaną na pozycji dodatniej p′, gdzie p = p′r′ dla pewnego r′, to na mocy Lematu 6.3 mamy następujące możliwości:

• możliwość trywialna — p′ = p oraz β ∉ F V (ϱ);

• wszystkie wystąpienia zmiennych α i β są pozytywne.

W pierwszym przypadku mamy do czynienia z następującą sytuacją:

σ|_{p} = ∀δ_{1}, …, δ_{i−1} β δ_{i+1}, …, δ_{n} α ϱ

gdzie ∀β jest pustym kwantyfikatorem. Wystarczy odpowiednią liczbę razy użyć aksjomatu (B1), aby doprowadzić do sytuacji

∀δ_{1}, …, δ_{i−1} β α δ_{i+1}, …, δ_{n} ϱ

a następnie raz aksjomatu (B2), aby wyeliminować pusty kwantyfikator ∀β.

W drugim przypadku zamieniamy najpierw wszystkie wystąpienia zmiennych α i β na ⊥ za pomocą aksjomatu (B2), a następnie zamieniamy wszystkie wystąpienia ⊥ na pozycjach zajmowanych oryginalnie przez α i β na nową zmienną γ dostawiając kwantyfikator ∀γ w miejscu oryginalnego kwantyfikatora ∀β

σ = σ[∀δ⃗β υ[∀ζ⃗α ϱ]_{r′}]_{p′}
\overrightarrow{(B2)}  ∼ σ[∀δ⃗β υ[∀ζ⃗ ϱ\{α ↦ ⊥\}]_{r′}]_{p′}
\overrightarrow{(B2)}  ∼ σ[∀δ⃗ υ[∀ζ⃗ ϱ\{α ↦ ⊥\}]_{r′}\{β ↦ ⊥\}]_{p′}
\overleftarrow{(B2)}  ∼ σ[∀δ⃗γ υ[∀ζ⃗ ϱ\{α ↦ γ\}]_{r′}\{β ↦ γ\}]_{p′}
≡ σ[∀δ⃗β υ[∀ζ⃗ ϱ{α ↦ β}]_{r′}]_{p′}

W obu przypadkach jeszcze trzeba odpowiednią liczbą zastosowań aksjomatu (B2) dostawić we wszystkich koniecznych miejscach brakujące puste kwantyfikatory ∀α_{1} … α_{n}.

Jeśli rozpatrywany krok τ ⟹ σ był krokiem =^{p} ⟹_{i}^{−}, to sytuacja jest dualna. Wystarczy w podobny sposób przeanalizować krok τ → γ =^{0p} ⟹_{i}^{+} σ → γ (gdzie γ jest nową zmienną), który również jest odwracalny, ponieważ σ → γ ⊑ τ → γ.

Zatem dla każdego kroku odwracalnego σ ⟹ τ, wyrażenie σ ∼ τ da się wyprowadzić używając wyłącznie aksjomatów (B1) i (B2). ■

Lemat 6.5 Jeśli wyrażenie σ ∼ τ może być udowodnione jednokrotnym użyciem aksjomatu (B1) lub (B2), to σ ⟹ ⟹ τ oraz τ ⟹ ⟹ σ. Ponadto w wyprowadzeniach tych używamy samych bezpiecznych redukcji.

Dowód. Musimy rozpatrzeć cztery możliwości, ze względu na to, który aksjomat został użyty i na jakiej pozycji

• jeśli do dowodu σ ∼ τ użyto aksjomatu (B1) na pozycji dodatniej p, tzn.

σ = σ[∀δ⃗αβ ϱ]_{p} ∼ σ[∀δ⃗βα ϱ]_{p} = τ

to używamy następujących kroków:

σ[∀δ⃗αβ ϱ]_{p} =^{p} ⟹_{q}^{+} σ[∀δ⃗γαβ ϱ]_{p} =^{p} ⟹_{i}^{+} σ[∀δ⃗γα ϱ{β ↦ γ}]_{p} ≡ τ

gdzie γ jest nową zmienną. Krok =^{p} ⟹_{i}^{+} jest bezpieczny, ponieważ term podstawiany jest zmienną związaną na pozycji o identycznym znaku. Wyprowadzenie nierówności w drugą stronę jest analogiczne; • jeśli użyto aksjomatu (B1) na pozycji ujemnej, to korzystając z faktu, że

∀αβ ϱ ≡ ∀γβ ϱ{α ↦ γ}

gdzie γ jest nową zmienną, możemy użyć kroków następujących

σ[∀δ⃗αβ ϱ]_{p} ≡ σ[∀δ⃗γβ ϱ{α ↦ γ}]_{p} =^{p} ⟹_{i}^{−} σ[∀δ⃗γβα ϱ]_{p} =^{p} ⟹_{q}^{−} σ[∀δ⃗βα ϱ]_{p}

Krok =^{p} ⟹_{i}^{−} jest bezpieczny, jak poprzednio. Podobnie, wyprowadzenie drugiej nierówności jest analogiczne;

• jeśli użyty został aksjomat (B2) na pozycji dodatniej p, to mamy do czynienia z następującą sytuacją:

σ = σ[∀δ⃗α ϱ]_{p} ∼ σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p} = τ

gdzie wystąpienia zmiennej α w typie ϱ są wyłącznie pozytywne. Aby pokazać nierówność w jedną stronę, używamy bezpiecznego kroku

σ[∀δ⃗α ϱ]_{p} =^{p} ⟹_{i}^{+} σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p}

Aby pokazać nierówność w drugą stronę, oznaczmy przez r_{1}, …, r_{n} pozycje wszystkich wystąpień zmiennej α w typie ϱ. Dla każdego i mamy ϱ{α ↦ ⊥}|_{r_{i}} = ∀ζ⃗_{i}⊥ = ∀ζ⃗_{i}β β, zatem

σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p}  =^{p} ⟹_{q}^{+} σ[∀δ⃗γ ϱ{α ↦ ⊥}]_{p}
=^{pr_{1}} ⟹_{i}^{+} σ[∀δ⃗γ ϱ{α ↦ ⊥}[∀ζ⃗_{1} γ]_{r_{1}}]_{p}
⋮
=^{pr_{n}} ⟹_{i}^{+} σ[∀δ⃗γ ϱ{α ↦ ⊥}[∀ζ⃗_{1} γ]_{r_{1}} ⋯ [∀ζ⃗_{n} γ]_{r_{n}}]_{p}
=  σ[∀δ⃗γ ϱ{α ↦ γ}]_{p}
≡  σ[∀δ⃗α ϱ]_{p}

gdzie γ jest nową zmienną. Kroki =^{pr_{i}} ⟹_{i}^{+} są poprawne i bezpieczne, ponieważ wszystkie r_{i}, a co za tym idzie również wszystkie pr_{i} są pozytywne, a wstawiana w miejsce kolejnych ∀β β zmienna γ jest związana na pozycji dodatniej p;

• jeżeli aksjomat (B2) został użyty na pozycji ujemnej, sytuacja jest dualna. Nierówność τ ⊑ σ dowodzimy łatwo

τ = σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p} =^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ]_{p} = σ

a drugą nierówność dowodzimy tak, jak poprzednio, oznaczając r_{1}, …, r_{n} pozycje wszystkich wystąpień zmiennej α w typie ϱ (dla każdego i mamy ϱ|_{r_{i}} = ∀ζ⃗_{i} α)

σ[∀δ⃗α ϱ]_{p}  =^{pr_{1}} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗_{1} ⊥]_{r_{1}}]_{p}
⋮
=^{pr_{n}} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗_{1} ⊥]_{r_{1}} ⋯ [∀ζ⃗_{n} ⊥]_{r_{n}}]_{p}
=  σ[∀δ⃗α ϱ{α ↦ ⊥}]_{p}
=^{p} ⟹_{q}^{−} σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p}
■

Twierdzenie 1 (charakteryzacja bikoercyjności)

Nierówności σ ⊑ τ oraz τ ⊑ σ zachodzą równocześnie wtedy i tylko wtedy, gdy σ ∼ τ.

Dowód. Jeżeli zachodzą obie nierówności σ ⊑ τ oraz τ ⊑ σ, to istnieje wyprowadzenie normalne σ ⟹ ⟹^{+} ⟹ ⟹^{−} τ złożone z samych kroków odwracalnych. Z Lematu 6.4 wynika, że σ ∼ τ.

W drugą stronę, jeżeli σ ∼ τ, to z Lematu 6.5 i z przechodniości relacji ⊑ mamy σ ⊑ τ oraz τ ⊑ σ. ■

Własność typów bikoercyjnych, której będziemy używać w dalszej części pracy wyraża następujące stwierdzenie:

Stwierdzenie 6.6 Jeśli σ_{0} ∼ σ_{1} i σ_{1} ⊑ τ to zachodzi również nierówność σ_{0} ⊑ τ oraz waga tej ostatniej nierówności równa jest wadze nierówności σ_{1} ⊑ τ.

Dowód. Stwierdzenie to wynika łatwo z Lematu 6.5 oraz ze Stwierdzenia 5.6. ■

7 Derywacje uporządkowane

Aby pokazać własności relacji ⊑, będziemy używać uporządkowanej wersji normalnych derywacji. Intuicyjnie, pozytywne kroki derywacji będą wykonywać się w kolejności wyznaczonej przez porządek leksykograficzny pozycji, indukowany przez 0 ≺ 1. W ramach tej samej pozycji najpierw wykonywać się będą wszystkie kroki dostawiające kwantyfikatory, a następnie kroki instancjujące, ułożone od zewnętrznych do wewnętrznych. Kroki negatywne uporządkowane będą dualnie. Przepisywanie typów będzie się zatem odbywać najpierw na pozycjach pozytywnych od góry do dołu, a następnie na pozycjach negatywnych od dołu do góry.

Definicja 7.1 (derywacje uporządkowane)

Ciąg kroków pozytywnych σ_{0} =^{p_{1}} ⟹^{+} ⋯ =^{p_{n}} ⟹^{+} σ_{n} jest uporządkowany, jeśli spełnione są następujące warunki:

1. dla każdego i, j jeśli i < j, to p_{i} ⪯ p_{j};

2. dla ustalonego p kroki =^{p} ⟹_{q}^{+} poprzedzają kroki =^{p} ⟹_{i}^{+};

3. nie występują pary kroków

σ_{j}[∀δ⃗ α ζ⃗β ϱ]_{p}  =^{p} ⟹_{i}^{+} σ_{j}[∀δ⃗ α ζ⃗ ϱ{β ↦ ξ_{β}}]_{p}
=^{p} ⟹_{i}^{+} σ_{j}[∀δ⃗ ζ⃗ ϱ{β ↦ ξ_{β}}{α ↦ ξ_{α}}]_{p}

Ciąg kroków negatywnych τ_{0} ⟹^{−} ⋯ ⟹^{−} τ_{n} jest uporządkowany, jeśli dualny ciąg kroków pozytywnych τ_{n} → γ ⟹^{+} ⋯ ⟹^{+} τ_{0} → γ (gdzie γ jest nową zmienną) jest uporządkowany.

Normalną derywację σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ nazywamy uporządkowaną jeśli ciągi σ ⟹ ⟹^{+} ρ oraz ρ ⟹ ⟹^{−} τ są uporządkowane.

Udowodnimy teraz, że każdą derywację da się uporządkować. Potrzebny nam będzie następujący kluczowy lemat.

Lemat 7.2 Jeśli ciąg kroków σ =^{p} ⟹^{+} ρ =^{p′} ⟹^{+} τ nie jest uporządkowany, to istnieje typ ρ′ taki, że derywacja σ ⟹^{+} ρ′ ⟹^{+} τ jest uporządkowana.

Dowód. Jeśli obydwa kroki są krokami ⟹_{q}, to zamiana ich miejscami nie stanowi żadnego problemu.

Jeśli pierwszy jest krok ⟹_{q}, a drugi ⟹_{i} i derywacja nie jest uporządkowana, to znaczy, że p′ ≺ p. W każdym przypadku, nowo dostawiony kwantyfikator nie wiąże żadnej zmiennej w typach ρ i τ, zatem można go wstawić również po instancjacji.

Jeśli pierwszy krok jest krokiem ⟹_{i}, a drugi ⟹_{q}, to zamiana również jest oczywista.

Jeśli obydwa kroki wyprowadzenia są typu ⟹_{i}, to znaczy, że p′ ⪯ p. Jeśli p′ nie jest prefiksem p, to zamiana jest trywialna. W przeciwnym przypadku, dla r takiego że p = p′r (być może r = ϵ), mamy następującą sytuację

σ = σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{r}]_{p′}  =^{p} ⟹_{i}^{+} σ[∀δ⃗α ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{r}]_{p′}
=^{p′} ⟹_{i}^{+} σ[∀δ⃗ ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{r}{α ↦ ξ_{α}}]_{p′} = τ

Stosując fakt, że υ{β ↦ ξ_{β}}{α ↦ ξ_{α}} = υ{α ↦ ξ_{α}}{β ↦ ξ_{β}{α ↦ ξ_{α}}} i oznaczając \overline{ϱ} = ϱ\{α ↦ ξ_{α}\} oraz \overline{υ} = υ\{α ↦ ξ_{α}\} możemy dokonać następującej zamiany

σ = σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{r}]_{p′}  =^{p} ⟹_{i}^{+} σ[∀δ⃗ ϱ[∀ζ⃗β υ]_{r}{α ↦ ξ_{α}}]_{p′}
= σ[∀δ⃗ \overline{ϱ}[∀ζ⃗β \overline{υ}]_{r}]_{p′}
=^{p′} ⟹_{i}^{+} σ[∀δ⃗ \overline{ϱ}[∀ζ⃗ \overline{υ}\{β ↦ ξ_{β}\{α ↦ ξ_{α}\}\}]_{r}]_{p′}
= σ[∀δ⃗ ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{r}{α ↦ ξ_{α}}]_{p′} = τ

W każdym przypadku można więc zamieniać kolejność źle uporządkowanych par kroków. ■

Lemat 7.3 (porządkowanie derywacji)

Jeśli σ ⊑ τ, to istnieje derywacja uporządkowana σ ⟹ ⟹^{+} ⟹ ⟹^{−} τ, której waga jest równa wadze nierówności.

Dowód. Na podstawie Lematu 7.2 wnioskujemy, że dowolne ciągi kroków dodatnich mogą być sortowane. Stosując metodę dualną sortować można również kroki ujemne.

Niech σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ będzie wyprowadzeniem nierówności σ ⊑ τ o minimalnej wadze. Sortowanie kroków pozytywnych i negatywnych nie zmienia oczywiście typu ρ, więc waga wyprowadzenia σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ równa 2 × waga(ρ) − waga(σ) − waga(τ) nie ulega zmianie. ■

8 Wymuszanie nierówności

Ten rozdział zawiera dowód własności relacji ⊑ używanych bezpośrednio w dowodzie nierozstrzygalności.

Lemat 8.1 Niech σ ⊑ τ oraz σ|_{p} = ϱ_{σ} i τ|_{p} = ϱ_{τ} są podtermami, których zmienne wolne nie są związane odpowiednio w σ i τ. Jeżeli p jest ścieżką pozytywną, to ϱ_{σ} ⊑ ϱ_{τ}, a jeśli jest ścieżką negatywną, to ϱ_{τ} ⊑ ϱ_{σ}.

Dowód. Niech σ = σ_{0} =^{p_{1}} ⟹^{+} ⋯ =^{p_{n}} ⟹^{+} σ_{n} = τ_{m} =^{q_{m}} ⟹^{−} ⋯ =^{q_{1}} ⟹^{−} τ_{0} = τ bę-

dzie uporządkowanym wyprowadzeniem nierówności σ ⊑ τ. Ponieważ ciągi p_{1}, …, p_{n} oraz q_{1}, …, q_{m} są posortowane leksykograficznie, więc pozycje, których prefiksem jest p występują jako kolejne. Niech p_{k}, …, p_{k′}, q_{l}, …, q_{l′} będą wszystkimi takimi pozycjami i niech r_{k}, …, r_{k′}, s_{l}, …, s_{l′} będą takie, że p_{i} = pr_{i} oraz q_{j} = ps_{j}.

Załóżmy najpierw, że p jest pozytywne. Wówczas kroki

σ_{k−1}|_{p} =^{r_{k}} ⟹^{+} ⋯ =^{r_{k′}} ⟹^{+} σ_{k′}|_{p} = τ_{l′}|_{p} =^{s_{l′}} ⟹^{−} ⋯ =^{s_{l}} ⟹^{−} τ_{l−1}|_{p}

stanowią poprawne wyprowadzeniem nierówności ϱ_{σ} ⊑ ϱ_{τ}.

Istotnie, spośród pozostałych kroków, których pozycjami są p_{1}, …, p_{k−1}, p_{k′+1}, …, p_{n} oraz q_{1}, …, q_{l−1}, q_{l′+1}, …, q_{m}, na podterm na pozycji p mogłyby wpływać wyłącznie te, w których p_{i} (bądź q_{j}) jest prefiksem p. Ponieważ wyprowadzenie jest uporządkowane, więc takie pozytywne kroki wystąpią tylko przed krokami p_{k}, …, p_{k′}, a negatywne po krokach q_{l}, …, q_{l′}. Zgodnie z założeniem żadne zmienne w ϱ_{σ} nie są związane w σ, ani zmienne w ϱ_{τ} nie są związane w τ. Z tego względu kroki na pozycjach, które są prefiksami p, również nie mogą zmieniać podtypu na pozycji p i zachodzi σ_{k−1}|_{p} = σ|_{p} = ϱ_{σ} oraz τ_{l′+1}|_{p} = τ_{p} = ϱ_{τ}.

Niektóre kroki ⟹_{i}^{+} spośród p_{k}, …, p_{k′} mogą związać pewne zmienne z podtypu na pozycji p przez kwantyfikatory znajdujące się powyżej p

σ_{i−1}[∀δ⃗β ρ[ϱ[∀ζ⃗α υ]_{r_{i}}]_{u}]_{t} =^{p_{i}} ⟹_{i}^{+} σ_{i−1}[∀δ⃗β ρ[ϱ[∀ζ⃗ υ{α ↦ ξ_{α}}]_{r_{i}}]_{u}]_{t} = σ_{i}

(gdzie p = tu, p_{i} = pr_{i} jak poprzednio), w przypadku gdy β ∈ F V (ξ_{α}). Jednak jako że wyprowadzenie jest uporządkowane, te ostatnie kwantyfikatory nie mogą być dalej instancjonowane. Można więc zamiast zmiennych związanych przez te kwantyfikatory, wprowadzać zmienne wolne, ponieważ i tak w fazie ujemnej zostaną one wszystkie zlikwidowane (przez kroki ⟹_{i}^{−}), tak jak zostałyby zlikwidowane wszystkie zmienne związane przez kwantyfikatory występujące powyżej pozycji p. Odpowiednikiem tego kroku w nowym wyprowadzeniu, będzie

ϱ[∀ζ⃗α υ]_{r_{i}} =^{r_{i}} ⟹_{i}^{+} ϱ[∀ζ⃗ υ{α ↦ ξ_{α}}]_{r_{i}}

gdzie β ∈ F V (ξ_{α}) jest zmienną wolną.

Jeśli p jest negatywne, podobna analiza dowodzi, że nierówność ϱ_{τ} ⊑ ϱ_{σ} może być udowodniona przez ciąg kroków

τ_{l−1}|_{p} =^{s_{l}} ⟹^{+} ⋯ =^{s_{l′}} ⟹^{+} τ_{l′}|_{p} = σ_{k′}|_{p} =^{r_{k′}} ⟹^{−} ⋯ =^{r_{k}} ⟹^{−} σ_{k−1}|_{p}

■

Lemat 8.2 Nierówność σ′ → σ′′ ⊑ τ′ → τ′′ zachodzi wtedy i tylko wtedy, gdy zachodzą nierówności σ′ ⊒ τ′ i σ′′ ⊑ τ′′. Ponadto, jeśli nierówności te są prawdziwe, to waga pierwszej jest równa sumie wag pozostałych.

Dowód. Implikacja od prawej strony do lewej jest prostą konsekwencją reguły (→-kontekst), a od lewej do prawej — poprzedniego lematu.

Zależność wag tych nierówności jest również łatwa do ustalenia. Niech

τ′ = τ′_{0} =^{t_{1}} ⟹^{+} ⋯ =^{t_{k}} ⟹^{+} τ′_{k} = σ′_{l} =^{u_{l}} ⟹^{−} ⋯ =^{u_{1}} ⟹^{−} σ′_{0} = σ′  (3)

będzie uporządkowanym wyprowadzeniem nierówności σ′ ⊒ τ′ o minimalnej wadze. Podobnie, niech

σ′′ = σ′′_{0} =^{p_{1}} ⟹^{+} ⋯ =^{p_{n}} ⟹^{+} σ′′_{n} = τ′′_{m} =^{q_{m}} ⟹^{−} ⋯ =^{q_{1}} ⟹^{−} τ′′_{0} = τ′′  (4)

będzie minimalnym wyprowadzeniem nierówności σ′′ ⊑ τ′′. Wówczas wyprowadzenie

\begin{aligned}& σ′_{0} → σ′′_{0} =^{0u_{1}} ⟹^{+} ⋯ =^{0u_{l}} ⟹^{+} σ′_{l} → σ′′_{0} =^{1p_{1}} ⟹^{+} ⋯ =^{1p_{n}} ⟹^{+} σ′_{l} → σ′′_{n} & = \\ = & τ′_{k} → τ′′_{m} =^{1q_{m}} ⟹^{−} ⋯ =^{1q_{1}} ⟹^{−} τ′_{k} → τ′′_{0} =^{0t_{k}} ⟹^{−} ⋯ =^{0t_{k}} ⟹^{−} τ′_{0} → τ′′_{0} \end{aligned} (5)

jest uporządkowanym wyprowadzeniem normalnym nierówności σ′ → σ′′ ⊑ τ′ → τ′′. Zatem waga tej ostatniej jest nie większa od sumy wag pozostałych.

W drugą stronę, każde uporządkowane wyprowadzenie normalne nierówności σ′ → σ′′ ⊑ τ′ → τ′′ zaczyna się od kroków =^{ϵ} ⟹_{q}^{+}, poprzedzających kroki =^{ϵ} ⟹_{i}^{+}. Mamy zatem następującą sytuację:

σ′ → σ′′ =^{ϵ} ⟹_{q}^{+} ⋯ =^{ϵ} ⟹_{q}^{+} ∀α_{1} … α_{n} σ′ → σ′′

gdzie oczywiście α_{1}, …, α_{n} ∉ F V (σ′ → σ′′). Zatem kolejne kroki =^{ϵ} ⟹_{i}^{+} są pustymi instancjacjami

∀α_{1} … α_{n} σ′ → σ′′ =^{ϵ} ⟹_{i}^{+} ⋯ =^{ϵ} ⟹_{i}^{+} ∀α_{i_{1}} … α_{i_{k}} σ′ → σ′′

Ponieważ do końca wyprowadzenia nie ma już więcej kroków =^{ϵ} ⟹, a typ końcowy jest postaci τ′ → τ′′, więc ciąg α_{i_{1}}, …, α_{i_{k}} musi być ciągiem pustym. Zatem całe wyprowadzenie jest równoważne wyprowadzeniu bez kroków =^{ϵ} ⟹^{+}. Pozostałe kroki dzielą się dokładnie tak, jak w (5), na wyprowadzenia nierówności σ′ ⊒ τ′ (3) oraz σ′′ ⊑ τ′′ (4). Zatem suma wag tych dwóch nierówności jest nie większa niż waga σ′ → σ′′ ⊑ τ′ → τ′′. ■

Lemat 8.3 Niech σ i τ będą takimi typami, że istnieją dwie ścieżki: pozytywna p i negatywna s, takie że σ|_{p} = σ|_{s} = α i τ|_{p} = τ|_{s} = α dla pewnej zmiennej wolnej α. Ponadto typ τ nie jest postaci ∀γ τ′. Wówczas

1. ∀α σ ⊑ τ{α ↦ ξ} wtedy i tylko wtedy, gdy σ{α ↦ ξ} ⊑ τ{α ↦ ξ} ;

2. jeśli obie nierówności zachodzą, to waga pierwszej jest większa lub równa wadze drugiej; 3. ponadto jeśli waga(ξ) > 0 to waga pierwszej nierówności jest ostro większa

od wagi drugiej.

Dowód. Jeśli zachodzi nierówność σ{α ↦ ξ} ⊑ τ{α ↦ ξ} dla typów σ i τ jak w treści lematu, to ponieważ ∀α σ =^{ϵ} ⟹_{+}^{i} σ{α ↦ ξ}, więc prawdziwa jest również nierówność

∀α σ ⊑ τ{α ↦ ξ}  (6)

Aby pokazać wynikanie w drugą stronę, załóżmy, że zachodzi nierówność (6). Rozpatrzmy wyprowadzenie uporządkowane tej nierówności o minimalnej wadze. Zaczyna się ono od pewnej liczby (być może zerowej) kroków =^{ϵ} ⟹^{+} o zerowej wadze

∀α σ =^{ϵ} ⟹_{q}^{+} ⋯ =^{ϵ} ⟹_{q}^{+} ∀α_{1} … α_{n}αβ_{1} … β_{m} σ
=^{ϵ} ⟹_{i}^{+} ⋯ =^{ϵ} ⟹_{i}^{+} ∀α_{i_{1}} … α_{i_{k}}αβ_{1} … β_{m} σ

Gdyby ciąg α_{i_{1}} … α_{i_{k}} nie był pusty, kwantyfikatory te zostałyby na pozycji ϵ aż do końca derywacji, co jest niemożliwe. Z tego samego powodu kolejnym krokiem derywacji musi być krok instancjujący kwantyfikator ∀α

∀α σ′ =^{ϵ} ⟹_{i}^{+} σ′{α ↦ χ}  (7)

gdzie σ′ = ∀β_{1} … β_{m} σ. Oczywiście β_{1}, …, β_{m} ∉ F V (σ′{α ↦ χ}). Z Lematu 8.1 wynika, że ξ ∼ χ, a zatem również σ′{α ↦ ξ} ∼ σ′{α ↦ χ}. Ponadto kwantyfikatory ∀β_{1} … β_{m} są puste, więc σ{α ↦ ξ} ∼ σ′{α ↦ χ} i co za tym idzie

σ{α ↦ ξ} ⊑ τ{α ↦ ξ}

Waga tej ostatniej nierówności, na mocy Stwierdzenia 6.6, jest nie większa od wagi wyprowadzenia σ′{α ↦ χ} ⟹ ⟹ τ{α ↦ ξ} zatem nie większa niż waga nierówności (6) odjąć waga kroku (7). Waga tego kroku jest większa od zera wtedy i tylko wtedy, gdy waga(ξ) > 0, ponieważ wagi ξ i χ są równe. ■

9 Nierozstrzygalność relacji osłabiania

Niniejszy rozdział zamknie dowód nierozstrzygalności relacji ⊑. Po udowodnieniu Lematów 8.2 i 8.3, wiemy już, że relacja ⊑ ma wszystkie własności relacji ⊑_{M} używane w pracy [TU95] do kodowania problemu stopu maszyny rejestrów stosowych. Pokażemy w pewnym skrócie na czym to kodowanie polega.

Maszyna rejestrów stosowych M posiada dwa rejestry główne V_{1} i V_{2} oraz skończoną liczbę rejestrów pomocniczych v_{1}, …, v_{n}. Rejesty te zawierają niepuste słowa nad skończonym alfabetem Σ, złożonym z etykiet instrukcji, w tym wyróżnionej etykiety końcowej e. Krok maszyny polega na zdjęciu etykiety instrukcji z pierwszego rejestru głównego, wykonaniu jej na rejestrach pomocniczych oraz zamianie miejscami rejestrów głównych. Jeśli przeczytana etykieta była ostatnią w rejestrze V_{1}, to na jego miejsce kopiujemy zawartość pierwszego rejestru pomocniczego v_{1} sprzed wykonania instrukcji. Instrukcje maszyny są równoległymi przypisaniami zawartości jednych rejestrów na inne, z ewentualnym dopisaniem na wierzchołku dodatkowych etykiet. Dla danej etykiety ℓ ≠ e, zapisujemy to

ℓ(r_{1}, …, r_{n}) = (w_{1}r_{i_{1}}, …, w_{n}r_{i_{n}}) gdzie w_{i} ∈ Σ^{∗}

Mając daną chwilową konfigurację maszyny — krotkę (V_{1}, V_{2}, v_{1}, …, v_{n}) złożoną z n + 2 słów — następny krok spowoduje następującą zmianę, w zależności od zawartości pierwszego rejestru głównego:

• jeśli V_{1} = eV′_{1}, to maszyna się zatrzymuje;

• jeśli V_{1} = ℓV′_{1}, gdzie ℓ ≠ e oraz V_{1} ≠ ϵ, to następną konfiguracją będzie (V_{2}, V′_{1}, v′_{1}, …, v′_{n}), jeśli ℓ(v_{1}, …, v_{n}) = (v′_{1}, …, v′_{n});

• jeśli V_{1} = ℓ, dla ℓ ≠ e, to następną konfiguracją będzie (V_{2}, v_{1}, v′_{1}, …, v′_{n}), dla v′_{1}, …, v′_{n} jak poprzednio.

Konfiguracja chwilowa maszyny (V_{1}, V_{2}, v_{1}, …, v_{n}) kodowana jest przez n + 2 typy σ_{V_{1}}, σ_{V_{2}}, σ_{v_{1}}, …, σ_{v_{n}}, zawierające pewną ustaloną zmienną wolną γ, łatwo konstruowalne na podstawie zawartości odpowiednich rejestrów. Kluczem do dowodu nierozstrzygalności jest następujące stwierdzenie:

Stwierdzenie 9.1 Dla danej maszyny rejestrów stosowych M, jej konfiguracja chwilowa (V_{1}, V_{2}, v_{1}, …, v_{n}) prowadzi do zatrzymania wtedy i tylko wtedy, kiedy zachodzi nierówność kodująca

σ_{V_{1}} ⊑ (σ_{v_{1}} → σ_{v_{1}}) → ⋯ (σ_{v_{n}} → σ_{v_{n}}) → σ_{V_{2}} → γ  (8)

Szkic dowodu:^{4} Równoważność ta opiera się na następujących własnościach kodowania i relacji ⊑

• jeśli (V_{1}, V_{2}, v_{1}, …, v_{n}) jest konfiguracją końcową, tj. V_{1} = eV′_{1}, to σ_{V_{1}} = ⊥;

• jeśli V_{1} = ℓV′_{1} dla V′_{1} ≠ ϵ oraz ℓ(r_{1}, …, r_{n}) = (w_{1}r_{i_{1}}, …, w_{n}r_{i_{n}}), mamy

σ_{V_{1}} = ∀α_{1} … α_{n} ((α_{1} → α_{1}) → … → (α_{n} → α_{n}) →
((σ_{w_{1}}[α_{i_{1}}] → σ_{w_{1}}[α_{i_{1}}]) → ⋯ → (σ_{w_{n}}[α_{i_{n}}] → σ_{w_{n}}[α_{i_{n}}]) →
σ_{V′_{1}} → γ) → γ)

Jeśli zachodzi nierówność kodująca (8), to na mocy n-krotnego użycia Lematu 8.3, wiemy, że jest ona równoważna nierówności

(σ_{v_{1}} → σ_{v_{1}}) → … → (σ_{v_{n}} → σ_{v_{n}}) →

((σ_{w_{1}}[σ_{v_{i_{1}}} ] → σ_{w_{1}}[σ_{v_{i_{1}}} ]) → … → (σ_{w_{n}}[σ_{v_{in}}] → σ_{w_{n}}[σ_{v_{in}}]) → σ_{V′_{1}} → γ) → γ

⊑ (σ_{v_{1}} → σ_{v_{1}}) → … → (σ_{v_{n}} → σ_{v_{n}}) → σ_{V_{2}} → γ

4Szczegóły kodowania oraz niniejszego dowodu mogą być znalezione w [TU95]

Po (n + 1)-krotnym zastosowaniu Lematu 8.2 mamy z kolei równoważność tej nierówności z nierównością kodującą konfigurację po jednym kroku

σ_{V_{2}} ⊑ (σ_{w_{1}}[σ_{v_{i_{1}}} ] → σ_{w_{1}}[σ_{v_{i_{1}}} ]) → … → (σ_{w_{n}}[σ_{v_{in}}] → σ_{w_{n}}[σ_{v_{in}}]) → σ_{V′_{1}} → γ

Waga ostatniej nierówności jest nie większa od wagi nierówności (8), a różnica wag staje się ściśle dodatnią, jeśli choć jeden z typów σ_{v_{1}}, …, σ_{v_{n}} miał niezerową wagę;

• podobnie, jeśli V_{1} = ℓ, dla ℓ jak wyżej, mamy

σ_{V_{1}} = ∀α_{1} … α_{n} ((α_{1} → α_{1}) → … → (α_{n} → α_{n}) →
((σ_{w_{1}}[α_{i_{1}}] → σ_{w_{1}}[α_{i_{1}}]) → ⋯ → (σ_{w_{n}}[α_{i_{n}}] → σ_{w_{n}}[α_{i_{n}}]) →
α_{1} → γ) → γ)

i stąd, rozumując jak poprzednio, otrzymujemy równoważność nierówności kodującej (8) z nierównością

σ_{V_{2}} ⊑ (σ_{w_{1}}[σ_{v_{i_{1}}} ] → σ_{w_{1}}[σ_{v_{i_{1}}} ]) → … → (σ_{w_{n}}[σ_{v_{in}}] → σ_{w_{n}}[σ_{v_{in}}]) → σ_{v_{1}} → γ

Łatwo zatem pokazać, że jeśli konfiguracja (V_{1}, V_{2}, v_{1}, …, v_{n}) jest końcowa, to nierówność kodująca zachodzi. W przeciwnym przypadku mamy równoważność

\begin{matrix}σ_{V_{1}} ⊑ (σ_{v_{1}} → σ_{v_{1}}) → ⋯ (σ_{v_{n}} → σ_{v_{n}}) → σ_{V_{2}} → γ \\ ⟺ σ_{U_{1}} ⊑ (σ_{u_{1}} → σ_{u_{1}}) → ⋯ (σ_{u_{n}} → σ_{u_{n}}) → σ_{U_{2}} → γ \end{matrix}

gdzie (U_{1}, U_{2}, u_{1}, …, u_{n}) jest konfiguracją maszyny po wykonaniu jednego kroku. Ponadto waga tej drugiej nierówności jest nie większa od wagi pierwszej, a jeśli nie wszystkie v_{1}, …, v_{n} zaczynają się od etykiety końcowej e, to różnica wag jest ściśle dodatnia.

Dowód faktu, że jeśli dla danej konfiguracji maszyna zatrzymuje się, to nierówność kodująca zachodzi, jest łatwy i był już opisany we wstępie.

W drugą stronę, jeśli zachodzi nierówność kodująca konfigurację chwilową maszyny, to nie może ona zrobić nieskończonej liczby kroków, gdyż przy każdym kroku waga nierówności kodującej zmniejsza się lub pozostaje bez zmian przy jednocześnie malejącej liczbie etykiet w rejestrach głównych. W ostatnim przypadku, jeśli opróżni się któryś z rejestrów głównych, to jego następna zawartość będzie zaczynać się od etykiety końcowej, co w kolejnym kroku doprowadzi do zatrzymania maszyny. ■

Twierdzenie 2 Relacja osłabiania polimorficznego bez aksjomatu rozdzielności ⊑ jest nierozstrzygalna.

Dowód. Twierdzenie wynika łatwo z właśnie udowodnionego Stwierdzenia 9.1 oraz z Lematu 16 z pracy Tiuryna i Urzyczyna [TU95], redukującego nierozstrzygalny problem stopu deterministycznych maszyn dwulicznikowych do problemu stopu maszyn rejestrów stosowych. ■

10 Podsumowanie

Praca zawiera dowód nierozstrzygalności relacji osłabiania polimorficznego ⊑ powstałej z relacji osłabiania Mitchella z pracy [Mit88] przez usunięcie aksjomatu rozdzielności kwantyfikatora. Dowód przebiega poprzez redukcję problemu stopu maszyny rejestrów stosowych z pracy Tiuryna i Urzyczyna [TU95]. Niezbędne własności relacji ⊑ dowiedzione są przy użyciu systemu przepisywania typów opartego na aksjomatach Mitchella. Dodatkowo rozdział 6 prezentuje równościową charakteryzację relacji równoważności indukowanej przez quasiporządek ⊑.

Niemal identyczny dowód nierozstrzygalności mógłby zostać przeprowadzony dla relacji powstałej z ⊑ przez usunięcie kolejnego aksjomatu — aksjomatu dostawiania pustego kwantyfikatora (kwant). Poważniejsze różnice wystąpiłyby jedynie w rozdziale 6, ale najważniejsze dla dalszego dowodu Stwierdzenie 6.6 pozostaje prawdziwe.

Pożądaną kontynuacją pracy byłoby znalezienie jakiejś rozstrzygalnej relacji osłabiania zawartej w relacji ⊑_{M} Mitchella. Pewnym pomysłem na rozstrzgalność jest stratyfikacja typów polimorficznych, opisana w pracy Daniela Leivanta [Lei91]. Mając daną rozłączną sumę zbiorów zmiennych V = ∪_{i≥0}V_{i} określamy rząd typu jako maksymalny rząd zmiennej (wolnej lub związanej), która w nim występuje. Następnie kroki (inst) mogą być wykonywane wyłacznie wtedy, gdy typ wstawiany ma rząd ściśle mniejszy niż rząd instancjowanej zmiennej.

Przy takim systemie dowód nierozstrzygalności z pracy [TU95], oparty na kodowaniu obliczeń maszyny, nie mógłby być zastosowany, gdyż jak powiedzieliśmy we wstępie, opiera się on na nieograniczonym zagnieżdżeniu instancjacji. Za to prawdopodobnie dowód nierozstrzygalności Wellsa (por. [Wel95]) mógłby zostać przeprowadzony bez problemów. Jednak, ponieważ opiera się on bardzo silnie na aksjomacie rozdzielności, to system bez tego aksjomatu, z ograniczoną przez stratyfikcję instancjacją mógłby okazać się rozstrzygalny.

Bibliografia

[CL91] L. Cardelli and G. Longo. “A semantic basis for Quest”, Journal of Functional Programming, 1:417-458, October 1991.

[Gir89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Jim95] T. Jim, “System F plus subsumption reduces to Mitchell’s subtyping relation”, Manuscript (1995).

[Lei91] D. Leivant, “Finitely stratified polymorphism”, Information and Computation, 93 (1), 1991, 93–113.

[LMS95] G. Longo, K. Milsted, and S. Soloviev, “A logic of subtyping”, Proc. 10-th IEEE Symp. Logic in Computer Science, San Diego (1995), pp. 292-299.

[Mit88] J.C. Mitchell, “Polymorphic type inference and containment”, Information and Computation, 76 (2-3), 1988, pp. 211–249.

[Tiu95] J. Tiuryn, “Equational Axiomatization of Bicoercibility for Polymorphic Types”, Proc. Conf. Foundations of Software Technology and Teoretical Computer Science’95, Bangalore, India; 18-20 Dec 1995. Lecture Notes in Computer Science 1026, pp. 166-179.

[TU95] J. Tiuryn and P. Urzyczyn, “The Subtyping Problem For Second-Order Types in Undecidable” Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp. 74-85, 27-30 July 1996.

[Wel94] J.B. Wells, “Typability and type checking in the second-order λcalculus calculus are equivalent and undecidable”, Proc. 9th LICS, IEEE, 1994, pp. 176–185.

[Wel95] J.B. Wells, “The Undecidabilility of Mitchell’s Subtyping Relationship”, Technical Report, Computer Science Department, Boston University, Number 95-019, December 10 1995.

[Wel96] J.B. Wells, “Typability is Undecidable for F+Eta” Technical Report, Computer Science Department, Boston University, Number 96-022, March 9 1996.