Eine Kategorie von Reduktionsmodellen für den ungetypten λ-Kalkül

Diplomarbeit

von Martina Fischer

Betreuer: Prof. K. Keimel Fachbereich Mathematik

�

TU Darmstadt Januar 1998

Inhaltsverzeichnis

Vorwort 3

Einleitung 5

1 Grundlagen 6 1.1 Modelle für den ungetypten λ-Kalkül . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Reduktionsmodelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 1.3 Eigenschaften von Reduktionsmodellen . . . . . . . . . . . . . . . . . . . . . 8

2 Kategorielle Modelle 13 2.1 Charakterisierung von Adjunktionen . . . . . . . . . . . . . . . . . . . . . . 16

3 Einige Grundbegriffe der Kategorientheorie 19

4 Eine Kategorie von Reduktionsmodellen 26 4.1 Konstruktion eines Modells auf dem Exponential D^{D} in POSET . . . . . . . 33 4.2 Konstruktion eines Modells auf dem Produkt D × E in POSET . . . . . . . 35 4.3 RED_{⊥} ist eine symmetrisch monoidale Kategorie . . . . . . . . . . . . . . . 39

Vorwort

In der letzten Phase meines Studiums habe ich diese Diplomarbeit geschrieben. Auch wenn sie unter Zeitdruck entstanden ist (etwas anderes hatten ich, oder zumindest die Menschen, die mich kennen, auch nicht erwartet ^{^{⌣} ··}), so habe ich doch viel Freude dabei gehabt. Ich hatte noch einmal die Möglichkeit, mich mit einigen der mathematischen Gebiete zu befassen, die mich in meinem Studium am meisten interessiert haben: Bereichstheorie, Kategorientheorie und Semantik des λ-Kalküls. Mathematischer Ausgangspunkt der Arbeit war die Dissertationsschrift von Peter Selinger an der University of Pennsylvania. Ich habe mich dabei auf den Teil seiner Arbeit gestützt, der Reduktionsmodelle für den λ-Kalkül behandelt. Da dieser Modellbegriff bisher noch nicht erschöpfend untersucht worden ist, war es meine Aufgabe, eine Reihe von Eigenschaften und Anwendungen der Reduktionsmodelle zu finden. Zu Beginn habe eine Charakterisierung kategorieller Modelle auf Bäumen für solche Modelle auf beliebigen Bereichen verallgemeinert. Anschließend habe ich versucht, einen neuen Beweis für die Konsistenz des um die Gleichung (λx.xx)(λx.xx) = λx.x erweiterten λ-Kalküls zu finden. Die Konsistenz ist zwar schon weithin bekannt und sowohl beweistheoretisch als auch modelltheoretisch bewiesen, die Modellierung der Reduktion lieferte aber den Verdacht, daß es einen einfacheren oder zumindest neuen Beweis geben könnte. Leider traten aber mathematische Schwierigkeiten auf, so daß ich keinen Beweis finden konnte. Nach dieser ”syntaxreichen“ Zeit habe ich den wesentlichen Teil meiner Arbeit geschrieben. Ich habe eine Kategorie von Reduktionsmodellen angegeben und ihre kategoriellen Eigenschaften untersucht. Diese Aufgabe war ergiebiger und konnte sowohl eine symmetrisch monoidale Kategorie von Reduktionsmodellen als auch Konstruktionen ”neuer“ Modelle aus gegebenen Modellen zutage bringen. Und somit ward eine Diplomarbeit geboren.

Nicht nur bei der Betreuung dieser Arbeit hat mein Betreuer, Herr Keimel, außergewöhnlich viel Geduld aufgebracht. Auch bei Seminaren in früheren Semestern habe ich erfahren, daß ich mit meinen mathematischen Aufgaben auch noch dann kommen konnte, wenn sie schon ”vor Ewigkeiten“ hätten gelöst sein sollen. Für dieses Verständnis und für den mathematischen Spaß, den mir Herr Keimels Veranstaltungen gemacht haben, möchte ich mich sehr bedanken. Als sehr ergiebig habe ich auch die – leider wenigen – Treffen mit Peter Selinger empfunden. Da er in der gleichen ”Materie“ steckte wie ich, konnten wir immer sofort losdiskutieren. Hier im Hause mußte manchmal Thomas Erker das Ohr hinhalten, wenn ich ein mathematisches oder auch Latex-spezifisches Problem hatte. Ich möchte nicht verheimlichen, daß dies schnell zu (mathematischen) Auseinandersetzungen führen konnte, aber das muß wohl so sein. Um so dankbarer bin ich ihm für seine spontane stundenlange Hilfe in den letzten Tagen. Er hat in letzter Minute Teile der Arbeit korrekturgelesen, meine letzten LATEX-Probleme gelöst und mir dadurch freundschaftlichen Beistand geleistet. Der Spruch ”to leave it to the last minute“ wurde mir von Alex Rohr auf den Schreibtisch gelegt. Ich habe den Spruch über meinen Schreibtisch gehängt. Auch Alex sei gedankt, daß er im Vorfeld korrekturgelesen und ”Formalkram“ hat über sich ergehen lassen. Meiner Familie sei vielmals gedankt, daß sie mich so, wie ich wollte, und solange ich wollte hat studieren lassen. Mein Studium wurde mir durch die Fachschaftsarbeit und sonstiges Engagement besonders wichtig und wertvoll. Meine WG hat in letzter Zeit nicht viel von mir zu sehen bekommen. Genauso leise hat sie all die Hausarbeit mitgemacht, die ich habe liegenlassen. Auch ihr sei gedankt.

Darmstadt, den 30. Januar 1998

Einleitung

In dieser Diplomarbeit werden Reduktionsmodelle für den ungetypten λ-Kalkül betrachtet. Die Arbeit gliedert sich in zwei Abschnitte. Der erste Abschnitt weist Eigenschaften, die von anderen Modellen bekannt sind, für Reduktionsmodelle nach. Desweiteren werden (ordnungstheoretische) Bereiche charakterisiert, auf denen sich ein ”gutes“ kategorielles Modell angeben läßt. Im zweiten Abschnitt wird eine Kategorie spezieller Reduktionsmodelle angegeben und auf kategorielle Eigenschaften hin untersucht.

Ein Reduktionsmodell ist eine geordnete Menge derart, daß die Ordnung die β- bwz. βη-Reduktion des λ-Kalküls widerspiegelt. Gewünschte Eigenschaften der Interpretation der Terme, wie das Substitutionslemma, die Monotonie der Interpretationsfunktion in Abhängigkeit von der Variablenbelegung und die Korrektheit der Interpretation werden in Abschnitt 1.3 gezeigt. Diese Ergebnisse sind [Plo94] entnommen und nochmals und ausführlicher aufgeschrieben. Im zweiten Kapitel wird erläutert, weshalb eine Adjunktion zwischen einer geordneten Menge P und dem Exponential P^{P} ein Reduktionsmodell liefert, in dem die Terme eine möglichst große Denotation erhalten. In [Sel97] wird eine Charakterisierung einer solchen Adjunktion für Bäume mit endlicher Höhe angegeben, die von mir auf bc-Bereiche übertragen und allgemeiner für Bereiche umformuliert wird. Im dritten Kapitel werden die kategorientheoretische Grundlagen für das vierte Kapitel bereitgestellt. In diesem letzten Kapitel definiere ich eine Kategorie von Reduktionsmodellen, in der die Morphismen Ordnungseinbettungen sind. Es wird nachgewiesen, daß ein Morphismus von D nach E die Denotationen der λ-Terme in D unter die Denotationen der λ-Terme in E einbettet. Das Modell E liefert also eine ”größere“ Interpretation der Terme als D, was nach Kapitel 2 wünschenswert ist. In den Abschnitten 4.1 und 4.2 habe ich gezeigt, daß sich für Reduktionsmodelle D und E auf dem Produkt D × E der geordneten Mengen und dem Raum D^{D} aller monotonen Funktionen auf D Reduktionsmodelle definieren lassen. Man erhält zugehörige ”Produkt“- bzw. ”Exponential“-Funktoren. Leider sind diese Modelle nicht Produkte und Exponentiale im kategoriellen Sinne, jedoch läßt sich mit dem Produkt-Funktor für eine volle Unterkategorie der ursprünglichen Kategorie zeigen, daß sie symmetrisch monoidal ist.

Kenntnisse der Ordnungstheorie und des λ-Kalküls setzte ich voraus, sie können in [AJ94] und im Skript zur Vorlesung ”Einführung in den λ-Kalkül“ von Herrn Keimel erworben werden. Alle kategorientheoretischen Begriffe, die ich in Kapitel 4 benutze, werden in Kapitel 3 definiert. Man kann aber auch, ohne mit Kategorien vertraut zu sein, viele Überlegungen des Kapitels 4 nachvollziehen. Als weitere Literatur dazu sei auf [Mac71, Kap. 3] verwiesen.

1 Grundlagen

Wie in der Einleitung erwähnt wurde, werden Syntax und Semantik des λ-Kalküls als bekannt vorausgesetzt, doch zur Wiederholung und Festlegung von Bezeichnungen seien einige Definitionen angegeben.

Sei Λ die Menge der bis auf α-Äquivalenz verschiedenen λ-Terme über einer abzählbar unendlichen Variablenmenge V, d.h. λ-Terme, die sich nur durch Umbenennung gebundener Variablen unterscheiden, werden miteinander identifiziert. Für jeden Term M wird mit F V (M) wie üblich die Menge der freien Variablen von M bezeichnet.

DEFINITION 1.1 (Substitution von λ-Termen) Die Substitution von λ-Termen ist induktiv definiert:

(i) x[N/x] := N

(ii) y[N/x] := y , falls y ≠ x

(iii) (P Q)[N/x] := P [N/x]Q[N/x]

(iv)

(λy.P)[N/x] := \{ \begin{matrix}λy.P , & falls y = x \\ λy.(P [N/x]) , & falls y ≠ x, y ∉ F V (N) \\ λz.(P [z/y])[N/x] , & falls y ≠ x, y ∈ F V (N); dabei sei z \\ & eine neue Variable; \end{matrix}

Bemerkung 1.2 Die Substitution verträgt sich offensichtlich mit der α -Äquivalenz von λ-Termen, man kann also o.B.d.A. annehmen, daß in dem Ausdruck (λy.P)[N/x] für die gebundene Variable y gilt: y ∉ F V (N).

DEFINITION 1.3 (Reduktion) Ein Term M β-reduziert zu einem Term N, in Zeichen M → N, falls sich die Reduktion mit Hilfe der folgenden Axiome und Regeln herleiten läßt:

(β^{1})  (λx.M)N → M[N/x]
(ρ)  M → M
(μ)  M → M′ , N → N′ ⇒ MN → M′N′
(ξ)  M → M′ ⇒ λx.M → λx.M′

Fügt man dem Regelsystem noch das Axiom

(η)  λx.Mx → M, falls x ∉ F V (M)

hinzu, so definiert man, daß M βη-reduziert zu N, in Zeichen: M →_{βη} N, falls sich die Reduktion mit Hilfe dieser Regeln herleiten läßt.

1.1 Modelle für den ungetypten λ-Kalkül 7

Für Terme M und N definiert man die β-Äquivalenz durch:

M =_{β} N :⟺ (∃P ∈ Λ)(M → P und N → P)

Entsprechend definiert man die βη-Äquivalenz:

M =_{βη} N :⟺ (∃P ∈ Λ)(M →_{βη} P und N →_{βη} P)

Es läßt sich leicht nachrechnen, daß die angegebenen β- bzw. βη-Relationen tatsächlich Äquivalenzen sind.

1.1 Modelle für den ungetypten λ-Kalkül

Ein Modell für den λ-Kalkül ist eine Menge M zusammen mit einer Interpretationsfunktion, die jedem Term ein Element von M so zuweist, daß eine gewünschte Korrektheitseigenschaft erfüllt ist. Dabei hängt die Interpretation von der Belegung der freien Variablen des Terms durch Elemente von M ab. Man definiert die Interpretationsfunktion ⟦.⟧_{.} durch:

⟦.⟧_{.} : Λ × M^{V} → M
(M, ρ) ↦ ⟦M⟧_{ρ}

Der Interpretationswert eines Terms (zu einer gegebenen Belegung ρ) wird auch Denotation des Terms genannt. Üblicherweise werden Modelle untersucht, die die β-Äquivalenz oder auch die βη-Äquiva-lenz respektieren. Die gewünschte Korrektheit besagt dann, daß β-äquivalente Terme bzw. βη-äquivalente Terme unter jeder Variablenbelegung gleich interpretiert werden.

DEFINITION 1.4 Das Paar (M, ⟦.⟧_{.}) heißt ein Modell für die β-Äquivalenz, falls gilt:

(∀M, N) M =_{β} N ⇒ (∀ρ) ⟦M⟧_{ρ} = ⟦N⟧_{ρ}

Bemerkung 1.5 (i) Es wurde stillschweigend vorausgesetzt, daß M und N λ-Terme sind und ρ : V → M eine Variablenbelegung bezeichnet. Geht die Bedeutung von diesen Bezeichnern aus dem Zusammenhang offensichtlich hervor, so wollen wir ihre Deklaration auch in Zukunft weglassen.

(ii)

Für jedes a ∈ M sei definiert ρ_{(x↦a)}(y) := \{ \begin{matrix}ρ(y) , & falls y ≠ x \\ a , & falls y = x \end{matrix}

(iii) Natürlich läßt sich analog zur Definition 1.4 ein Modell für die βη-Äquivalenz definieren durch:

(∀M, N) M =_{βη} N ⇒ (∀ρ) ⟦M⟧_{ρ} = ⟦N⟧_{ρ}

1.2 Reduktionsmodelle

Eine andere Klasse von Modellen wird gegeben durch Reduktionsmodelle. Hierbei werden die λ-Terme in einer geordneten Menge interpretiert und zwar derart, daß die β-Reduktion modelliert wird. Gilt also M → N, so ist ⟦M⟧ ≤ ⟦N⟧. In [Bar84, Chap. 5] wird der Begriff eines syntaktischen Modells für die β-Äquivalenz angegeben. Reduktionsmodelle werden in [Sel97, Chap. 4] und [Plo94] als Verallgemeinerung davon definiert. Stattet man Barendregts Modelle mit der trivialen Ordnung aus, d.h. x ≤ y genau dann, wenn x = y, so erhält man folgende Definition:

DEFINITION 1.6 Eine geordnete Menge mit einer zweistelligen monotonen Operation heißt geordnete applikative Struktur. Sei (P, ≤, ·) eine solche Struktur und sei eine Interpretationsfunktion

⟦.⟧_{.} : Λ × P^{V} → P
(M, ρ) ↦ ⟦M⟧_{ρ}

gegeben, so daß für alle ρ, ρ′ ∈ P^{V}, für alle M, N ∈ Λ und für alle x ∈ V die folgenden Eigenschaften gelten:

(1) ⟦x⟧_{ρ} = ρ(x)

(2) ⟦MN⟧_{ρ} = ⟦M⟧_{ρ} · ⟦N⟧_{ρ}

(3) ρ|_{F V (M)} = ρ′|_{F V (M)} ⇒ ⟦M⟧_{ρ} = ⟦M⟧_{ρ′}

(4) ((∀a ∈ P) ⟦M⟧_{ρ(x↦a)} ≤ ⟦N⟧_{ρ(x↦a)}) ⇒ ⟦λx.M⟧_{ρ} ≤ ⟦λx.N⟧_{ρ}

(5) (∀a ∈ P) ⟦λx.M⟧_{ρ} · a ≤ ⟦M⟧_{ρ(x↦a)}

Dann heißt (P, ≤, ·, ⟦.⟧_{.}) ein Modell für die β-Reduktion oder auch kurz Reduktionsmodell. Gilt zusätzlich die Eigenschaft

(6) ⟦λx.Mx⟧_{ρ} ≤ ⟦M⟧_{ρ}, falls x ∉ F V (M),

dann heißt (P, ≤, ·, ⟦.⟧_{.}) ein Modell für die βη-Reduktion. Wir schreiben auch nur P, wenn die Ordnung, die Applikation und die Interpretation klar sind.

Daß die in Definition 1.6 angegebene Struktur P tatsächlich korrekt bzgl. der β- bzw. βη-Reduktion ist, wird nachgerechnet in dem letzten der folgenden drei Lemmata. Die Beweisideen sind entnommen aus [Plo94].

1.3 Eigenschaften von Reduktionsmodellen

Lemma 1.7 (Substitutionslemma)

(∀ρ)(∀M, N) ⟦M[N/x]⟧_{ρ} = ⟦M⟧_{ρ(x↦⟦N⟧_{ρ})}

Beweis: (induktiv über den Aufbau von M)

M ≡ y und y ≠ x

⟦y[N/x]⟧_{ρ} = ⟦y⟧_{ρ} = ⟦y⟧_{ρ(x↦⟦N⟧_{ρ})}

M ≡ x

⟦x[N/x]⟧_{ρ} = ⟦N⟧_{ρ} = ⟦x⟧_{ρ(x↦⟦N⟧_{ρ})}

M ≡ P Q ⟦(P Q)[N/x]⟧_{ρ} =^{Def.Subst.} ⟦P [N/x]Q[N/x]⟧_{ρ} =^{1.6(2)} ⟦P [N/x]⟧_{ρ} · ⟦Q[N/x]⟧_{ρ} =^{Ind.Vor.}

⟦P ⟧_{ρ(x↦⟦N⟧_{ρ})} · ⟦Q⟧_{ρ(x↦⟦N⟧_{ρ})} =^{1.6(2)} ⟦(P Q)⟧_{ρ(x↦⟦N⟧_{ρ})}

M ≡ λy.P

Fall 1: x ∉ F V (N)

(a): y = x

⟦(λy.P)[N/x]⟧_{ρ} =^{Vor.} ⟦(λy.P)[N/y]⟧_{ρ} =^{Def. Subst.} ⟦λy.P ⟧_{ρ} =^{y∉F V (λy.P)}

⟦λy.P ⟧_{ρ(y↦⟦N⟧_{ρ})} =^{Vor.} ⟦λy.P ⟧_{ρ(x↦⟦N⟧_{ρ})}

(b): y ≠ x

Wie schon in Bemerkung 1.2 festgestellt, können wir o.B.d.A. annehmen, daß y ∉ F V (N) ist. Wir wollen nun zeigen:

⟦(λy.P)[N/x]⟧_{ρ} = ⟦λy.P ⟧_{ρ(x↦⟦N⟧_{ρ})}  (1)

Der linke Term läßt sich umformen:

⟦(λy.P)[N/x]⟧_{ρ} = ⟦λy.(P [N/x])⟧_{ρ} = ⟦λy.(P [N/x])⟧_{ρ(x↦⟦N⟧_{ρ})}

(da nach Vor. x ∉ F V (N), also x ∉ F V (λy.P [N/x])) Es bleibt also zu zeigen:

⟦λy.(P [N/x])⟧_{ρ(x↦⟦N⟧_{ρ})} = ⟦λy.P ⟧_{ρ(x↦⟦N⟧_{ρ})}  (2)

Mit ψ := ρ(x ↦ ⟦N⟧_{ρ}) schreibt sich die Gleichung als

⟦λy.(P [N/x])⟧_{ψ} = ⟦λy.P ⟧_{ψ}  (3)

Nach 1.6(4) erhält man diese Gleichheit, falls gilt:

(∀a ∈ P) ⟦P [N/x]⟧_{ψ(y↦a)} = ⟦P ⟧_{ψ(y↦a)}  (4)

Die Induktionsvoraussetzung für P besagt, daß für alle a ∈ P gilt:

⟦P [N/x]⟧_{ψ(y↦a)} = ⟦P ⟧_{ψ(y↦a,x↦⟦N⟧_{ψ(y↦a)})}

Der rechte Term rechnet sich wegen x, y ∉ F V (N) aus zu

⟦P ⟧_{ψ(y↦a,x↦⟦N⟧_{ρ})} =^{Def. ψ} ⟦P ⟧_{ψ(y↦a)}, womit (4) gezeigt wäre.

Fall 2: x ∈ F V (N)

Benenne den ”Platzhalter“ x in M in eine neue Variable z um und betrachte den Term M[N/z]. Jetzt läßt sich der schon bewiesene Fall 1 anwenden. Sei also z ∈ V, z ∉ F V (MN). Dann ist

⟦M[N/x]⟧_{ρ} = ⟦M[z/x][N/z]⟧_{ρ}
= ⟦M[z/x]⟧_{ρ(z↦⟦N⟧_{ρ})}  (nach Fall 1, mit z ∉ F V (N))
= ⟦M⟧_{ρ(z↦⟦N⟧_{ρ},x↦⟦z⟧_{ρ(z↦⟦N⟧ρ)})}  (nach Fall 1, mit x ∉ F V (z))
= ⟦M⟧_{ρ(z↦⟦N⟧_{ρ},x↦⟦N⟧_{ρ})} =^{z∉F V (M)} ⟦M⟧_{ρ(x↦⟦N⟧_{ρ})}

Folgerung 1.8 (Lemma für mehrfache Substitution) Sind x_{1}, …, x_{n} Variablen und N_{1}, …, N_{n} λ-Terme derart, daß (∀i) x_{i} ∉ F V (N_{1}) ∪ … ∪ F V (N_{i−1}) gilt, so gilt auch für die mehrmals hintereinander durchgeführte Substitution:

⟦M[N_{1}/x_{1}] … [N_{n}/x_{n}]⟧_{ρ} = ⟦M⟧_{ρ(x_{1}↦⟦N_{1}⟧_{ρ},...,x_{n}↦⟦N_{n}⟧_{ρ})}

Beweis: n-faches Anwenden des obigen Substitutionslemmas liefert das gewünschte Ergebnis.

Lemma 1.9 ⟦.⟧_{.} : V × P^{V} → P ist monoton im zweiten Argument, d.h.

wenn ρ ≤ ρ′, dann (∀M) ⟦M⟧_{ρ} ≤ ⟦M⟧_{ρ′}

Beweis: (induktiv über den Aufbau von M)

M ≡ x : ⟦x⟧_{ρ} =^{1.6(1)} ρ(x) ≤ ρ′(x) =^{1.6(1)} ⟦x⟧′_{ρ}

M ≡ P Q : ⟦P Q⟧_{ρ} =^{1.6(2)} ⟦P ⟧_{ρ} · ⟦Q⟧_{ρ} ≤ ⟦P ⟧_{ρ′} · ⟦Q⟧_{ρ′} (Ind.Vor. für P, Q, · monoton)

=^{1.6(2)} ⟦P Q⟧_{ρ′}

M ≡ λx.P : Für eine Liste \overline{x} von Variablen und eine Belegung ρ sei mit ρ(\overline{x}) die Liste der Belegungen und mit ⟦\overline{x}⟧_{ρ} die Liste der Interpretationen der Variablen aus \overline{x} unter ρ bezeichnet. Sei nun ρ ≤ ρ′ gegeben, und sei \overline{y} eine Liste der freien Variablen von λx.P, die kein Element mehrfach enthält. Sei \overline{z} eine Liste gleicher Länge wie \overline{y}, die nur Variablen verschieden von x und verschieden von denen aus \overline{y} enthält. Wir ”simulieren“ mit \overline{z} die freien Variablen von λx.P : Definiere ρ′′ := ρ′(\overline{z} ↦ ρ(\overline{y})). Die Struktur des Beweises ist nun die folgende:

(a) \overline{z} ”verhält sich“ unter ρ′′ wie \overline{y} unter ρ. Später rechnen wir nach:

⟦λx.P ⟧_{ρ} = ⟦(λx.P)[\overline{z}/\overline{y}]⟧_{ρ′′}  (5)
(∀a ∈ P) ⟦P [\overline{z}/\overline{y}]⟧_{ρ′′(x↦a)} = ⟦P ⟧_{ρ(x↦a)}  (6)

(b) \overline{y} ”verhält sich“ unter ρ′′ wie \overline{y} unter ρ′, d.h. ρ′′|\overline{y} = ρ′|\overline{y} , folglich
⟦λx.P ⟧_{ρ′′} = ⟦λx.P ⟧_{ρ′}  (7)

Da P als freie Variablen nur \overline{y} und eventuell x enthält, ist:

(∀a ∈ P) ⟦P ⟧_{ρ′(x↦a)} = ⟦P ⟧_{ρ′′(x↦a)}  (8)

(c) Wir erhalten für alle a ∈ P:

⟦P [\overline{z}/\overline{y}]⟧_{ρ′′(x↦a)} =^{(6)} ⟦P ⟧_{ρ(x↦a)} ≤^{Ind.Vor. für P} ⟦P ⟧_{ρ′(x↦a)} =^{(8)} ⟦P ⟧_{ρ′′(x↦a)}

Wendet man 1.6(4) an, so folgt die Ungleichung

⟦(λx.P)[\overline{z}/\overline{y}]⟧_{ρ′′} =^{Def. Subst.} ⟦λx.(P [\overline{z}/\overline{y}])⟧_{ρ′′} ≤ ⟦λx.P ⟧_{ρ′′}  (9)

(d) Das Gewünschte ergibt sich durch:

⟦λx.P ⟧_{ρ} =^{(5)} ⟦(λx.P)[\overline{z}/\overline{y}]⟧_{ρ′′} ≤^{(9)} ⟦λx.P ⟧_{ρ′′} =^{(7)} ⟦λx.P ⟧_{ρ′}

(e) Nachzuweisen bleiben (5) und (6):

zu (5): ⟦λx.P ⟧_{ρ} =^{1.6(3)} ⟦λx.P ⟧_{ρ′′(\overline{y}↦ρ(\overline{y}))} =^{1.6(3)} ⟦(λx.P ⟧_{ρ′′(\overline{y}↦⟦\overline{z}⟧_{ρ′′})} =^{Subst.Lemma}

⟦(λx.P)[\overline{z}/\overline{y}]⟧_{ρ′′}

zu (6): Sei a ∈ P. Dann gilt:

⟦P [\overline{z}/\overline{y}]⟧_{ρ′′(x↦a)} =^{Subst.Lemma} ⟦P ⟧_{ρ′′(x↦a, \overline{y}↦⟦\overline{z}⟧_{ρ′′(x↦a)})} =^{x∉F V (\overline{z})}

⟦P ⟧_{ρ′′(x↦a, \overline{y}↦⟦\overline{z}⟧_{ρ′′})} =^{Def.ρ′′} ⟦P ⟧_{ρ′′(x↦a, \overline{y}↦ρ(\overline{y}))} = ⟦P ⟧_{ρ(x↦a)}

weil F V (P) ⊆ \{x, \overline{y}\} und erneut wegen 1.6(3).

Als letzte und interessante Eigenschaft zeigen wir, daß Modelle für die β- bzw. βη-Reduktion tatsächlich die β- bzw. βη-Reduktion modellieren. Da jede β-Reduktion im besonderen eine βη-Reduktion ist, reicht es, folgendes Lemma zu zeigen:

Lemma 1.10 (Korrektheit) Wenn M →_{βη} N, dann (∀ρ) ⟦M⟧_{ρ} ≤ ⟦N⟧_{ρ}.

Beweis: (induktiv über die Herleitung von M →_{βη} N)

• Sei M ≡ (λx.P)Q und N ≡ P [Q/x], betrachte also die Reduktion (λx.P)Q → P [Q/x]. Dann rechnet man für eine beliebige Belegung ρ nach:

⟦(λx.P)Q⟧_{ρ} =^{1.6(2)} ⟦λx.P ⟧_{ρ} · ⟦Q⟧_{ρ} ≤^{1.6(5)} ⟦P ⟧_{ρ(x↦⟦Q⟧_{ρ})} =^{Subst.Lemma} ⟦P [Q/x]⟧_{ρ}, also

(∀ρ) ⟦M⟧_{ρ} ≤ ⟦N⟧_{ρ}.

• Ist M ≡ P Q und existieren P′, Q′ derart, daß P → P′, Q → Q′, dann läßt sich die Reduktion P Q → P′Q′ durchführen. Mit N :≡ P′Q′ erhält man für jede Belegung ρ:

⟦P Q⟧_{ρ} =^{1.6(2)} ⟦P ⟧_{ρ} ·⟦Q⟧_{ρ} ≤ ⟦P′⟧_{ρ} ·⟦Q′⟧_{ρ} , da · monoton ist und für P, Q die Induktions-

voraussetzung gilt. Wir rechnen weiter ⟦P′⟧_{ρ} · ⟦Q′⟧_{ρ} =^{1.6(2)} ⟦P′Q′⟧_{ρ}, also ⟦M⟧_{ρ} ≤ ⟦N⟧_{ρ}.

• Ist M ≡ λx.P und existiert ein P′ derart, daß P → P′, so erhält man die Reduktion λx.P → λx.P′. Definiere N :≡ λx.P′. Nach Voraussetzung gilt P → P′. Mit der Induktionsannahme folgt dann (∀ρ)⟦P ⟧_{ρ} ≤ ⟦P′⟧_{ρ}. Demnach gilt auch (∀a ∈ P)(∀ρ)⟦P ⟧_{ρ(x↦a)} ≤ ⟦P′⟧_{ρ(x↦a)}, und mit 1.6(4) ist ⟦λx.P ⟧_{ρ} ≤ ⟦λx.P′⟧, d.h. (∀ρ) ⟦M⟧_{ρ} ≤ ⟦N⟧_{ρ}.

• Sei M ≡ λx.P x und es gelte x ∉ F V (P). Dann läßt sich die Reduktion λx.P x →_{βη} P betrachten. Sei N :≡ P. Für jede Belegung ρ gilt mit 1.6(6) offensichtlich ⟦λx.P x⟧_{ρ} ≤ ⟦P ⟧_{ρ}, d.h. (∀ρ) ⟦M⟧_{ρ} ≤ ⟦N⟧_{ρ}.

2 Kategorielle Modelle

Eine Möglichkeit, ein Reduktionsmodell zu finden, ist die Konstruktion eines kategoriellen Modells. Wir beginnen mit einer geordneten Menge P und suchen eine Applikation darauf derart, daß die erhaltene geordnete applikative Struktur ein Reduktionsmodell ist. Mit Hilfe des Funktionenraums P^{P} der monotonen Funktionen auf P läßt sich ein hinreichendes Kriterium für die Existenz einer solchen applikativen Struktur formulieren:

SATZ 2.1 Sei P eine geordnete Menge, und seien monotone Abbildungen e: P → P^{P} und p: P^{P} → P gegeben, so daß die Ungleichung e ∘ p ≤ id_{P^{P}} gilt.

P^{P}
[figure: p; ≤]
[figure: P; e; P^{P}; ^{id^{P^{P}}}]

Dann läßt sich eine Applikation definieren durch

·: P × P → P
(a, x) ↦ a · x := e(a)(x),

die P zu einer geordneten applikativen Struktur macht. Die Menge P wird zu einem Reduktionsmodell durch die folgende induktiv definierte Interpretation von λ-Termen:

(∀x)(∀M, N)(∀ρ)  ⟦x⟧_{ρ} := ρ(x)
⟦MN⟧_{ρ} := e(⟦M⟧_{ρ})(⟦N⟧_{ρ})
⟦λx.M⟧_{ρ} := p(a ↦ ⟦M⟧_{ρ(x↦a)})

Beweis: Die Applikation ist monoton im ersten Argument, denn e ist als monoton vorausgesetzt. Ist a ≤ b, dann folgt e(a) ≤ e(b). Im besonderen gilt dann für jedes x ∈ P die Ungleichung a·x = e(a)(x) ≤ e(b)(x) = b·x. Die Applikation ist auch im zweiten Argument monoton, da die Abbildung e jedes a ∈ P auf eine monotone Funktion e(a) abbildet. Somit ist (P, ≤, ·) eine geordnete applikative Struktur. Für den Nachweis, daß P durch die angegebene Interpretationsfunktion ⟦.⟧_{.} zu einem Reduktionsmodell wird, sind die Eigenschaften (1) bis (5) der Definition 1.6 zu zeigen. Die Eigenschaften (1) und (2) folgen sofort aus der Festsetzung ⟦x⟧_{ρ} := ρ(x) und ⟦MN⟧_{ρ} := e(⟦M⟧_{ρ})(⟦N⟧_{ρ}) = ⟦M⟧_{ρ} · ⟦N⟧_{ρ}. Zu (3): Seien ρ, ρ′ mit ρ|_{F V (M)} = ρ′|_{F V (M)} gegeben. Eine Induktion über den Aufbau von M zeigt, daß ⟦M⟧_{ρ} = ⟦M⟧_{ρ′} gilt: für M ≡ x und M ≡ P Q ist dies wegen (1) und (2) und der Induktionsvoraussetzung für P und Q klar. Sei M ≡ λx.P. Da die Variable x im Term λx.P gebunden ist, gilt F V (λx.P) = F V (P)\{x}. Nach Voraussetzung der zu beweisenden Implikation ist ρ|_{F V (λx.P)} = ρ′|_{F V (λx.P)}. Für alle a ∈ P ist demnach ρ_{(x↦a)}|_{F V (P)} = ρ′_{(x↦a)}|_{F V (P)}. Die Induktionsvoraussetzung für P liefert für alle a ∈ P die Gleichung ⟦P ⟧_{ρ(x↦a)} = ⟦P ⟧_{ρ′(x↦a)}. Mit der Interpretation eines abstrahierten Terms erhalten wir

⟦λx.P ⟧_{ρ} =^{def} p(a ↦ ⟦P ⟧_{ρ(x↦a)})
= p(a ↦ ⟦P ⟧_{ρ′(x↦a)})
= ⟦λx.P ⟧_{ρ′}

Wir haben nun ⟦M⟧_{ρ} = ⟦M⟧_{ρ′} gezeigt. Die Eigenschaft (4) gilt nach Definition der Interpretation, denn nach Voraussetzung ist für alle a ∈ P gegeben: ⟦M⟧_{ρ(x↦a)} ≤ ⟦N⟧_{ρ(x↦a)}. Also ist

⟦λx.M⟧_{ρ} =^{def} p(a ↦ ⟦M⟧_{ρ(x↦a)}) ≤ p(a ↦ ⟦N⟧_{ρ(x↦a)}) =^{def} ⟦λx.N⟧_{ρ}.

Zuletzt bleibt die Eigenschaft (5) zu zeigen. Für alle a ∈ P gilt:

⟦λx.M⟧_{ρ} · a =^{Def. ⟦.⟧_{.}} (p(a ↦ ⟦M⟧_{ρ(x↦a)})) · a =^{Def. ·} \underbrace{e(p}_{≤id_{P^{P}}} (a ↦ ⟦M⟧_{ρ(x↦a)}))(a) ≤ ⟦M⟧_{ρ(x↦a)}

Folglich ist (P, ≤, ·) ein Reduktionsmodell, und der Satz ist bewiesen.

DEFINITION 2.2 Ist P ein Reduktionsmodell, das durch die Abbildungen e, p wie in Satz 2.1 gegeben ist, so wird es auch mit (P, e, p) bezeichnet und kategorielles Reduktionsmodell genannt.

In dem Satz 2.1 wurde auf einem kategoriellen Modell (P, e, p) eine Applikation ·: P × P → P, a · x = e(a)(x) definiert. Ist umgekehrt eine geordnete applikative Struktur (P, ≤ , ·) gegeben, so läßt sich eine monotone Abbildung e: P → P^{P} definieren durch e(a) := (x ↦ a · x). Möchte man (P, ≤, e) zu einem kategoriellen Modell ergänzen, so ist durch die Eigenschaften (1) und (2) von Definition 1.6 die Interpretation der Variablen und die der Applikation von Termen festgelegt. Eine Wahl bleibt für die Interpretation abstrahierter Terme, d.h. für die Definition von p: P^{P} → P. Ist P derart geordnet, daß Elemente, die ”weiter oben“ in P liegen, ”besser“ sind als Elemente, die ”weiter unten“ liegen, so möchte man die λ-Terme ”möglichst groß“ interpretieren. Eine solche Ordnung ist die ”Informationsordnung“: größere Elemente tragen eine ”größere Information“. Diese Ordnung wird an folgendem Beispiel erläutert: wir betrachten das Einheitsintervall [0, 1] ⊆ ℝ mit der üblichen Ordnung und Multiplikation und definieren P als die Menge aller abgeschlossenen Intervalle von [0, 1]. Jede reelle Zahl r ∈ [0, 1] läßt sich als einpunktige Menge in P wiederfinden. Ein Intervall [a, b] kann nun als Näherung für r definiert werden, wenn r ∈ [a, b] gilt. Ist des weiteren ein Intervall [c, d] gegeben mit [c, d] ⊆ [a, b] und r ∈ [c, d], so liefert das Intervall [c, d] mindestens so viel ”Information“ über die Zahl r wie das Intervall [a, b], da das Intervall [c, d] die Zahl r mindestens so eng ”begrenzt“. Insofern kann man sagen, daß [c, d] eine ”bessere“ Näherung für r ist als [a, b].

Deshalb geben wir dem Intervall [c, d] eine größeren Wert in P als dem Intervall [a, b] und definieren: [a, b] ≤ [c, d] :⟺ [a, b] ⊇ [c, d], d.h. die kleineren ”kleinere“ Intervalle sind größer in P. Definiert man noch die monotone Applikation auf P durch [a, b] · [c, d] := [a · c, b · d], so ist (P, ≤, ·) eine geordnete applikative Struktur. Das Beispiel der abgeschlossenen reellen Intervalle hat erklärt, was es heißt, daß Elemente einer Menge P ”besser“ sind als andere. Ordnen wir P entsprechend, so daß ”weiter oben“ die ”besseren“ liegen, und statten P noch mit einer monotonen Applikation aus, dann erhalten wir eine ”gutes“ Modell, wenn wir die Terme möglichst groß interpretieren. Nun läßt sich induktiv über den Aufbau eines Terms M zeigen, daß je größer p gewählt wird, desto größer wird die Interpretation ⟦λx.M⟧_{ρ} := p(a ↦ ⟦M⟧_{ρ(x↦a)}). Für ein kategorielles Modell muß weiterhin gelten: e ∘ p ≤ id_{P^{P}}. Man sucht also zu (P, e) die größte monotone Funktion p: P^{P} → P, für die gilt: e ∘ p ≤ id_{P^{P}}. Allgemein definiert man:

DEFINITION 2.3 Seien Pund Q geordnete Mengen. Dann ist eine Adjunktion von P nach Q gegeben durch ein Paar monotoner Funktionen e: P → Q, q: Q → P, so daß gilt: p∘e ≥ id_{P} und e∘p ≤ id_{Q}. Man sagt, daß e linksadjungiert zu p und p rechtsadjungiert zu e ist und schreibt e ⊣ p.

Nachdem man im Kapitel 3 die Begriffe ‘Kategorie’ und ‘natürliche Transformation’ definiert hat, könnte man auch allgemein den Begriff der Adjunktion zwischen Kategorien definieren. Wir interessieren uns in dieser Arbeit aber nur für Adjunktionen zwischen geordneten Mengen, die wir als Kategorien auffassen. In diesem Spezialfall lassen sich Adjunktionen jedoch leichter wie in der Definition 2.3 angeben.

Hilfssatz 2.4 Seien Pund Q geordnete Mengen, und seien monotone Funktionen e: P → Q, p: Q → P gegeben. Dann ist e linksadjungiert zu p genau dann, wenn p die größte Funktion aus Q^{P} ist, für die e ∘ p ≤ id_{Q} gilt.

Beweis: Die Äquivalenz dieser Bedingungen kann von den LeserInnen dieser Arbeit entweder selbst nachgewiesen werden oder in [AJ94, Prop. 3.1.10.] nachgelesen werden.

Den Beweis des letzten Hilfssatzes hätte ich auch als ‘Übungsaufgabe’ stellen können. Da dies aber in Diplomarbeiten unüblich ist, verzichte ich darauf.

⌣ ··

Die bisherigen Überlegungen zeigen

Folgerung 2.5 Ist (P, ≤, ·) eine geordnete applikative Struktur, und definiert man e: P → P^{P} durch e(a) := (x ↦ a · x), so gibt es auf (P, ≤, e) genau dann ein kategorielles Modell mit größtmöglicher Interpretation , wenn es eine Rechtsadjungierte p: P^{P} → P zu e gibt.

Weitere Literatur zu Reduktionsmodellen ist zu finden in [Peter, Chap. 4]. Im nächsten Abschnitt charakterisieren wir für spezielle geordnete applikative Strukturen die Existenz von Adjunktionen.

2.1 Charakterisierung von Adjunktionen

In [Sel97, Chap. 4] wird eine Charakterisierung dafür angegeben, wann eine geordnete applikative Struktur auf einem Baum mit endlicher Höhe ein kategorielles Modell liefert. Im folgenden wird gezeigt, daß sich die Charakterisierung leicht auf geordnete applikative Strukturen auf bc-Bereichen übertragen läßt. Zusätzlich wird eine allgemeine Formulierung für geordnete applikative Strukturen auf Bereichen angegeben, die allerdings nichts mehr besagt, als daß das Urbild eines Hauptideals unter einer linken Adjungierten wieder ein Hauptideal sein muß.

Bezeichnung Ist P geordnet und sind a, b ∈ P nach oben gemeinsam beschränkt, so schreibt man a ⌢ b.

DEFINITION 2.6 Sei P eine geordnete Menge. Eine nichtleere Teilmenge M ⊆ P heißt gerichtet, falls gilt: (∀x, y ∈ M)(∃z ∈ M) x, y ≤ z. Eine geordnete Menge P heißt Bereich, falls jede gerichtete Teilmenge ein Supremum hat. Desweiteren nennt man einen Bereich P einen bc-Bereich (engl.: bounded-complete), falls für alle x, y ∈ P gilt: wenn x ⌢ y gilt, dann existiert das Supremum sup{x, y} ∈ P. Eine geordnete Menge, in der beliebige Suprema und Infima existieren, heißt vollständiger Verband.

DEFINITION 2.7 Sei (P, ·) eine geordnete applikative Struktur und sei e: P → P^{P}, e(a) := (x ↦ a · x). Die Struktur heißt gleichmäßig extensional, falls für alle a, b ∈ P und alle f ∈ P^{P} gilt:

Wenn e(a), e(b) ≤ f , dann (∃c ∈ P)(a, b ≤ c und e(c) ≤ f).

Die Struktur heißt streng extensional, falls für alle a, b ∈ P gilt:

Wenn (∀x) a · x ⌢ b · x , dann a ⌢ b.

Hilfssatz 2.8 Ist eine Adjunktion e ⊣ p zwischen geordneten Mengen P und Q gegeben, so erhält e alle existierenden Suprema, d.h. falls sup_{i} x_{i} in P existiert, so existiert sup_{i} e(x_{i}) in Q und es ist e(sup_{i} x_{i}) = sup_{i} e(x_{i}).

Beweis: Man beachte die Zeichnung, die dem Beweis folgt. Es existiere x := sup_{i} x_{i} ∈ P. Da e monoton ist, gilt (∀i) e(x_{i}) ≤ e(x). Somit ist e(x) eine obere Schranke für {e(x_{i}) | i}. Sei z eine andere obere Schranke, d.h. (∀i) e(x_{i}) ≤ z. Weil p monoton ist und da, wegen e ⊣ p, die Ungleichung id_{P} ≤ p ∘ e gilt, ergibt sich (∀i) x_{i} ≤ p(e(x_{i})) ≤ p(z). Also ist auch x = sup_{i} x_{i} ≤ p(z). Die Adjunktion e ⊣ p liefert außerdem e ∘ p ≤ id_{Q}, also folgt mit der Monotonie von e die Ungleichung e(x) ≤ e(p(z)) ≤ z. Das Element e(x) ist demnach kleiner oder gleich jeder oberen Schranke z von {e(x_{i}) | i}. Somit ist sup_{i} e(x_{i}) = e(x) = e(sup_{i} x_{i}).

P  Q  • z
[figure: p(z) •; e(p(z)) •]
[figure: x; •; •; p(e(x_{i})); e(x); •]
[figure: x_{i}; •; e(x_{i}); •]

Der nächste Satz charakterisiert die gewünschte Adjunktion auf Bereichen.

SATZ 2.9 Sei (P, ·) eine geordnete applikative Struktur auf einem Bereich P. Definiere e: P → P^{P}, e(a) := (x ↦ a · x). Dann gilt: die Funktion e hat eine Rechtsadjungierte genau dann, wenn e alle existierenden Suprema erhält und (P, ·) gleichmäßig extensional ist.

Beweis: ”⇐“: Für alle f ∈ P^{P} definiere P_{f} := e^{−1}(↓f) = {b ∈ P | e(b) ≤ f}. Nach Voraussetzung ist (P, ·) gleichmäßig extensional, was gerade besagt, daß für alle f ∈ P^{P} die Menge P_{f} gerichtet ist. Da P ein Bereich ist, existiert sup P_{f}. Jetzt können wir eine Rechtsadjungierte zu e definieren durch

p: P^{P} → P
f ↦ sup P_{f}

Die Funktion p ist monoton, denn falls f ≤ f′ gilt, so ist P_{f} = e^{−1}(↓ f) ⊆ e^{−1}(↓ f′) = P_{f′}. Um die Adjunktion e ⊣ p nachzuweisen, rechnen wir nach:

a) id_{P} ≤ p ∘ e : Für a ∈ P gilt a ∈ {b ∈ P | e(b) ≤ e(a)} = P_{e(a)}. Deshalb ist a ≤ sup P_{e(a)}, nach Definition von p ist also a ≤ p(e(a)).

b) e∘p ≤ id_{P^{P}} : Sei f ∈ P^{P}. Da e existierende Suprema erhält, berechnet man e(p(f)) = e(sup P_{f}) = sup e(P_{f}) ≤ f. Letztere Ungleichung gilt, weil die Menge e(P_{f}) durch f beschränkt ist. Wir haben somit für alle f ∈ P^{P} e(p(f)) ≤ f nachgewiesen.

”⇒“: Sei p ∈ P^{P} und e ⊣ p. In Hilfssatz 2.8 haben wir gezeigt, daß Linksadjungierte existierende Suprema erhalten. Es bleibt also nur noch die gleichmäßige Extensionalität nachzuweisen: Seien a, b ∈ P, f ∈ P^{P}und e(a), e(b) ≤ f. Da p monoton ist und wegen e ⊣ p die Ungleichung id_{P} ≤ p ∘ e gilt, folgt a ≤ p(e(a)) ≤ p(f) und b ≤ p(e(b)) ≤ p(f). Also ist c := p(f) eine obere Schranke für a und b, und wegen e ⊣ p ist auch e ∘ p ≤ id_{P^{P}}, also e(c) = e(p(f)) ≤ f. Somit ist (P, ·) gleichmäßig extensional.

Im Teil b) des letzten Beweises haben wir e(sup P_{f}) ≤ f nachgerechnet. Folglich gilt sup P_{f} ∈ {b ∈ P | e(b) ≤ f} = P_{f}, also ist sup P_{f} maximal in P_{f}. Wir hätten die Rechtsadjungierte somit auch durch den Ausdruck p(f) := max P_{f} definieren können.

Nach [AJ94, Prop. 3.1.10] ist für e: P → Q, p: Q → P genau dann e ⊣ p gegeben, wenn (∀f ∈ Q) p(f) = max e^{−1}(↓ f). Diese Formel ist durch die Funktion p offensichtlich erfüllt. Die Teile a) und b) des Beweises wurden nur geführt, weil wir Adjunktionen durch die Eigenschaften id_{P} ≤ p ∘ e und e ∘ p ≤ id_{Q} definiert hatten. Die Definition wurde deshalb so gewählt, weil im Kapitel 4 spezielle Adjunktionen, nämlich Einbettungs-Projektions-Paare untersucht werden, für die sogar id_{P} = p ∘ e gilt.

Folgerung 2.10 (aus dem Satz 2.9) In einem vollständigen Verband P existieren alle Suprema. Deshalb kann die zusätzliche Voraussetzung im Satz 2.9 der gleichmäßigen Extensionalität von (P, ·) für einen vollständigen Verband P weggelassen werden. In diesem Fall gilt also: eine Adjunktion e ⊣ p, e: P → P^{P}, p: P^{P} ↦ P ist schon dann gegeben, wenn e alle Suprema erhält.

Sucht man eine Adjunktion im Falle einer geordneten applikativen Struktur auf einem bc-Bereich, so kann die gleichmäßige Extensionalität ersetzt werden durch die strenge Extensionalität, die sich allein mit der Struktur auf (P, ·) formulieren läßt, ohne den Funktionenraum P^{P} zu betrachten. In Anlehnung an die Charakterisierung der Adjunktion auf Bäumen mit endlicher Höhe in [Sel97, Prop. 4.3.] zeigt man das

Lemma 2.11 Sei (P, ·) eine geordnete applikative Struktur auf einem bc-Bereich und e: P → P^{P} definiert durch e(a) := (x ↦ a · x). Genau dann hat e eine Rechtsadjungierte, wenn e alle existierenden Suprema erhält und (P, ·) streng extensional ist.

Beweis: ” ⇐ “: Wie auch schon im Beweis des Satzes 2.9 muß man zeigen, daß für alle f ∈ P^{P} das Supremum sup P_{f} := sup e^{−1}(↓ f) existiert, weshalb wir P_{f} als gerichtet nachweisen. Seien a, b ∈ P_{f}, d.h. e(a), e(b) ≤ f. Dann gilt für alle x ∈ P: die Elemente a · x, b · x sind beschränkt durch f(x). Wegen der strengen Extensionalität von (P, ·) sind dann auch a und b beschränkt. Die Funktionen e(a) und e(b) sind beschränkt durch f, und da P und somit auch P^{P} bc-Bereiche sind, existieren nun die Suprema sup{a, b} und sup{e(a), e(b)}. Nach Voraussetzung erhält e existierende Suprema und es gilt: e(sup{a, b}) = sup{e(a), e(b)} ≤ f. Also ist sup{a, b} ∈ P_{f}, die Menge P_{f} gerichtet und sup P_{f} existiert. Der restliche Teil dieser Beweisrichtung stimmt mit dem Beweis des vorherigen Satzes 2.9 überein. ” ⇒ “: Unter Voraussetzung der Adjunktion e ⊣ p bleibt wegen Hilfssatz 2.8 nur noch zu zeigen, daß (P, ·) streng extensional ist. Seien a, b ∈ P gegeben mit (∀x ∈ P) a·x ⌢ b·x. Es ist zu zeigen: a ⌢ b. Da P ein bc-Bereich ist, existiert sup{a · x, b · x} für alle x ∈ P . Die Funktion f: x ↦ sup{a·x, b·x} ist monoton und eine obere Schranke für e(a) := (x ↦ a·x) und e(b) := (x ↦ b · x). Nach Voraussetzung ist e ⊣ p, also id_{P} ≤ p ∘ e. Wie auch im Beweis des vorherigen Satzes folgen aus e(a), e(b) ≤ f und der Monotonie von p die Ungleichungen a ≤ p(e(a)) ≤ p(f) und b ≤ p(e(b)) ≤ p(f), somit ist a ⌢ b.

3 Einige Grundbegriffe der Kategorientheorie

Dieses Kapitel stellt jene Begriffe der Kategorientheorie bereit, die im Kapitel 4 für eine Kategorie von Reduktionsmodellen verwendet werden. Eine ausführliche Behandlung des Stoffes kann in [Mac71] nachgelesen werden.

DEFINITION 3.1 Eine Kategorie C ist gegeben durch

• eine Klasse Ob(C), deren Elemente ‘Objekte’ genannt werden,

• für jedes Paar (A, B) von Objekten eine Menge C(A, B), die ‘Hom-Set von A nach B’ genannt wird und deren Elemente ‘Morphismen von A nach B’ genannt werden; für verschiedene Paare sind diese Hom-Sets disjunkt,

• für jedes Tripel (A, B, C) von Objekten eine assoziative Operation ∘: C(B, C) × C(A, B) → C(A, C), genannt ‘Komposition von Morphismen’; da verschiedene Hom-Sets disjunkt sind, ist bei jeder tatsächlichen Anwendung der Operation ∘ auf zwei Morphismen klar, um welche Operation es sich bei dieser Anwendung handelt,

• für jedes Objekt A einen ‘identischen Morphismus’ id_{A} ∈ C(A, A) mit den Eigenschaften (∀C ∈ Ob(C))(∀f ∈ C(C, A)) id_{A} ∘ f = f und (∀B ∈ Ob(C))(∀g ∈ C(A, B)) g ∘ id_{A} = g.

Zu einer Kategorie C definiert man die duale Kategorie oder auch ‘opposite category’ C^{op} durch Ob(C^{op}) := Ob(C) und C^{op}(A, B) := C(B, A) für je zwei Objekte A, B. Man erhält C^{op} aus C, indem man die Morphismen ”herumdreht“. Demnach ist für Objekte A, B, C aus C^{op} die Funktion ∘^{op} eine Abbildung von C(C, B) × C(B, A) nach C(C, A).

Bezeichnung Objekte werden im allgemeinen mit Großbuchstaben, Morphismen mit Kleinbuchstaben bezeichnet. Da die Klasse aller Mengen als Objektklasse und alle Abbildungen zwischen den Mengen als Morphismen mit der Hintereinanderausführung als Komposition den Erfordernissen einer Kategorie nachkommen, schreibt man allgemein statt f ∈ C(A, B) auch f: A → B oder

A ⟶^{f} B.

Sind f, g, h und k Morphismen einer Kategorie, so schreibt man statt der Gleichung k ∘h = g ∘ f oft

[figure: •; f; •; •; h; k; •; g; •; •; f; •; •; ∃!h; •; h; g; •; h] ‖

und sagt, daß ”das Diagram kommutiert“. Die Punkte in obigen Diagrammen sind lediglich Platzhalter für konkrete Objekte. Möchte man über eines der Objekte oder einen der Morphismen quantifizieren, so schreibt man ∀ bzw. ∃ vor den Bezeichner im Diagramm. Der Allquantor ist dabei vor dem Existenzquantor zu lesen, weshalb ein Morphismus, über den ”existenzquantifiziert“ wird, gestrichelt gezeichnet wird. Taucht ein quantifizierter Morphismus noch an anderer Stelle im Diagramm auf, so heißt das, daß die Gleichung des zugehörigen Teildiagramms erst nach dem Quantor zu lesen ist.

DEFINITION 3.2 Ein Morphismus f ∈ C(A, B) heißt Isomorphismus von A nach B, falls es einen Morphismus f^{−1} ∈ C(B, A) gibt derart, daß die beiden Diagramme kommutieren:

[figure: A; f; B; B; f^{−1}; A]
[figure: id_{A}; id_{B}]
[figure: A; f^{−1}; B; f]

Dann wird f^{−1} die Inverse von f genannt.

Beispiele für Kategorien sind die Kategorie SET der Mengen und Funktionen, die Kategorie VEC der Vektorräume und linearen Abbildungen, die Kategorie Ab der abelschen Gruppen und Gruppenhomomorphismen, die Kategorie TOP der topologischen Räume und stetigen Abbildungen, die Kategorie POSET der geordneten Mengen und monotonen Abbildungen. Betrachtet man die Punkte einer geordneten Menge P als Objekte, und legt man für je zwei Punkte x, y fest, daß das Hom-Set P(x, y) genau dann ein Element (und auch nur dieses eine) enthält, wenn x ≤ y gilt, so erhält man eine Kategorie, in der die Morphismen keine Abbildungen sind.

In SET läßt sich das kartesische Produkt A × B := {(a, b)|a ∈ A, b ∈ B} von Mengen A und B bilden. Es hat die Eigenschaft, daß es Projektionen p_{A}: A × B → A, (a, b) ↦ a und p_{B}: A × B → B, (a, b) ↦ b gibt, so daß das folgende Diagramm kommutiert:

[figure: ∀C; ∀f; ∀g; A; p_{A}; A × B; ∃!h; p_{B}; B]  (10)

Die durch f, g eindeutig bestimmte Funktion h ist gegeben durch h(x) := (f(x), g(x)). Sind A und B geordnete Mengen, so läßt sich auf A × B eine Ordnung komponentenweise definieren durch (a, b) ≤ (a′, b′) :⇔ (a ≤ a′ und b ≤ b′). Die Projektionen p_{A} und p_{B} sind monotone Abbildungen von A × B nach A bzw. B. Für jede geordnete Menge C und für alle monotonen Abbildungen f: C → A, g: C → B ist auch die oben angegebene Funktion h: C → A × B monoton. Deshalb heißt A × B auch ‘Produkt der geordneten Mengen A und B’. Für eine beliebige Kategorie C definiert man:

DEFINITION 3.3 Sind A, B ∈ Ob(C), so heißt ein Objekt A × B zusammen mit Morphismen p_{A}: A×B → A, p_{B}: A×B → B das Produkt von A und B, falls die Eigenschaft (10) gilt. Die Abbildungen p_{A} und p_{B} nennt man Projektionen. Sind desweiteren Morphismen a: A → A′, b: B → B′ gegeben, und werden mit p_{A′}: A′ ×B′ → A′, p_{B′}: A′ ×B′ → B′ die zugehörigen Projektionen bezeichnet, dann kommutiert das Diagramm:

[figure: A; p_{A}; A × B; p_{B}; B; A′; a; p_{A′}; A′ × B′; ∃!h; p_{B′}; B′; b]

Der eindeutige Morphismus h wird mit a × b bezeichnet. Im übrigen sei bemerkt, daß für je zwei Objekte A und B alle Produkte isomorph sind. Es ist also gerechtfertigt, von dem Produkt A × B zu sprechen.

Betrachtet man für Mengen A und B den Funktionenraum B^{A} := {f: A → B}, so gibt es eine ‘Auswertungsabbildung’ ϵ: B^{A} × A → B, (f, x) ↦ f(x), und es kommutiert

[figure: B^{A}; B^{A} × A; ϵ; B; ∀g; ∀C; ∃!h; C × A; h × id_{A}]  (11)

Die durch g eindeutig bestimmte Funktion h ist gegeben durch h(x) := (g̃: A → B, y ↦ g(x, y)). Sind A und B wieder geordnete Mengen, so wird B^{A} durch die punktweise gegebene Ordnung f ≤ f′ :⇔ (∀x ∈ A) f(x) ≤ f′(x) zu einer geordneten Menge. Die Auswertungsabbildung ϵ ist monoton. Ist auch C geordnet und g: C × A → B monoton, so ist die oben angegebene Funktion h ebenfalls monoton. Für eine beliebige Kategorie C mit einem Produkt × definiert man:

DEFINITION 3.4 Sind A, B ∈ Ob(C), so heißt ein Objekt B^{A} zusammen mit einem Morphismus ϵ: B^{A} × A → B das Exponential von A nach B, falls (11) gilt. Die Abbildung ϵ nennt man den Auswertungsmorphismus. Sind desweiteren Morphismen a: A′ → A, b: B → B′ gegeben, und wird mit ϵ′ der zu (B′)^{A′} gehörende Auswertungsmorphismus bezeichnet, so kommutieren die Diagramme:

[figure: A′; B^{A} × A′; \overbrace{b∘ϵ∘(id_{B^{A}}×a)}^{g:=}; B′; A; a; B^{A} × A; id_{B^{A}} × a; ϵ; B; b; (B′)^{A′}; (B′)^{A′} × A′; ϵ′; B′; g; B^{A}; ∃!h; B^{A} × A′; h × id_{A′}]

Der eindeutige Morphismus h wird mit b^{a} bezeichnet. Wie schon entsprechend für Produkte bemerkt wurde, sind für je zwei Objekte A und B alle Exponentiale von A nach B isomorph; man kann also auch von dem Exponential B^{A} sprechen.

Nachdem bisher nur Strukturen innerhalb einer Kategorie untersucht wurden, werden im folgenden Strukturen zwischen Kategorien betrachtet.

DEFINITION 3.5 Ein Funktor F von der Kategorie C in die Kategorie D ist eine Zuordnungsvorschrift F: C → D, die jedem Objekt A ∈ Ob(C) ein Objekt F (A) ∈ Ob(D) und jedem Morphismus f ∈ C(A, B) einen Morphismus F (f) ∈ D(F (A), F (B)) zuordnet. Es wird gefordert, daß F die identischen Morphismen erhält, d.h. für alle A ∈ Ob(C) gilt: F (id_{A}) = id_{F (A)}. Desweiteren wird verlangt, daß F sich mit der Komposition von Morphismen verträgt, d.h. für alle A, B, C ∈ Ob(C), für alle f ∈ C(A, B), g ∈ C(B, C) gilt: F (g ∘ f) = F (g) ∘ F (f). Sind C und D Kategorien, so wird ein Funktor F von C^{op} nach D kontravarianter Funktor von C nach D genannt. Definiert man das Produkt von Kategorien durch:

Ob(C × D) := Klasse aller Paare von Elementen, wobei das erste Element aus Ob(C) ist

und das zweite Element aus Ob(D) ist

(C × D)((A, A′),(B, B′)) := C(A, B) × D(A′, B′)

so wird ein Funktor von der Kategorie C × D in eine Kategorie B auch Bifunktor genannt. Man überlegt sich leicht, daß ein Bifunktor in jeder Komponente ein Funktor ist. D.h. ist F: C × D → B, so sind für alle A, B, C ∈ Ob(C), A′, B′, D ∈ Ob(D), f ∈ C(A, B), g ∈ D(A′, B′) zwei Funktoren gegeben durch gegeben:

F_{1} : C → B  F_{2} :D → B
F_{1}(X) := F (X, D)  F_{2}(X) := F (C, X)
F_{1}(h) := F (h, g)  F_{2}(h) := F (f, h)

Auch für Funktoren läßt sich ein Produkt definieren. Sind F: C → D, G: C’ → D’ Funktoren, so ist der Funktor F × G: C × C’ → D × D’ gegeben durch (F × G)(A, B) := (F (A), G(B)), (F × G)(f, g) := (F (f), G(g)). Die Komposition G ∘ F von Funktoren F: B → C, G: C → D ist durch die Hintereinanderausführung von Funktionen gegeben.

Funktoren sind also die ‘strukturerhaltenden Abbildungen’ zwischen Kategorien, genau so, wie es z.B. die Homomorphismen für allgemeine Algebren sind. In diesem Sinne kann man Kategorien selbst als Objekte einer (”größeren“) Kategorie auffassen, deren Morphismen Funktoren zwischen den Objekt-Kategorien sind. Als Beispiel für einen Funktor betrachten wir den ”Vergißfunktor“ U: Ab → SET, der jeder abelschen Gruppe die ihr zugrundeliegende Menge zuordnet und jeden Gruppenhomomorphismus lediglich als Abbildung zwischen Mengen definiert. Bifunktoren, die wir in Kapitel 4 noch benutzen werden, sind der ”Produkt“-Funktor und der ”Exponential“-Funktor. Sind B, C und D Kategorien, dann ist ersterer gegeben durch F: C × D → B, F (A, B) := A × B, F (f, g) := f × g. Der zweite wird definiert durch F : C × D → B, F (A, B) := B^{A}, F (f, g) := g^{f} und ist kontravariant im ersten Argument. Ebenfalls im Kapitel 4 wird der Begriff der monoidalen Kategorie benutzt. Um diesen zu definieren, benötigt man die

DEFINITION 3.6 Seien F, G: C → D Funktoren. Eine natürliche Transformation η: F ⟶^{·} G besteht aus einer Familie von Morphismen η = (η_{A})_{A∈Ob(C)}, η_{A}: F A → GA, so daß das folgende Diagramm kommutiert:

C  [figure: F; G]  D
∀A  F A \overline{η_{A}} GA

[figure: ∀B; ∀f; F B; F f; η_{B}; GB; Gf]

Eine natürliche Transformation η: F ⟶^{·} G heißt natürlicher Isomorphismus (von F nach G), falls für jedes A ∈ Ob(C) der Morphismus η_{A}: F A → GA ist ein Isomorphismus ist.

Bemerkung 3.7 (i) Sind F, G: C × D → B Bifunktoren, und ist eine Familie η = (η_{(A,B)})_{(A,B)∈Ob(C×D)}, η_{(A,B)} : F (A, B) → G(A, B), gegeben, so ist η genau dann eine natürliche Transformation von F nach G, falls sie es für die Funktoren F_{1}, G_{1} : C → B und F_{2}, G_{2} : D → B ist, die man erhält, wenn man F und G jeweils in einer Komponente festhält. Vergleiche mit den Funktoren in Definition 3.5. Für den Nachweis der Natürlichkeit von η reicht es also, die Natürlichkeit von η ‘in A’ und ‘in B’ nachzuweisen.

(ii) Gibt man sich eine Klasse von Funktoren als Objektklasse vor und betrachtet alle natürlichen Transformationen zwischen zwei Funktoren als deren Hom-Set, so erhält man mit der Verknüpfung (ϵ: G ⟶^{·} H) ∘ (η: F ⟶^{·} G) := (ϵ_{A} ∘ η_{A})_{A Objekt} von natürlichen Transformationen erneut eine Kategorie, genannt die ”Funktorkategorie“. Tatsächlich handelt es sich aber nicht mehr um eine Kategorie im Sinne von Definition 3.1, da nicht garantiert ist, daß diese Hom-Sets Mengen sind. Auf den Begriff von ”größeren“ Kategorien wird hier jedoch nicht weiter eingegangen.

Kategorien, die keine Produkte haben, können zumindest daraufhin untersucht werden, ob sie eine Art ”Tensorprodukt“ haben, wie z.B. das Tensorprodukt abelscher Gruppen. Gesucht ist daher eine binäre ”Verknüpfung“, die ”assoziativ“ ist und ein 1-”Element“ hat, welches links- und rechts-”neutral“ ist: in der Kategorie Ab ist dies die Gruppe ℤ der ganzen Zahlen. Die genannten Eigenschaften gelten in Ab aber nur ”bis auf Isomorphie“. Allgemeiner definiert man

DEFINITION 3.8 Eine monoidale Kategorie C ist gegeben durch

• eine Kategorie C,

• einen Bifunktor ⊗: C × C → C,

• einen natürlichen Isomorphismus

α: ⊗ ∘ (id_{C} × ⊗) ⟶^{·} ⊗ ∘ (⊗ × id_{C})
α_{A,B,C}: A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C,

• ein ausgezeichnetes Objekt 1 ∈ Ob(C),

• natürliche Isomorphismen

λ: ⊗ ∘ (1 × id_{C}) ⟶^{·} id_{C}  σ: ⊗ ∘ (id_{C} × 1) ⟶^{·} id_{C}
λ_{A}: 1 ⊗ A → A  σ_{A}: A ⊗ 1 → A .

(Hierbei sei mit 1 der Funktor 1: {⋆} → C von der Kategorie mit nur einem Objekt und dem identischen Morphismus darauf nach C bezeichnet, der das Objekt 1 ∈ Ob(C) ”auswählt“.)

Außerdem wird verlangt, daß alle Diagramme, die sich mit Hilfe der Funktoren ⊗, id_{C} und 1 und den natürlichen Transformationen α, λ, σ, id = id_{A}: A → A und id_{1} : 1 ⟶^{·} 1 (triviale Transformation, zugehöriges Diagramm ist id_{1} ∘id_{1} = id_{1} ∘id_{1}) konstruieren lassen, kommutieren. Eine monoidale Kategorie C heißt symmetrisch, falls es für den Bifunktor S: C × C → C × C, S(A, B) := (B, A), S(f, g) := (g, f) einen natürlichen Isomorphismus

γ: ⊗ ∘(id_{C} × id_{C}) → ⊗ ∘ S ∘ (id_{C} × id_{C})
γ_{A,B}: A × B → B × A

gibt, so daß alle Diagramme, die sich mit den oben genannten Funktoren und dem Funktor S konstruieren lassen, kommutieren.

Die Bedingung aus Definition 3.8, daß ”alle“ Diagramme kommutieren, ist erfüllt, falls für alle A, B, C, D ∈ Ob(C) folgende Diagramme kommutieren:

[figure: A ⊗ (B ⊗ (C ⊗ D)); α; (A ⊗ B) ⊗ (C ⊗ D); α; ((A ⊗ B) ⊗ C) ⊗ D; A ⊗ ((B ⊗ C) ⊗ D); id ⊗ α; α; (A ⊗ (B ⊗ C)) ⊗ D; α ⊗ id]

[figure: A ⊗ (1 ⊗ B); α; (A ⊗ 1) ⊗ B; A ⊗ B; id ⊗ λ; =; A ⊗ B; σ ⊗ id; 1 ⊗ 1; λ; σ; 1]

[figure: B ⊗ A; γ; A ⊗ B; A ⊗ 1; γ; 1 ⊗ A]
[figure: id; σ]
[figure: B ⊗ A; γ; A; λ]

[figure: A ⊗ (B ⊗ C); α; (A ⊗ B) ⊗ C; γ; C ⊗ (A ⊗ B); A ⊗ (C ⊗ B); id ⊗ γ; α; (A ⊗ C) ⊗ B; γ ⊗ id; (C ⊗ A) ⊗ B; α]

In den Diagrammen wurden die offensichtlichen Indizes an den natürlichen Transformationen weggelassen. Ein Beweis dafür, daß die Kommutativität dieser Diagramme hinreichend für die Kommutativität aller Diagramme, kann in [Mac71, S.161-166] nachgelesen werden.

4 Eine Kategorie von Reduktionsmodellen

In diesem Kapitel wird eine Kategorie von Reduktionsmodellen vorgestellt. Die Objekte der Kategorie sind spezielle Reduktionsmodelle. Die Morphismen sind Einbettungs-Projektions-Paare zwischen den den Reduktionsmodellen zugrundeliegenden geordneten Mengen. Zusätzlich erfüllen die Morphismen eine Bedingung, die die Verträglichkeit mit der Struktur der Reduktionsmodelle sicherstellt. Gezeigt wird desweiteren, daß bei der Interpretation der Menge der λ-Terme in Modellen D und E jeder Morphismus von D nach E die Denotationen der Terme in D unter die Denotationen der Terme in E einbettet, sofern dies schon für die Variablen erfüllt ist. Abschließend werden einige Konstruktionen angegeben, wie man aus gegebenen Modellen neue konstruieren kann.

DEFINITION 4.1 Wir definieren folgendermaßen die Kategorie RED: Ein Objekt ist ein kategorielles Reduktionsmodell mit der Eigenschaft, daß statt nur einer Adjunktion zwischen einer geordneten Menge D und ihrem Funktionenraum D^{D} sogar ein monotones Einbettungs-Projektions-Paar d: D → D^{D}, d^{∗}: D^{D} → D gefordert wird. Wenn nichts weiter erwähnt wird, so wollen wir diese Modelle mit Großbuchstaben, z.B. D, die Einbettung mit dem zugehörigen Kleinbuchstaben, also d: D → D^{D}, und die (durch die Einbettung eindeutig festgelegte) Projektion mit einem ^{∗} an dem Namen der Einbettung, also d^{∗}: D^{D} → D, bezeichnen. Ein Reduktionsmodell (D, d, d^{∗}) wird auch oft abkürzend mit D bezeichnet. Ein Morphismus zwischen Modellen (D, d, d^{∗}) und (E, e, e^{∗}) ist ein Einbettungs-Projektions-Paar (f, f^{∗}), f: D → E, f^{∗}: E → D, derart, daß das folgende Diagramm kommutiert:

D  \overline{d} D^{D}
(K1)
[figure: E; f; e; E^{E}; f^{f^{∗}}]

Dabei ist f^{f^{∗}} := f ∘ ∘ f^{∗}. Wir schreiben dann (f, f^{∗}): (D, d, d^{∗}) → (E, e, e^{∗}) oder auch (etwas verwirrend) (f, f^{∗}): D → E. Mit RED(D, E) bezeichnen wir wie üblich die Menge der Morphismen von einem Reduktionsmodell D zu einem Reduktionsmodell E in der Kategorie RED.

Lemma 4.2 Jedes Modell (D, d, d^{∗}) dieser Kategorie modelliert die βη-Reduktion.

Beweis: Für das Einbettung-Projektions-Paar (d, d^{∗}) gilt: d^{∗} ∘ d = id_{D}. Es ist die Eigenschaft 1.6(6) nachzuweisen. Sei x ∉ F V (M). Dann ist für jedes ρ gegeben: ⟦λx.Mx⟧_{ρ} =^{def}

d^{∗}(a ↦ ⟦Mx⟧_{ρ(x↦a)}) =^{x∉F V (M)} d^{∗}(a ↦ ⟦M⟧_{ρ} · ⟦x⟧_{ρ(x↦a)}) = d^{∗}(a ↦ ⟦M⟧_{ρ} · a) =

d^{∗}(d(⟦M⟧_{ρ})) =^{Vor.} ⟦M⟧_{ρ}.

Bemerkung 4.3 Da sich Einbettung und Projektion gegenseitig eindeutig bestimmen, folgt aus der Gleichheit zweier Einbettungen schon die Gleichheit der zugehörigen Projektionen und umgekehrt.

Der nächste Satz weist einige Eigenschaften von Morphismen in RED nach.

Hilfssatz 4.4 Seien D, E ∈ Ob(RED) und (f, f^{∗}) ∈ RED(D, E). Dann erfüllt das Paar (f, f^{∗}) die folgenden Eigenschaften:

(a) f^{f^{∗}} und (f^{∗})^{f} bilden ein Einbettungs-Projektions-Paar von D^{D} nach E^{E}.

(b) Falls f ein Isomorphismus in POSET mit der Inversen f^{∗} ist, dann ist (f, f^{∗}): D → E schon ein Isomorphismus in RED mit der Inversen (f^{∗}, f): E → D.

(c)

D ^{d∗} D^{D}
(K2)  kommutiert
[figure: E; f^{∗}; e^{∗}; E^{E}; (f^{∗})^{f}]
D × D \overline{u} D
(K3)  kommutiert
[figure: E × E; f × f; v; E; f]
D × D \overline{u} D
(K4)  ≤  d.h. u ∘ (f^{∗} × f^{∗}) ≤ f^{∗} ∘ v
[figure: E × E; f^{∗} × f^{∗}; v; E; f^{∗}]

Dabei sei u := uncurry(d), d.h. u(x, y) = d(x)(y), v := uncurry(e), d.h. v(a, b) =

e(a)(b).

Beweis: zu (a): Es ist nachzuweisen:

(i) ((f^{∗})^{f}) ∘ (f^{f^{∗}}) = id_{D^{D}}
(ii) (f^{f^{∗}}) ∘ ((f^{∗})^{f}) ≤ id_{E^{E}}

zu (i): Sei h ∈ D^{D}. Dann ist

[((f^{∗})^{f}) ∘ (f^{f^{∗}})](h)
= ((f^{∗})f)(f ∘ h ∘ f^{∗})
= \underbrace{f^{∗} ∘ f}_{=id_{D}} ∘ h ∘ \underbrace{f^{∗} ∘ f}_{=id_{D}} = h

zu (ii): Sei k ∈ E^{E}. Dann ist

[(f^{f^{∗}}) ∘ ((f^{∗})^{f})](k)
=  (f^{f^{∗}})(f^{∗} ∘ k ∘ f)
= \underbrace{f ∘ f^{∗}}_{≤id_{E}} ∘ k ∘ \underbrace{f ∘ f^{∗}}_{≤id_{E}} ≤ k

zu (b): Ein Morphismus (g, g^{∗}): E → D ist die Inverse von (f, f^{∗}): D → E in RED, falls

gilt: (g, g^{∗}) ∘ (f, f^{∗}) =^{def} (g ∘ f, f^{∗} ∘ g^{∗}) =^{!} (id_{D}, id_{D}) und

(f, f^{∗}) ∘ (g, g^{∗}) =^{def} (F ∘ g, g^{∗} ∘ f^{∗}) =^{!} (id_{E}, id_{E})

(Beachte, daß die Einbettung id_{D} und die Projektion id_{D} den identischen Morphismus auf D bilden.) Nach Voraussetzung ist f ein Iso in POSET mit der Inversen f^{∗}, also f^{∗} ∘ f = id_{D} und f ∘ f^{∗} = id_{E}. Folglich ist (f^{∗}, f) ein Einbettungs-Projektions-Paar, d.h. (f^{∗})^{∗} = f. Ist (f^{∗}, f) außerdem ein Morphismus der Kategorie RED, d.h. erfüllt (K1), dann erfüllt (f^{∗}, f) die obige Bedingung für die Inverse von (f, f^{∗}) und (f, f^{∗}) ist ein Iso in RED. Es bleibt zu zeigen: (f^{∗}, f) erfüllt

[figure: E; e; E^{E}; D; f^{∗}; d; D^{D}; (f^{∗})^{f}]

Da (f, f^{∗}) die Eigenschaft (K1) erfüllt, gilt (∀x ∈ D)e(f(x)) = f ∘ d(x) ∘ f^{∗}. Wählt man a ∈ E und setzt x = f^{∗}(a), so erhält man

(∀a ∈ E) e(a) = e(\underbrace{f(f^{∗}}_{=id_{E}}(a))) = f ∘ d(f^{∗}(a)) ∘ f^{∗}

Somit ist für alle a ∈ E

f^{∗} ∘ e(a) ∘ f
= \underbrace{f^{∗} ∘ f}_{=id_{D}} ∘ d(f^{∗}(a)) ∘ \underbrace{f^{∗} ∘ f}_{=id_{D}}
=  d(f^{∗}(a))

d.h (f^{∗})^{f} ∘ e = d ∘ f^{∗} und obiges Diagramm kommutiert. zu (c): Nach Teil (a) ist die Projektion zu f^{f^{∗}} gegeben durch (f^{∗})^{f}. Die Hintereinander-

ausführung von Einbettungen bzw. Projektionen ergibt eine Einbettung bzw. eine Projektion. Mit Bemerkung 4.3 kommutiert also (K2) genau dann, wenn (K1) kommutiert. (K3) ist gezeigt, falls gilt:

(∀x, y ∈ D × D) f(u(x, y)) = v(f(x), f(y))

Nach der Definition von u und v bleibt zu zeigen:

(∀x, y ∈ D × D) f(d(x)(y)) = e(f(x))(f(y))

(f, f^{∗}) erfüllt (K1), also gilt

(∀x ∈ D) f ∘ d(x) ∘ f^{∗} = e(f(x)) ∈ E^{E}

Also ist

(∀x ∈ D)(∀a ∈ E) f(d(x)[f^{∗}(a)]) = e(f(x))(a)

Wählt man y ∈ D und setzt a := f(y), so erhält man

(∀x, y ∈ D) f(d(x)(y)) = f(d(x)[\underbrace{f^{∗}(f}_{=id_{D}}(y))]) = e(f(x))(f(y))

Somit ist (K3) gezeigt. Für (K4) ist zu zeigen:

(∀a, b ∈ E) u(f^{∗}(a), f^{∗}(b)) ≤ f^{∗}(v(a, b))

Nach der Definition von u und v bleibt zu zeigen:

(∀a, b ∈ E) d(f^{∗}(a))(f^{∗}(b)) ≤ f^{∗}(e(a)(b))

Wir benutzen wieder, daß (f, f^{∗}) die Eigenschaft (K1) erfüllt, d.h.

(∀x ∈ D)(∀b ∈ E) f[d(x)(f^{∗}(b))] = e[f(x)](b)

Wählt man a ∈ E und setzt man x := f^{∗}(a), so erhält man

(∀a, b ∈ E) f[d(f^{∗}(a))(f^{∗}(b))] = e[\underbrace{f(f^{∗}}_{≤id_{E}}(a))](b) ≤ e(a)(b)

Wendet man die monotone Funktion f^{∗} auf beide Seiten der Gleichung an, so ergibt sich

(∀a, b ∈ E) \underbrace{f^{∗}(f}_{=id_{D}}[d(f^{∗}(a))(f^{∗}(b))] ≤ f^{∗}(e(a)(b))

also (∀a, b ∈ E) d(f^{∗}(a))(f^{∗}(b)) ≤ f^{∗}(e(a)(b))

Um zu zeigen, daß für gewisse a, b ∈ E der Ausdruck d(f^{∗}(a))(f^{∗}(b)) echt kleiner als f^{∗}(e(a)(b)) werden kann, betrachte man das folgende Beispiel: Seien zwei Reduktionsmodelle D und E gegeben durch:

D = {⊥, a} ⊥≤ a ; E = {⊥, a, b} ⊥≤ a, b

D  a •  D^{D}  ^{aaa •}
[figure: ⊥ •; ⊥⊥ •; ^{⊥a •}]

aaa •  • bbb
E  E^{E}  • ⊥ab  • ⊥ba
[figure: a •; • b; ⊥a⊥ •; ^{⊥aa •}; ⊥⊥a •; ⊥⊥b •; • ⊥b⊥; ^{• ⊥bb}]
[figure: ⊥ •] ⊥⊥⊥ •

Eine Funktion h ∈ D^{D} ist durch die Angabe von h(⊥), h(a) festgelegt, eine Funktion k ∈ E^{E} durch die Angabe von k(⊥), k(a), k(b). Die Funktionswerte, in dieser Reihenfolge notiert, bezeichnen in diesem Beispiel die Funktion h bzw. k. Die zu den Reduktionsmodellen zugehörigen Einbettungen seien nun gegeben durch

d: D → D^{D}  e: E → E^{E}
d(⊥) =⊥⊥  e(⊥) =⊥⊥⊥
d(a) =⊥ a  e(a) =⊥⊥ a
e(b) =⊥⊥ b

Man erhält die zugehörigen Projektionen durch:

d^{∗}: D^{D} → D  e^{∗}: E^{E} → E
h ↦ \begin{cases}a, & falls h(a) = a \\ ⊥, & sonst \end{cases}  k ↦ \begin{cases}a, & falls k(b) = a \\ b, & falls k(b) = b \\ ⊥, & sonst \end{cases}

Anhand der Ordnungsdiagramme sieht man leicht, daß (d, d^{∗}) und (e, e^{∗}) monotone Einbettungs-Projektions-Paare sind. Bettet man außerdem D in E ein durch

f: D → E  f^{∗}: E → D
f(⊥) = a  f^{∗}(⊥) = f^{∗}(b) =⊥
f(a) = a  f^{∗}(a) = a

so erhält man die echte Kleinerrelation

d(f^{∗}(a))(f^{∗}(b)) = d(a)(⊥) = (⊥ a)(⊥) =⊥
< a = f^{∗}(a) = f^{∗}[(⊥⊥ a)(b)] = f^{∗}[e(a)(b)]

Der folgende Abschnitt gibt Auskunft darüber, was eine gute Interpretation der λ-Terme sein soll. Sind Modelle D, E ∈ Ob(RED) und ein Morphismus (f, f^{∗}) ∈ RED(D, E) gegeben, so bettet f die geordnete Menge D in die geordnete Menge E ein. Eine Interpretation der λ-Terme in einem Reduktionsmodell, wie sie in Kapitel 1 definiert wird, kann man bzgl. des gegebenen Modells ”gut“ nennen, wenn die Terme durch in der Ordnung große Werte interpretiert werden. Siehe dazu auch die Forderung im Kapitel 2, die Abstraktion λx.P durch den größtmöglichen Wert zu interpretieren, so daß die Interpretation noch korrekt ist. Betrachtet man die Interpretation in den im letzten Absatz gegebenen Modellen D und E, so ist es wünschenswert, daß die Interpretation in E besser ist als die in D. Die Interpretationen in den verschiedenen Modellen sind allerdings nur über die Einbettung f vergleichbar. Gezeigt wird also der

SATZ 4.5 Seien D, E ∈ Ob(RED) und (f, f^{∗}) ∈ RED(D, E). Seien Belegungen ρ_{D}: V → D, ρ_{E}: V → E gegeben derart, daß (∀x ∈ V) f(ρ_{D}(x)) ≤ ρ_{E}(x). Dann gilt: (∀M)f(⟦M⟧_{ρ_{D}}) ≤ ⟦M⟧_{ρ_{E}}.

Beweis: Der Beweis wird induktiv über den Aufbau von M geführt.

M ≡ y : Seien Belegungen ρ_{D}, ρ_{E} gegeben mit (∀x)f(ρ_{D}(x)) ≤ ρ_{E}(x). Nach 1.6(1) ist für alle x erfüllt: ⟦x⟧_{ρ_{D}} = ρ_{D}(x), ⟦x⟧_{ρ_{E}} = ρ_{E}(x). Offensichtlich ist also f(⟦y⟧_{ρ_{D}}) ≤ ⟦y⟧_{ρ_{E}}.

M ≡ P Q : Seien Belegungen ρ_{D}, ρ_{E} gegeben mit (∀x)f(ρ_{D}(x)) ≤ ρ_{E}(x). Zu zeigen ist:

f(⟦P Q⟧_{ρ_{D}}) ≤ ⟦P Q⟧_{ρ_{E}}

Man erinnere sich daran, daß Reduktionsmodelle mit einer Applikation ausgestattet sind. Es gilt für alle r, s ∈ D: f(r · s) =^{Def. d} f(d(r)(s)) =^{Def. u} f(u(r, s)) =^{(K3)}

v(f(r), f(s)) =^{Def. v} e(f(r))(s) =^{Def. e} f(r) · f(s).

Für den Term PQ gilt deshalb: f(⟦P Q⟧_{ρ_{D}}) =^{1.6(2)} f(⟦P ⟧_{ρ_{D}} · ⟦Q⟧_{ρ_{D}}) = f(⟦P ⟧_{ρ_{D}}) ·

f(⟦Q⟧_{ρ_{D}}) ≤ ⟦P ⟧_{ρ_{E}} · ⟦Q⟧_{ρ_{E}}. Für den Nachweis der letzten Ungleichung wurde die Induktionsvoraussetzung für P und Q angewandt und die Monotonie der Applikation · in beiden Argumenten ausgenutzt.

M ≡ λy.P : Seien Belegungen ρ_{D}, ρ_{E} gegeben mit (∀x)f(ρ_{D}(x)) ≤ ρ_{E}(x). Zu zeigen ist

f(⟦λy.P ⟧_{ρ_{D}}) ≤ ⟦λy.P ⟧_{ρ_{E}}

Die Interpretation eines abstrahierten Terms ist (in kategoriellen Modellen) mit Hilfe der Projektion des Funktionenraums in die geordnete Menge des Modells definiert. Mit Satz 2.1 bleibt also zu zeigen:

\begin{aligned}f[d^{∗}(r & ↦ & ⟦P ⟧_{ρ_{D}(y↦r)})] & ≤ & e^{∗}(a & ↦ & ⟦P ⟧_{ρ_{E}(y↦a)}) \\ D & → & D & & E & → & E \end{aligned}

Die Induktionsvoraussetzung für P besagt: für alle Belegungen ρ_{D}: V → D, ρ_{E}: V → E gilt:

((∀x) f(ρ_{D}(x)) ≤ ρ_{E}(x)) ⇒ (f(⟦P ⟧_{ρ_{D}}) ≤ ⟦P ⟧_{ρ_{E}})

Um die gewünschte Ungleichung zu zeigen, ist es hilfreich, eine obere Schranke für f zu berechnen. Da f^{∗} ∘ f = id_{D} und e^{∗} ∘ e = id_{E}, gilt auch f^{∗} ∘ e^{∗} ∘ e ∘ f = id_{D}. Desweiteren erfüllt (f, f^{∗}) die Eigenschaft (K1), d.h. e ∘ f = (f^{f^{∗}}) ∘ d. Verknüpft man beide Seiten von links mit f ∘ f^{∗} ∘ e^{∗}, so ergibt sich

f ∘ \underbrace{f^{∗} ∘ e^{∗} ∘ e ∘ f}_{=id_{D}} = \underbrace{f ∘ f^{∗}}_{≤id_{E}} ∘ e^{∗} ∘ (f^{f^{∗}}) ∘ d,  also
f ≤ e^{∗} ∘ (f^{f^{∗}}) ∘ d,  d.h.
(∀s ∈ D) f(s) ≤ e^{∗}(f ∘ d(s) ∘ f^{∗})

Wählt man s = d^{∗}(\underbrace{r ↦ ⟦P ⟧_{ρ_{D}(y↦r)}}_{D→D}), dann ist

f[d^{∗}(r ↦ ⟦P ⟧_{ρ_{D}(y↦r)})] ≤ e^{∗}[f ∘ \underbrace{d(d^{∗}}_{≤idD^{D}}(r ↦ ⟦P ⟧_{ρ_{D}(y↦r)})) ∘ f^{∗}]
≤  e^{∗}[f ∘ (r ↦ ⟦P ⟧_{ρ_{D}(y↦r)}) ∘ f^{∗}]
=  e^{∗}[(r ↦ f(⟦P ⟧_{ρ_{D}(y↦r)})) ∘ f^{∗}]

Nach Voraussetzung gilt (∀x) f(ρ_{D}(x)) ≤ ρ_{E}(x), also ist auch erfüllt

(∀r ∈ D)(∀x) f(ρ_{D(y↦r)}(x)) ≤ ρ_{E(y↦f(r))}(x)

Die Induktionsvoraussetzung für P besagt, daß für die Belegungen ρ_{D}(y ↦ r), ρ_{E}(y ↦ f(r)) mit r ∈ D, welche die letzte Ungleichung erfüllen, gilt:

(∀r ∈ D) f(⟦P ⟧_{ρ_{D}(y↦r)}) ≤ ⟦P ⟧_{ρ_{E}(y↦f(r))}

4.1 Konstruktion eines Modells auf dem Exponential D^{D} in POSET 33

Wird die Ungleichung ausgenutzt im zuletzt berechneten Ausdruck, so ergibt sich

e^{∗}[(r ↦ f(⟦P ⟧_{ρ_{D}(y↦r)})) ∘ f^{∗}] ≤ e^{∗}[(r ↦ ⟦P ⟧_{ρ_{E}(y↦f(r))}) ∘ f^{∗}]

= \begin{matrix}e^{∗}[(r & ↦ & ⟦P ⟧_{ρ_{E}(y↦f(r))}) & ∘ & (a & ↦ & f^{∗}(a))] \\ D & → & E & & E & → & D \end{matrix}
= e^{∗}[a ↦ ⟦P ⟧_{ρ_{E}(y↦\underbrace{f(f^{∗}}_{≤id_{D}}(a)))}]

≤ e^{∗}(a ↦ ⟦P ⟧_{ρ_{E}(y↦a)})

Insgesamt wurde gezeigt:

f[d^{∗}(r ↦ ⟦_{⟧}ρ_{D}(y ↦ r))] ≤ e^{∗}(a ↦ ⟦_{⟧}ρ_{E}(y ↦ a))

4.1 Konstruktion eines Modells auf dem Exponential D^{D} in POSET

Ist ein Reduktionsmodell (D, d, d^{∗}) gegeben, so läßt sich mit Hilfe von d und d^{∗} die geordnete Menge D^{D} in (D^{D})^{D^{D}} einbetten. Damit wird D^{D} zu einem Reduktionsmodell, erfüllt aber in der Kategorie RED nicht die Aufgabe eines Exponentials.

Lemma 4.6 Sei ein Reduktionsmodell (D, d, d^{∗}) gegeben. Dann läßt sich auf dem Exponential D^{D} in POSET ein Reduktionsmodell definieren. Die Einbettung und die Projektion sind gegeben durch:

h: D^{D} → (D^{D})^{D^{D}}  h^{∗}: (D^{D})^{D^{D}} → D^{D}
h := d^{d^{∗}}  h^{∗} := (d^{∗})^{d}

Beweis: Für alle f ∈ D^{D}, U ∈ (D^{D})^{D^{D}} ist nachzurechnen

(i) h^{∗}(h(f)) = f.

h^{∗}(h(f)) = h^{∗}(d ∘ f ∘ d^{∗}) = \underbrace{d^{∗} ∘ (d}_{=id_{D}} ∘f ∘ \underbrace{d^{∗}) ∘ d}_{=id_{D}} = f

(ii) h(h^{∗}(U)) ≤ U.

h(h^{∗}(U)) = h(d^{∗} ∘ U ∘ d) = \underbrace{d ∘ (d^{∗}}_{≤id_{D^{D}}} ∘U ∘ \underbrace{d) ∘ d^{∗}}_{≤id_{D^{D}}} = U

Das Einbettungs-Projektions-Paar (d, d^{∗}) erfüllt die Eigenschaft (K1), denn nach Definition von h kommutiert trivialerweise

[figure: D; d; D^{D}; D^{D}; d; h; (D^{D})^{D^{D}}; d^{d^{∗}}]

Wir erhalten also

Folgerung 4.7 Jedes Reduktionsmodell (D, d, d^{∗}) läßt sich via (d, d^{∗}) als Morphismus in RED zwischen den Reduktionsmodellen (D, d, d^{∗}) und (D^{D}, h, h^{∗}) auffassen. Dabei seien h und h^{∗} wie in Lemma 4.6 definiert.

Interessant ist die Frage, ob sich die Abbildung D ↦ D^{D}: RED → RED zu einem Funktor ausbauen läßt. Vergißt man die Struktur der Reduktionsmodelle und betrachtet nur die geordneten Mengen und monotonen Abbildungen, so gibt es einen (in der ersten Komponente kontravarianten) Bifunktor F̃: POSET^{op} ×POSET mit F̃[D, E] := E^{D}, F̃[f, g] := g^{f}. Dann ist F̃[f^{∗}, f] = f^{f^{∗}}: D^{D} → E^{E}, F̃[f, f^{∗}] = (f^{∗})^{f}: E^{E} → D^{D}.

\overline{F̃}
D  D  D^{D} D^{D}

[figure: E; f; E; f^{∗}; E^{E}; f^{f^{∗}}; E^{E}; (f^{∗})^{f}]

In Hilfssatz 4.4(a) wurde schon gezeigt, daß (f^{f^{∗}}, (f^{∗})^{f}) ein Einbettungs-Projektions-Paar von D^{D} nach E^{E} ist. Im folgenden Hilfsatz 4.8 wird nachgewiesen, daß (f^{f^{∗}}, (f^{∗})^{f}) die Eigenschaft (K1) hat und folglich ein Morphismus zwischen den Reduktionsmodellen D^{D} und E^{E} ist. Definiert man F (D) := F̃[D, D] = D^{D} und F ((f, f^{∗})) := F̃[f^{∗}, f] = f^{f^{∗}}, so ist F ein Funktor F: RED → RED: F erhält den identischen Morphismus (id_{D}, id_{D}) auf jedem Objekt D, denn F ((id_{D}, id_{D})) = F̃[id_{D}, id_{D}] = (id_{D})^{id^{D}}: D^{D} → D^{D}. Ebenso verträgt sich F mit der Komposition von Morphismen, da F ((f, f^{∗}) ∘ (g, g^{∗})) = F ((f ∘ g, g^{∗} ∘ f^{∗})) =

F̃[g^{∗} ∘ f^{∗}, f ∘ g] =^{F̃ Funktor} F̃[f^{∗}, f] ∘ F̃[g^{∗}, g] = F ((f, f^{∗})) ∘ f((g, g^{∗})).

Hilfssatz 4.8 Sind D und E Reduktionsmodelle und bezeichnen (h, h^{∗}) wie in Lemma 4.6 und (k, k^{∗}) mit k: E^{E} → (E^{E})^{E^{E}}, k := e^{e^{∗}}, k^{∗}: (E^{E})^{E^{E}} → E^{E}, k^{∗} := (e^{∗})^{e} Einbettungs-Projektions-Paare, so erfüllt das Einbettungs-Projektions-Paar (f^{f^{∗}}, (f^{∗})^{f}) die Eigenschaft (K1), d.h. das folgende Diagramm kommutiert:

4.2 Konstruktion eines Modells auf dem Produkt D × E in POSET 35

[figure: D^{D}; h; (D^{D})^{D^{D}}; E^{E}; f^{f^{∗}}; k; (E^{E})^{E^{E}}; (f^{f^{∗}})^{(f^{∗})^{f}}]

Beweis: Für den Beweis wird benutzt, daß (f, f^{∗}) die Eigenschaften (K1) und (K2) erfüllt, d.h.

[figure: D; d; D^{D}; D; d^{∗}; D^{D}; E; f; e; E^{E}; f^{f^{∗}}; E; f^{∗}; e^{∗}; E^{E}; (f^{∗})^{f}]

Sei u ∈ D^{D}.

(k ∘ f^{f^{∗}})(u) =^{Def. k} (e^{e^{∗}} ∘ f^{f^{∗}})(u)

= e ∘ f ∘ u ∘ f^{∗} ∘ e^{∗} =^{(K1)} f^{f^{∗}} ∘ d ∘ u ∘ f^{∗} ∘ e^{∗} =^{(K2)} f^{f^{∗}} ∘ (d ∘ u ∘ d^{∗}) ∘ (f^{∗})^{f}
= (f^{f^{∗}})^{(f^{∗})^{f}} (d ∘ u ∘ d^{∗}) = ((f^{f^{∗}})^{(f^{∗})^{f}} ∘ d^{d^{∗}})(u)
=^{Def. h}((f^{f^{∗}})^{(f^{∗})^{f}} ∘ h)(u)

4.2 Konstruktion eines Modells auf dem Produkt D × E in POSET

In Anlehnung an das vorangegangene Kapitel möchte man auf dem Produkt D × E geordneter Mengen ein Reduktionsmodell definieren, sofern D und E schon Reduktionsmodelle sind. Eine allgemeine Konstruktion ist zumindest dann möglich, wenn man sich auf die volle Unterkategorie RED_{⊥} beschränkt, die aus RED hervorgeht, indem nur Modelle betrachtet werden, deren zugrundeliegende geordnete Menge ein kleinstes Element besitzt.

Lemma 4.9 Seien (D, d, d^{∗}), (E, e, e^{∗}) ∈ Ob(RED_{⊥}). Dann läßt sich auf dem Produkt D × E in POSET ein Reduktionsmodell definieren. Die Einbettung und die Projektion sind gegeben durch:

h: D × E → (D × E)^{D×E}
h(x, a) := d(x) × e(a) := (y, b) ↦ (d(x)(y), e(a)(b))
h^{∗}: (D × E)^{D×E} → D × E
h^{∗}(U) := ( d^{∗}[y ↦ p_{D}(U(y, ⊥))], e^{∗}[b ↦ p_{E}(U(⊥, b))] )

Hierbei seien mit p_{D} und p_{E} die Projektionen vom Produkt D ×E in der Kategorie POSET in die Faktoren D und E bezeichnet.

Beweis: Weise für alle (x, a) ∈ D × E und für alle U ∈ (D × E)^{D×E} nach:

(i) h^{∗}(h(x, a)) = (x, a)

h^{∗}(h(x, a)) = h^{∗}(d(x) × e(a))
= ( d^{∗}[y ↦ p_{D}(d(x)(y), e(a)(⊥))], e^{∗}[b ↦ p_{E}(d(x)(⊥), e(a)(b))] )
= ( d^{∗}[y ↦ d(x)(y)], e^{∗}[b ↦ e(a)(b)] )
= (\underbrace{d^{∗}(d}_{=id_{D}}(x)), \underbrace{e^{∗}(e}_{=id_{E}}(a))) = (x, a)

(ii) h(h^{∗}(U)) ≤ U

h(h^{∗}(U))
= h(d^{∗}[y ↦ p_{D}(U(y, ⊥))], e^{∗}[b ↦ p_{E}(U(⊥, b))])
= ( \underbrace{d(d^{∗}}_{≤id_{D^{D}}}[y ↦ p_{D}(U(y, ⊥))]) ) × ( \underbrace{e(e^{∗}}_{≤id_{E^{E}}}[b ↦ p_{E}(U(⊥, b))]) )
≤ (y ↦ p_{D}(U(y, ⊥))) × (b ↦ p_{E}(U(⊥, b)))
= (y, b) ↦ (p_{D}(\underbrace{U(y, ⊥)}_{≤U(y,b)}), p_{E}(\underbrace{U(⊥, b)}_{≤U(y,b)}))
≤ (y, b) ↦ U(y, b) = U

Das Reduktionsmodell (D × E, h, h^{∗}) mit h, h^{∗} wie in Lemma 4.9 ist kein Produkt in der Kategorie RED_{⊥}, denn dann müßte es Morphismen von D × E in die Faktoren D und E geben. Jeder Morphismus in RED_{⊥} ist aber ein Einbettungs-Projektions-Paar, und das kartesische Produkt D × E läßt sich im allgemeinen nicht in D bzw. E injektiv abbilden. Im nächsten Teilkapitel wird jedoch nachgewiesen, daß die Abbildung × die Eigenschaften eines Tensorprodukts hat und RED_{⊥} symmetrisch monoidal ist. Zuvor wollen wir aber einen Bifunktor F: RED_{⊥} × RED_{⊥} → RED_{⊥} definieren, der zwei Modelle D, E auf das Modell D × E abbildet,welches in Lemma 4.9 angegeben wurde. Für den Rest der Arbeit sei mit dem Reduktionsmodell D × E immer dieses ”kanonische“ Modell bezeichnet. Sei F̃: POSET × POSET → POSET der ”Produkt“-Funktor, der gegeben wird durch F̃(D, E) := D × E, F̃(f, g) := f × g. Auf der Kategorie RED_{⊥} läßt sich in gleicher Weise ein Funktor definieren durch

F: RED_{⊥} × RED_{⊥} → RED_{⊥}

F (D, E) := D × E und F ((f, f^{∗}), (g, g^{∗})) := (f, f^{∗}) × (g, g^{∗}) := (f × g, f^{∗} × g^{∗}) (12)

Für Morphismen (f, f^{∗}) und (g, g^{∗}) ist nachzuweisen, daß (f, f^{∗}) × (g, g^{∗}) ein Morphismus der Kategorie ist.

Hilfssatz 4.10 (i) Seien (D, d, d^{∗}) und (D′, d′, (d′)^{∗}) und (E, e, e^{∗}) und (E′, e′, (e′)^{∗}) ∈ Ob(RED_{⊥}). Sind Morphismen (f, f^{∗}) ∈ RED_{⊥}(D, D′) und (g, g^{∗}) ∈ RED_{⊥}(E, E′)

gegeben, so ist (f×g, f^{∗}×g^{∗}) ∈ RED_{⊥}(D × E, D′ × E′).

(ii) Definiert man F wie in Gleichung (12), so ist F tatsächlich ein Funktor.

Beweis: zu (i):

POSET  \overline{F̃}  POSET
D  D  E  E  D × E  D × E

[figure: D′; f; D′; f^{∗}; E′; g; E′; g^{∗}; D′ × E′; f × g; D′ × E′; f^{∗} × g^{∗}]

Da (f × g)^{∗} = f^{∗} × g^{∗} gilt, ist (f × g, f^{∗} × g^{∗}) ein Einbettung-Projektions-Paar. Nachzuweisen bleibt die Eigenschaft (K1). Sei die Einbettung h wieder wie in Lemma 4.9 definiert und die Einbettung k durch k: D′ × E′ → (D′ × E′)^{D′×E′}, k(x, a) := d′(x)×e′(a). Es wird benutzt, daß sowohl (f, f^{∗}) als auch (g, g^{∗}) die Eigenschaft (K1) hat. Sei nun (x, a) ∈ D × E. Dann ist

((f × g)^{f^{∗}×g^{∗}} ∘ h)(x, a)
= (f × g) ∘ h(x, a) ∘ (f^{∗} × g^{∗})
=^{Def. h}(f × g) ∘ (d(x) × e(a)) ∘ (f^{∗} × g^{∗})
= (f ∘ d(x) ∘ f^{∗}) × (g ∘ e(a) ∘ g^{∗})
=^{(K1)}(d′(f(x))) × (e′(g(a))) =^{Def. k} k(f(x), g(a)),  also kommutiert

[figure: D × E; h; (D × E)^{D×E}; D′ × E′; f × g; k; (D′ × E′)^{D′×E′}; (f × g)^{f^{∗}×g^{∗}}]

zu (ii): F erhält die identischen Morphismen, denn

F ((id_{D}, id_{D}), (id_{E}, id_{E})) = (id_{D} × id_{E}, id_{D} × id_{E})
=^{F̃ Funktor} (id_{D×E}, id_{D×E}) = (id_{F (D,E)}, id_{F (D,E)})

38 4 EINE KATEGORIE VON REDUKTIONSMODELLEN

Des weiteren verträgt sich F mit der Komposition von Morphismen, denn es ist

F ( (f, f^{∗}) ∘ (f′, (f′)^{∗}) , (g, g^{∗}) ∘ (g′, (g′)^{∗}) )

= F ( (f ∘ f′, (f′)^{∗} ∘ f^{∗}) , (g ∘ g′, (g′)^{∗} ∘ g^{∗}) )
= ( (f ∘ f′) × (g ∘ g′) , ((f′)^{∗} ∘ f^{∗}) × ((g′)^{∗} ∘ g^{∗}) )
=^{F̃ Funktor}( (f × g) ∘ (f′ × g′) , ((f′)^{∗} × (g′)^{∗}) ∘ (f^{∗} × g^{∗}) )
= (f × g, f^{∗} × g^{∗}) ∘ (f′ × g′, (f′)^{∗} × (g′)^{∗})
= F ((f, f^{∗}), (g, g^{∗})) ∘ F ((f′, (f′)^{∗}), (g′, (g′)^{∗}))

[figure: f′; (f′)^{∗}; g′; (g′)^{∗}; f; f^{∗}; g; g^{∗}]

4.3 RED_{⊥} ist eine symmetrisch monoidale Kategorie 39

4.3 RED_{⊥} ist eine symmetrisch monoidale Kategorie

Im letzten Kapitel wurde gezeigt, daß sich für Reduktionsmodelle D und E auf ”kanonische Weise“ ein Reduktionsmodell auf dem Produkt D × E geordneter Mengen angeben läßt. Wie schon festgestellt wurde, ist dieses kein Produkt im kategoriellen Sinne, aber zumindest läßt sich beweisen, das RED_{⊥} mit dem angegebenen Produkt-Funktor zu einer symmetrisch monoidalen Kategorie wird.

SATZ 4.11 Es seien der Bifunktor

⊗: RED_{⊥} × RED_{⊥} → RED_{⊥}
(D, E) ↦ D × E
((f, f^{∗}), (g, g^{∗})) ↦ (f × g, f^{∗} × g^{∗}),

das Objekt 1 := ({⊥}, const_{⊥}, const_{⊥}) ∈ Ob(RED_{⊥}) und für alle Objekte C, D, E ∈ Ob(RED_{⊥}) die Ordnungsisomorphismen

α_{C,D,E}: C × (D × E) → (C × D) × E  γ_{D,E}: D × E → E × D
(x, (y, z)) ↦ ((x, y), z)  (x, y) ↦ (y, x)

λ_{D}: 1 × D → D  σ_{D}: D × 1 → D
(⊥, x) ↦ x  (x, ⊥) ↦ x

gegeben. Dann lassen sich für C, D, E ∈ Ob(RED_{⊥}) folgende Morphismen in RED_{⊥} definieren:

ᾱ_{C,D,E} := (α_{C,D,E}; α_{C,D,E}^{−1}): C × (D × E) → (C × D) × E
γ̄_{D,E} := (γ_{D,E}; γ_{D,E}^{−1}): D × E → E × D
λ̄_{D} := (λ_{D}, λ_{D}^{−1}): 1 × D → D
σ̄_{D} := (σ_{D}, σ_{D}^{−1}): D × 1 → D

Bezeichnet man – wie in Definition 3.8 – mit S den Bifunktor S: RED_{⊥}×RED_{⊥} → RED_{⊥}× RED_{⊥}, S(D, E) = (E, D), S(f, g) = (g, f), dann erhält man natürliche Isomorphismen

ᾱ: ⊗ ∘ (id_{RED_{⊥}} × ⊗) ⟶^{·} ⊗ ∘ (⊗ × id_{RED_{⊥}})
γ̄: ⊗ ∘ (id_{RED_{⊥}} × id_{RED_{⊥}}) ⟶^{·} ⊗ ∘ S ∘ (id_{RED_{⊥}} × id_{RED_{⊥}})
λ̄: ⊗ ∘ (1 × id_{RED_{⊥}}) ⟶^{·} id_{RED_{⊥}}
σ̄: ⊗ ∘ (id_{RED_{⊥}} × 1) ⟶^{·} id_{RED_{⊥}}

die zusammen mit dem Bifunktor ⊗ und dem Objekt 1 die Kategorie RED_{⊥} zu einer symmetrisch monoidalen Kategorie machen.

Wie man erwarten wird, läßt sich der Nachweis dafür, daß die angegebenen Morphismenfamilien (ᾱ_{C,D,E})_{C,D,E}, (γ̄_{D,E})_{D,E}, (λ̄_{D})_{D} und (σ̄_{D})_{D} natürliche Isomorphismen in RED_{⊥} sind, führen mit Hilfe der natürlichen Isomorphismen (α_{C,D,E})_{C,D,E}, (γ_{D,E})_{D,E}, (λ_{D})_{D} und (σ_{D})_{D} in POSET. Wir definieren den Vergißfunktor

U: RED_{⊥} → POSET
U(D, d, d^{∗}) := D
U(f, f^{∗}) := f

Er bildet Reduktionsmodelle (D, d, d^{∗}), (D, d_{0}, d_{0}^{∗}), die auf derselben geordneten Menge D definiert sind, auf die Menge D ab. Deshalb schreibt man auch kürzer U(D) statt U(D, d, d^{∗}); die Einbettung d wird ”vergessen“. Sind F, G: RED_{⊥} → RED_{⊥} Funktoren, so erhält man Funktoren U ∘ F, U ∘ G: RED_{⊥} → POSET, die wir auch kürzer mit UF, UG bezeichnen. Bevor wir den Beweis von Satz 4.11 führen, zeigen wir den

Hilfssatz 4.12 Seien F, G: RED_{⊥} → RED_{⊥} Funktoren derart, daß für den oben angegebenen Vergißfunktor U gilt:

für alle (D, d, d^{∗}), (E, e, e^{∗}) ∈ Ob(RED_{⊥}) gilt: D = E
⇒ ( UF (D, d, d^{∗}) = UF (E, e, e^{∗}) und UG(D, d, d^{∗}) = UG(E, e, e^{∗}) ) (13)

(”Wenn Modelle die gleiche Grundmenge haben, so haben dies auch ihre Funktorbilder.“) Sei des weiteren ein natürlicher Isomorphismus η: UF ⟶^{·} UG (in POSET) gegeben, derart, daß gilt:

für alle (D, d, d^{∗}), (E, e, e^{∗}) ∈ Ob(RED_{⊥}) gilt:
D = E ⇒ η_{(D,d,d^{∗})} = η_{(E,e,e^{∗})} : UF (D) → UG(D)  (14)

Man schreibt deshalb auch kürzer η_{D} statt η_{(D,d,d^{∗})}, da der Isomorphismus η_{D} nicht von der Einbettung d: D → D^{D} abhängt. Mit η_{D}^{−1} wird die Inverse von η_{D} bezeichnet. Ist nun für jedes Modell (D, d, d^{∗}) ∈ Ob(RED_{⊥}) das Einbettungs-Projektions-Paar (η_{D}, η_{D}^{−1}) ein Morphismus aus RED_{⊥}(F (D, d, d^{∗}), G(D, d, d^{∗})) so ist

η̄: F ⟶^{·} G

\begin{aligned}η̄_{(D,d,d^{∗})} : & F (D, d, d^{∗}) → G(D, d, d^{∗}) \\ & η̄_{(D,d,d^{∗})} := (η_{D}, η_{D}^{−1}) \end{aligned}

ein natürlicher Isomorphismus (in RED_{⊥}).

Beweis: Seien F, G: RED_{⊥} → RED_{⊥} Funktoren und sei η: UF ⟶^{·} UG ein natürlicher Isomorphismus mit den zusätzlichen in der Voraussetzung angegebenen Eigenschaften. Dann gibt es für jedes Modell D ∈ Ob(RED_{⊥}) einen Isomorphismus η_{D}: UF (D) → UG(D) mit der Inversen η_{D}^{−1} : UG(D) → UF (D). Die Transformation (η_{D})_{D∈Ob(RED_{⊥})} ist natürlich in D, also kommutiert das folgende Diagramm:

RED_{⊥}  [figure: UF; UG]  POSET
∀D  UF (D) \overline{η_{D}} UG(D)

[figure: ∀E; ∀(f, f^{∗}); UF (E); UF (f, f^{∗}); η_{E}; UG(E); UG(f, f^{∗})]

(15)

Nach Voraussetzung ist für jedes Modell (D, d, d^{∗}) das Paar η̄_{(D,d,d^{∗})} := (η_{D}, η_{D}^{−1}): F (D, d, d^{∗}) → G(D, d, d^{∗}) ein Morphismus in RED_{⊥}. Mit Hilfssatz 4.4(b) ist dann (η_{D}, η_{D}^{−1}) schon ein Isomorphismus mit der Inversen (η_{D}^{−1}, η_{D}). Die Transformation (η̄_{D})_{D∈Ob(RED_{⊥})} = ((η_{D}, η_{D}^{−1}))_{D∈Ob(RED_{⊥})} ist natürlich in D, falls folgendes Diagramm kommutiert:

RED_{⊥}  [figure: F; G]  RED_{⊥}
∀(D, d, d^{∗})  F (D, d, d^{∗}) \overline{^{(η_{D},η_{D}^{−1})}} G(D, d, d^{∗})

[figure: ∀(E, e, e^{∗}); ∀(f, f^{∗}); F (E, e, e^{∗}); F (f, f^{∗}); (η_{E},η_{E}^{−1}); G(E, e, e^{∗}); G(f, f^{∗})]

Das Diagramm kommutiert genau dann, wenn die zugehörigen Einbettungs- bzw. Projektions-Diagramme in POSET kommutieren. Bezeichnet der Index ‘1’ den Einbettungsteil von einem Morphismus, der Index ‘2’ den Projektionsteil, so besagt die letztgenannte Forderung:

η_{E} ∘ F_{1}(f, f^{∗}) =^{!} G_{1}(f, f^{∗}) ∘ η_{D}

F_{2}(f, f^{∗}) ∘ η_{E}^{−1} =^{!} η_{D}^{−1} ∘ G_{2}(f, f^{∗})

Nach der Definition von U ist aber UF (f, f^{∗}) = F_{1}(f, f^{∗}) und UG(f, f^{∗}) = G_{1}(f, f^{∗}). Mit dem Diagramm 15 gilt folglich η_{E} ∘ F_{1}(f, f^{∗}) = G_{1}(f, f^{∗}) ∘ η_{D}. Bemerkung 4.3 besagt, daß aus der Gleichheit von Einbettungen auch die Gleichheit der zugehörigen Projektionen folgt. Also ist auch F_{2}(f, f^{∗}) ∘ η_{E}^{−1} = η_{D}^{−1} ∘ G_{2}(f, f^{∗})

Im folgenden wird der Beweis von Satz 4.11 nachgeholt:

Beweis: (von Satz 4.11) Wir wollen den Hilfssatzes 4.12 für die natürlichen Isomorphismen α, γ, λ und σ verwenden und weisen als erstes alle Voraussetzungen nach. Die Funktoren ⊗, id_{RED_{⊥}}, S und 1 erfüllen die in Hilfssatz 4.12 geforderte Eigenschaft (13), denn es gilt:

D = D′, E = E′ ⇒ U((D, d, d^{∗}) ⊗ (E, e, e^{∗})) = D × E
= D′ × E′ = U((D′, d_{0}, d_{0}^{∗}) ⊗ (E′, e_{0}, e_{0}^{∗}))

und U × U(S((D, d, d^{∗}), (E, e, e^{∗}))) = (E, D)

= (E′, D′) = U × U(S((D′, d_{0}, d_{0}^{∗}), (E′, e_{0}, e_{0}^{∗})))

Für die Funktoren id_{RED_{⊥}} und 1 ist die Eigenschaft (13) offensichtlich klar. Die Komposition und die Produktbildung von Funktoren erhalten diese Eigenschaft. Demnach wird sie auch von den Funktoren aus Satz 4.11 erfüllt, für die ᾱ, γ̄, λ̄ bzw. σ̄ als natürliche Isomorphismen nachgerechnet werden sollen. In der Voraussetzung des zu beweisenden Satzes werden die Ordnungsisomorphismen α_{C,D,E}, γ_{D,E}, λ_{D} und σ_{D} definiert, welche in allen Komponenten natürliche Isomorphismen zwischen den entsprechenden Funktoren von RED_{⊥} nach POSET sind. Die Isomorphismen α_{C,D,E}, γ_{D,E}, λ_{D} und σ_{D} sind offensichtlich unabhängig von Einbettungen c: C → C^{C}, d: D → D^{D} und e: E → E^{E} gegeben. Die natürlichen Isomorphismen α, γ, λ und σ haben also die Eigenschaft (14). Die folgende (leichte) Rechnung zeigt, daß die angegebenen Einbettungs-Projektions-Paare ᾱ_{C,D,E}, γ̄_{D,E}, λ̄_{D} und σ̄_{D} Morphismen in RED_{⊥} sind, d.h. die Eigenschaft (K1) haben. Genauer: seien C, D, E ∈ Ob(RED_{⊥}). Dann sind (α_{C,D,E}, α_{C,D,E}^{−1}) ∈ RED_{⊥}(C × (D × E), (C × D) × E) und (γ_{D,E}; γ_{D,E}^{−1}) ∈ RED_{⊥}(D × E, E × D) und (λ_{D}, λ_{D}^{−1}) ∈ RED_{⊥}(1 × D, D) und (σ_{D}, σ_{D}^{−1}) ∈ RED_{⊥}(D × 1, D), falls die folgenden Diagramme kommutieren:

[figure: C × (D × E); (x,(y,z))↦c(x)×(d(y)×e(z)); (C × (D × E))^{C×(D×E)}; (C × D) × E; α_{C,D,E}; ((x,y),z)↦(c(x)×d(y))×e(z); ((C × D) × E)^{(C×D)×E}; (α_{C,D,E})^{α_{C,D,E}^{−1}}]

[figure: D × E; (x,y)↦d(x)×e(y); (D × E)^{D×E}; E × D; γ_{D,E}; (y,x)↦e(y)×d(x); (E × D)^{E×D}; (γ_{D,E})^{γ_{D,E}^{−1}}]

[figure: 1 × D; (⊥,x)↦const_{⊥}×d(x); (1 × D)^{1×D}; D × 1; (x,⊥)↦d(x)×const_{⊥}; (D × 1)^{D×1}]

[figure: D; λ_{D}; d; D^{D}; ^{λ_{D}^{λ_{D}^{−1}}}; D; σ_{D}; d; D^{D}; ^{σ_{D}^{σ_{D}^{−1}}}]

Das obere Diagramm kommutiert, weil

[(α_{C,D,E})^{α_{C,D,E}^{−1}}](c(x) × (d(y) × e(z)))
= α_{C,D,E} ∘ (c(x) × (d(y) × e(z))) ∘ α_{C,D,E}^{−1}
= (c(x) × d(y)) × e(z)  , da α_{C,D,E} bzw. α_{C,D,E}^{−1} nur ”umklammern“
= [(x, (y, z)) ↦ (c(x) × d(y)) × e(z)](α_{C,D,E}(x, (y, z)))

Das mittlere Diagramm kommutiert, weil

[(γ_{D,E})^{γ_{D,E}^{−1}}](d(x) × e(y))
= γ_{D,E} ∘ (d(x) × e(y)) ∘ γ_{D,E}^{−1}
= e(y) × d(x)  , da γ_{D,E} bzw. γ_{D,E}^{−1} nur ”vertauschen“
= [(y, x) ↦ e(y) × d(x)](γ_{D,E}(x, y))

Die beiden unteren Diagramme kommutieren, da

λ_{D}^{λ_{D}^{−1}}(const_{⊥} × d(x))  σ_{D}^{σ_{D}^{−1}}(d(x) × const_{⊥})
= λ_{D} ∘ (const_{⊥} × d(x)) ∘ λ_{D}^{−1}  = σ_{D} ∘ (d(x) × const_{⊥}) ∘ σ_{D}^{−1}
= d(x) = d(λ_{D}(⊥, x))  = d(x) = d(σ_{D}(x, ⊥))

Nachdem alle Voraussetzungen von Hilfssatz 4.12 nachgewiesen wurden, liefert seine Anwendung, daß ᾱ, γ̄, λ̄ und σ̄ natürliche Isomorphismen sind. Für den Beweis, daß RED_{⊥} eine symmetrisch monoidale Kategorie ist, bleibt als letztes zu überlegen, daß folgende Diagramme für alle B, C, D, E ∈ Ob(RED_{⊥}) kommutieren (siehe auch Definition 3.8 einer symmetrisch monoidalen Kategorie):

[figure: B × (C × (D × E)); ᾱ_{B,C,D×E}; (B × C) × (D × E); ᾱ_{B×C,D,E}; ((B × C) × D) × E; B × ((C × D) × E); id_{B} × ᾱ_{C,D,E}; ᾱ_{B,C×D,E}; (B × (C × D)) × E; ᾱ_{B,C,D×id_{E}}]

D × (1 × E) \overline{ᾱ_{D,1,E} ; }(D × 1) × E
1 × 1 [figure: λ̄_{1}; σ̄_{1}] 1
[figure: D × E; id_{D} × λ̄_{E}; =; D × E; σ̄_{D} × id_{E}]
[figure: E × D; γ̄_{E,D}; D × E; D × 1; γ̄_{D,1}; 1 × D]
[figure: id_{E×D}; σ̄_{D}]
[figure: E × D; γ̄_{D,E}; D; λ̄_{D}]

[figure: C × (D × E); ᾱ_{C,D,E}; (C × D) × E; γ̄_{C×D,E}; E × (C × D); C × (E × D); id_{C} × γ̄_{D,E}; ᾱ_{C,D,E}; (C × E) × D; γ̄_{C,E} × id_{D}; (E × C) × D; ᾱ_{E,C,D}]

Wir benutzen wieder die Bemerkung 4.3. Folglich kommutiert ein Diagramm in RED_{⊥} genau dann, wenn das zugehörige Diagramm von Einbettungen in POSET kommutiert. Läßt man bei den sechs gewünschten Diagrammen den Querstrich über den Namen der natürlichen Isomorphismen weg, betrachtet also α, γ, λ bzw. σ statt ᾱ, γ̄, λ̄ bzw. σ̄, so erhält man die zugehörigen Diagramme von Einbettungen, welches Diagramme in POSET sind. Sie kommutieren offensichtlich, da die Abbildungen α_{C,D,E}, γ_{D,E}, λ_{D} und σ_{D} sich mit dem Produkt in POSET vertragen. Damit ist gezeigt, daß RED_{⊥} eine symmetrisch monoidale Kategorie ist.

Literatur

[AJ94] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, 1994.

[Bar84] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984.

[Mac71] S. Mac Lane. Categories for the Working Mathematician. Springer Verlag, Berlin, 1971.

[Plo94] G. Plotkin. A semantics for static type inference. Information and Computation, 109:256–299, 1994.

[Sel97] P. Selinger. Functionality, Polymorphism, and Concurrency: A Mathematical Investigation of Programming Paradigms. PhD thesis, University of Pennsylvania, June 1997. 129 pages.