Monomorphe Typsysteme des λ-Kalküls

Überarbeitete Version der Diplomarbeit von Michael Marz zuletzt aktualisiert: 13. Oktober 1995

Betreuer: Dr. A. Jung Fachbereich Mathematik

(λxy.y)Ω(λz.z)

[figure: β; β]
(λy.y)(λz.z)  (λxy.y)Ω(λz.z)
[figure: β; β; β]
λz.z  (λy.y)(λz.z)  (λxy.y)Ω(λz.z)
[figure: β; β; β]
λz.z  (λy.y)(λz.z)  (λxy.y)Ω(λz.z)
...........  ...........  ...........

�

Technische Hochschule Darmstadt Juni 1995

Inhaltsverzeichnis

Einleitung 2 1 Ungetypter λ-Kalkül 3 2 Freie Gruppoide als Typsysteme des λ-Kalküls 8 3 Starke Normalisierbarkeit monomorph getypter λ-Terme 28 4 Zusammenfassung 45 Literaturverzeichnis 46

Einleitung

Welche Typsysteme des λ-Kalküls gewährleisten starke Normalisierbarkeit? Diese Frage hat eine zentrale Bedeutung in der Theorie des λ-Kalküls. Auf die Funktionale Programmierung übertragen, entspricht starke Normalisierbarkeit genau der Terminierung von Programmen. Für zahlreiche Typsysteme ist diese Frage bereits positiv beantwortet. N. Mendler untersucht in [Men91] in diesem Zusammenhang Systeme mit rekursiven Typen und speziellen Typgleichungen. Seine Ergebnisse liegen dieser Arbeit zugrunde.

Das erste Kapitel dieser Arbeit gibt eine kurze Einführung in die Theorie des ungetypten λ-Kalküls. Im zweiten Kapitel werden Typrelationen auf monomorphen Typsystemen in einer allgemeinen Form eingeführt und grundlegende Eigenschaften wie beispielsweise Typtreue (”subject reduction“) untersucht. Zu diesem Zweck werden K-Typsysteme eingeführt; die dazu benötigten Grundbegriffe aus der Allgemeinen Algebra werden am Anfang des Kapitels bereitgestellt. Im dritten Kapitel wird eine graphentheoretische Charakterisierung von Mendlers Kriterium zur starken Normalisierbarkeit gegeben und dieses Ergebnis auf den allgemeinen Fall übertragen. Durch den allgemeinen Ansatz ist es möglich, auch das Entscheidbarkeitsproblem der Typisierung für normalisierende K-Typsysteme positiv zu beantworten.

An dieser Stelle möchte ich denjenigen danken, die mir während meines Studiums und bei der Erstellung der Arbeit geholfen haben. Hervorheben möchte ich hierbei Prof. Dr. Klaus Keimel, der mich durch seine engagierten Vorlesungen mathematisch stark beeinflußt hat.

Desweiteren möchte ich Prof. Dr. PawełUrzyczyn aus Warschau für sein großes Interesse und einige nützliche Hinweise danken.

Ein besonderer Dank geht an Mathias Kegelmann für die langen und leider manchmal fruchtlosen Diskussionen sowie für sein penibles Korrekturlesen der Arbeit.

Schließlich möchte ich mich bei Dr. Achim Jung für die hervorragende Betreuung bedanken, bei der er in schwierigen Phasen großes Verständnis zeigte und durch zahlreiche Ideen stets neue Impulse gab. Durch ihn war es mir möglich, die Arbeit auch mit ausländischen Wissenschaftlern zu diskutieren.

Darmstadt, 19. Juni 1995 Michael Marz

1 Ungetypter λ-Kalkül

Der λ-Kalkül wurde 1932 von A. Church entwickelt. Church verfolgte ein neues Konzept zur Begründung der Mathematik und benutzte den λ-Kalkül als einfache Darstellungsform für Funktionen. Sein Grundkonzept scheiterte, dennoch hat sich der λ-Kalkül zu einer eigenständigen, ausdrucksstarken Theorie mit Anwendungen in der Berechenbarkeitstheorie und in letzter Zeit zunehmend in der Funktionalen Programmierung entwickelt. [Bar92] liefert einen guten Überblick über die Grundlagen des λ-Kalküls, eine ausführliche Einführung findet man in [HS86]. Für weitergehende Ergebnisse siehe [Bar84].

In diesem Kapitel werden die Grundbegriffe des λ-Kalküls und einige Eigenschaften erklärt, die zum Verständnis der Arbeit nötig sind.

Im Umgang mit den in der Mathematik üblichen Symbolen zur Bezeichnung von Funktionen entstehen häufig Probleme, wenn Funktionale höherer Ordnung auftreten. Zu jedem Funktional müssen stets Definitions- und Wertebereich angegeben werden. Die λ-Schreibweise vermeidet dies, indem prinzipiell jede Funktion auf alles angewendet werden kann. Durch Einführung von Typsystemen wird dieser Willkür vorgebeugt, dies ist Gegenstand der folgenden Kapitel.

Ab sofort sei X eine abzählbar unendliche Variablenmenge.

Definition 1.1 Die Menge Λ aller λ-Terme ist induktiv wie folgt definiert:

x ∈ X ⇒ x ∈ Λ
s, t ∈ Λ ⇒ (st) ∈ Λ  (Applikation)
x ∈ X, t ∈ Λ ⇒ (λx.t) ∈ Λ  (Abstraktion)

Ein λ-Term der Form (st) kann daher gelesen werden als: wende die Funktion s auf das Argument t an. Der Term (λx.t) stellt eine Funktion dar, die x auf t abbildet, wobei t von x abhängen darf. Oft lassen wir die äußeren Klammern eines λ-Terms einfach weg, wir schreiben stu statt ((st)u) und λx.st statt (λx.(st)). Desweiteren benutzen wir λx_{1}x_{2} … x_{n}.t als Kurzschreibweise für λx_{1}.λx_{2}…. λx_{n}.t. Die Länge len(t) eines λ-Terms t ist induktiv definiert durch

len(t) = \{ \begin{matrix}1 & falls t ∈ X \\ len(t_{1}) + len(t_{2}) & falls t = t_{1}t_{2} \\ len(t_{1}) + 1 & falls t = λx.t_{1} \end{matrix}

Definition 1.2 Das Vorkommen einer Variablen x ∈ X in einem λ-Term t heißt gebunden, falls es in einem in t enthaltenen λ-Term der Form λx.s enthalten ist, ansonsten heißt es frei. BV(t) bezeichnet die Menge aller Variablen, die in t gebunden vorkommen, FV(t) ist die Menge aller in t frei vorkommenden Variablen.

Beispiel: Im λ-Term t := λy.zy(λz.zx) kommt x nur frei, y nur gebunden und z sowohl frei als auch gebunden vor.

Definition 1.3 Seien s, t λ-Terme und x ∈ X eine Variable. Die Substitution t[s/x] (”s für x in t”) ist induktiv definiert:

• t = x:

x[s/x] := s

• t = y ≠ x, y ∈ X:

y[s/x] := y

• t = t_{1}t_{2}:

(t_{1}t_{2})[s/x] := (t_{1}[s/x])(t_{2}[s/x])

• t = λx.t_{1}:

(λx.t_{1})[s/x] := λx.t_{1}

• t = λy.t_{1}, y ≠ x:

(λy.t_{1})[s/x] := λz.(t_{1}[z/y][s/x]) für ein z ∈ X mit z ∉ FV(s) ∪ FV(t_{1})

Weil im letzten Fall die Wahl von z willkürlich ist, ist die Substitution nicht eindeutig festgelegt. Dies ist aber kein großer Nachteil. λ-Terme werden als Funktionen betrachtet, somit ist die Bezeichnung der Funktionsargumente an sich unerheblich.

Definition 1.4 Falls zwei λ-Terme s und t sich nur durch die Benennung gebundener Variablen unterscheiden, so heißen sie α-äquivalent, wir schreiben: s =_{α} t.

Man überprüft leicht, daß die α-Äquivalenz tatsächlich eine Äquivalenzrelation ist, auf deren Klassen die Substitution wohldefiniert ist. Für den Rest des Kapitels fassen wir jeden λ-Term als Repräsentant seiner α-Äquivalenzklasse auf und schreiben beispielsweise λx.xz = λy.yz.

Um wirklich sinnvoll im λ-Kalkül ”rechnen“ zu können, muß sich ein λ-Term der Form (λx.t)s zu t[s/x] auswerten lassen. Dies leistet die β-Reduktion:

Definition 1.5 Ein β-Redex ist ein λ-Term der Form (λx.t)s, der Term t[s/x] heißt sein Kontraktum. Ist u′ derjenige λ-Term, den man erhält, wenn in u ∈ Λ das Auftreten eines β-Redex durch sein Kontraktum ersetzt wird, so ist u _{β}^{}u′ eine β-Kontraktion. Eine β-Reduktion u [figure: β] u′ ist eine endliche (möglicherweise leere) Folge von β-Kontraktionen.

Die β-Reduktion ist mit der Substitution verträglich, denn es gilt:

Lemma 1.6 Seien s, t, u ∈ Λ und x ∈ X mit s [figure: β] t. Dann gilt u[s/x] [figure: β] u[t/x] und s[u/x] [figure: β] t[u/x].

Beweis: Jede β-Kontraktion in s kann auch in u[s/x] durchgeführt werden, daraus folgt u[s/x] [figure: β] u[t/x]. Zum Beweis des zweiten Teils der Behauptung zeigen wir ((λy.w)v)[u/x] _{β}^{}w[v/y][u/x]. Es gilt:

((λy.w)v)[u/x] = ((λy.w)[u/x])(v[u/x])
= (λz.(w[z/y][u/x]))(v[u/x])

für ein z ∈ X, z ∉ FV(u) ∪ FV(w) nach Definition der Substitution. Weiter folgt

(λz.(w[z/y][u/x]))(v[u/x]) _{β}^{}w[z/y][u/x][v[u/x]/z]
= w[z/y][v/z][u/x] (da z ∉FV(u))
= w[v/y][u/x]  (da z ∉FV(w)).
□

Es gibt noch weitere Reduktionsregeln im λ-Kalkül:

Definition 1.7 Ein η-Redex ist ein λ-Term der Form λx.tx mit x ∉ FV(t), der Term t heißt sein Kontraktum. Ist u′ derjenige λ-Term, den man erhält, wenn in u ∈ Λ das Auftreten eines η-Redex durch sein Kontraktum ersetzt wird, so ist u _{η}^{}u′ eine η-Kontraktion. Eine βη-Reduktion u [figure: βη] u′ ist eine endliche (möglicherweise leere) Folge von β- und η-Kontraktionen.

Diese Definition wird dadurch motiviert, daß Funktionen miteinander identifiziert werden sollen, wenn sie zu gleichen Eingaben gleiche Ergebnisse liefern. Dies ist für λx.tx und t mit x ∉ FV(t) der Fall, denn es gilt:

(λx.tx)s _{β}^{}(tx)[s/x] = (t[s/x])(x[s/x]) = ts.

Folgendes Lemma zeigt, daß auch β- und βη-Reduktionen mit der Substitution verträglich sind:

Lemma 1.8 Seien s, t, u ∈ Λ und x ∈ X mit s [figure: βη] t. Dann gilt u[s/x] [figure: βη] u[t/x] und s[u/x] [figure: βη] t[u/x].

Beweis: Jede η-Kontraktion in s kann auch in u[s/x] durchgeführt werden, mit Lemma 1.6 folgt u[s/x] [figure: βη] u[t/x]. Zum Beweis des zweiten Teils der Aussage zeigen wir (λy.vy)[u/x] _{η}^{}v[u/x] für y ∉ FV(v). Nach Definition ist

(λy.vy)[u/x] = λz.((vy)[z/y][u/x])
= λz.(v[u/x])z

mit z ∉ FV(u)∪FV(v)∪{y}. Da auch z ∉ FV(v[u/x]), gilt (λy.vy)[u/x] _{η}^{}v[u/x]. Mit Lemma 1.6 folgt s[u/x] [figure: βη] t[u/x]. □

Sowohl die β- als auch die βη-Reduktion ist konfluent, das heißt, die Reihenfolge der Reduktionsschritte ist unerheblich. Der folgende Satz präzisiert diese Eigenschaft:

Satz 1.9 (Church-Rosser) Für beliebige λ-Terme s, t_{1}, t_{2} mit s [figure: βη] t_{1} sowie s [figure: βη] t_{2} gibt es einen λ-Term u mit t_{1} [figure: βη] u und t_{2} [figure: βη] u (analog für [figure: β] ).

s
[figure: βη; βη]
t_{1}  t_{2}
[figure: ..............; βη; ..............; βη]
u

Beweis: Wir geben die Skizze eines Beweises, der auf P. Martin-Löf und W. Tait zurückgeht, siehe [Tak92]. Dazu benötigen wir den Begriff der parallelen Reduktion ⇒, die wie folgt definiert ist:

• x ⇒ x für x ∈ X

• st ⇒ s′t′, falls s ⇒ s′ und t ⇒ t′

• λx.t ⇒ λx.t′, falls t ⇒ t′

• (λx.t)s ⇒ t′[s′/x], falls s ⇒ s′ und t ⇒ t′

• λx.tx ⇒ t′, falls x ∉ FV(t) und t ⇒ t′ Die βη-Reduktion ist die transitive Hülle der parallelen Reduktion ⇒. Daher genügt es zum Beweis von Satz 1.9 zu zeigen, daß aus s ⇒ t_{1} und s ⇒ t_{2} auch schon die Existenz eines λ-Terms u mit t_{1} ⇒ u und t_{2} ⇒ u folgt.

Zu jedem λ-Term t sei t^{∗} wie folgt definiert:

• x^{∗} = x für x ∈ X

• (st)^{∗} = s^{∗}t^{∗}, falls st kein β-Redex ist

• (λx.t)^{∗} = λx.t^{∗}, falls λx.t kein η-Redex ist

• ((λx.t)s)^{∗} = t^{∗}[s^{∗}/x]

• (λx.tx)^{∗} = t^{∗}, falls x ∉ FV(t) Mit Induktion über den Aufbau von s zeigt man, daß für ein beliebiges t ∈ Λ mit s ⇒ t auch t ⇒ s^{∗} gilt. Daraus folgt die Konfluenz von ⇒, was den Beweis vollendet.

□

2 Freie Gruppoide als Typsysteme des λ-Kalküls

Im ungetypten λ-Kalkül gibt es keine Einschränkungen für den Definitionsbereich von Termen. Insbesondere kann jeder λ-Term sogar auf sich selbst angewandt werden. Typsysteme bilden eine natürliche Form der Regulierung dieser Willkür: eine Funktion kann nur auf Argumente eines entsprechenden Typs angewandt werden. Dies hat zur Folge, daß zu einem gegebenen Typsystem nicht jeder λ-Term typisierbar ist, andererseits haben die mit geeigneten Typsystemen getypten λ-Terme schöne Eigenschaften, die wir in Kapitel 3 genauer untersuchen werden.

In diesem Kapitel sollen Typsysteme untersucht werden, die nur aus Grundtypen und Funktionentypen bestehen. Diese stellen die einfachsten Typsysteme der monomorphen Systeme dar, die im Gegensatz zu polymorphen Systemen wie beispielsweise Girards System F keine Typquantoren besitzen. Daher liegt es nahe, für Typsysteme Gruppoide zu benutzen. Dazu benötigen wir einige Begriffe und Resultate aus der Allgemeinen Algebra, die wir in die Sprache der Gruppoidtheorie übersetzen. Für eine ausführliche Einführung siehe z. B. [Ihr88].

Definition 2.1 Ein Gruppoid \underline{T} = (T , →) ist eine Menge T mit einer zweistelligen Operation →, wobei mit σ, τ ∈ T auch σ → τ ∈ T gilt. Die Elemente von T heißen Typen. Wir verwenden die übliche Konvention: τ_{1} → τ_{2} → τ_{3} steht für τ_{1} → (τ_{2} → τ_{3}). Eine Kongruenzrelation (oder kurz: Kongruenz) auf einem Gruppoid \underline{T} ist eine Relation ≈ auf T mit:

∀τ ∈ T : τ ≈ τ (Reflexivität)
∀σ, τ ∈ T : σ ≈ τ ⇒ τ ≈ σ (Symmetrie)
∀σ, τ, ρ ∈ T : σ ≈ τ, τ ≈ ρ ⇒ σ ≈ ρ (Transitivität)

∀σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ T : σ_{1} ≈ τ_{1}, σ_{2} ≈ τ_{2} ⇒ σ_{1} →σ_{2} ≈ τ_{1} →τ_{2} (Verträglichkeit)

Die Menge aller Kongruenzen auf \underline{T} heißt Con \underline{T} . Auf jedem Gruppoid T sind die Relationen Δ und ∇ mit

σΔτ ⇔ σ = τ und
σ∇τ für alle σ, τ ∈ T

stets Kongruenzen.

Zu einer Kongruenzrelation ≈ auf einem Gruppoid \underline{T} = (T , →) nennt man die Menge [τ]_{≈} := \{ξ ∈ T | ξ ≈ τ\} eine Kongruenzklasse auf \underline{T} . Wegen der Verträglichkeit von ≈ mit der Operation → ist →_{≈} mit [σ]_{≈} →_{≈} [τ]_{≈} = [σ → τ]_{≈} auf der Menge T /_{≈} := \{[τ]_{≈} | τ ∈ T \} wohldefiniert. Daher ist auch \underline{T} /_{≈} = (T /_{≈}, →_{≈}) ein Gruppoid, das sogenannte Faktor- oder Quotientengruppoid. Die Abbildung π_{≈}: \underline{T} → \underline{T} /_{≈} mit π_{≈}(τ) = [τ]_{≈} heißt kanonische Quotientenabbildung.

Lemma 2.2 Jede Relation ∼ auf einem Gruppoid \underline{T} läßt sich eindeutig zu einer kleinsten Kongruenzrelation ≈ mit σ ∼ τ ⇒ σ ≈ τ fortsetzen.

Beweis: Der Schnitt von Kongruenzrelationen ist wieder eine Kongruenzrelation. Die gesuchte Kongruenz ist also gerade der Schnitt aller Kongruenzen, die ∼ enthalten. □

Im folgenden sei zu einer gegebenen Relation ∼ mit ≈ stets die von ∼ erzeugte Kongruenz bezeichnet. Gilt σ ≈ τ für σ, τ ∈ T und eine Relation ∼, so gibt es dafür eine Herleitung in folgendem Kalkül:

\overline{(c)} ; σ ≈ τ falls σ ∼ τ  \overline{(r)} ; τ ≈ τ für alle τ ∈ T

σ ≈ τ ; \overline{(s)} ; τ ≈ σ  σ ≈ τ  τ ≈ ρ ; \overline{(t)} ; σ ≈ ρ  σ ≈ σ′ τ ≈ τ′ ; \overline{(v)} ; σ →τ ≈ σ′ →τ′

Definition 2.3 Ein (Gruppoid-) Homomorphismus ist eine Abbildung φ: \underline{T} → \underline{S} zwischen zwei Gruppoiden (\underline{T} , →\underline{T}), (\underline{S}, →\underline{S}), so daß gilt:

(Hom) ∀τ, τ′ ∈ \underline{T} : φ(τ →\underline{T} τ′) = φ(τ) →\underline{S} φ(τ′)

Existiert die Umkehrabbildung φ^{−1} : \underline{S} → \underline{T} , so erfüllt auch diese die Homomorphiebedingung. In diesem Fall ist φ ein (Gruppoid-) Isomorphismus, und die Gruppoide \underline{S} und \underline{T} heißen zueinander isomorph, in Zeichen: \underline{S} ≅ \underline{T} .

Die kanonische Quotientenabbildung π_{θ}: \underline{T} → \underline{T} /_{θ} und die Identität id\underline{T} : \underline{T} → \underline{T} mit id\underline{T} (τ) = τ sind stets Homomorphismen. Auch die Komposition φ ∘ ψ: \underline{R} → \underline{T} zweier Homomorphismen φ: \underline{S} → \underline{T} und ψ: \underline{R} → \underline{S} ist wieder ein Homomorphismus.

Wir werden sehen, daß der Begriff der Kongruenz mit dem der Homomorphie nahe verwandt ist. Dazu definieren wir den Kern eines Homomorphismus φ: \underline{T} → \underline{S} als ker(φ) = \{(τ, τ′) ∈ T ×T | φ(τ) = φ(τ′)\}. Für jeden Homomorphismus φ: \underline{T} → \underline{S} ist ker(φ) eine Kongruenzrelation, es gilt sogar:

Satz 2.4 (Homomorphiesatz) Sei φ: \underline{T} → φ(\underline{T} ) ein Homomorphismus. Dann gibt es einen Isomorphismus \overline{φ}: \underline{T} /_{ker(φ)} → φ(\underline{T} ) mit \overline{φ} ∘ π_{ker(φ)}(τ) = φ(τ) für alle τ ∈ \underline{T} .

Beweis: Man rechne nach, daß \overline{φ}: \underline{T} /_{ker(φ)} → φ(\underline{T} ) mit \overline{φ}([τ]_{ker(φ)}) = φ(τ) wohldefiniert, bijektiv und ein Homomorphismus ist. □

Definition 2.5 Sei J eine beliebige Menge. Ihre Elemente wollen wir Grundtypen nennen. Die Grammatik

τ ::= ι | τ →τ (ι beliebig aus J)

definiert die Menge F_{J} aller Typen über J. Zusammen mit der Operation → bildet \underline{F}_{J} = (F_{J} , →) ein Gruppoid. \underline{F}_{J} heißt Termgruppoid, von J frei erzeugt oder einfach frei. Um Verwechslungen mit λ-Termen zu vermeiden, benutzen wir die Bezeichnung freies Gruppoid. Die Länge len(τ) eines Typs τ ∈ F (\underline{F} frei), ist gerade die Anzahl der Pfeile in τ.

Für jedes J ist \underline{F}_{J} bis auf Isomorphie eindeutig bestimmt. Es gilt sogar:

Satz 2.6 Jedes Gruppoid \underline{T} ist homomorphes Bild eines freien Gruppoids.

Beweis: Setze φ: \underline{F}_{T} → \underline{T} mit φ(τ) := τ und φ(σ → τ) := φ(σ) →\underline{T} φ(τ) für alle σ, τ ∈ T . Dann ist φ der gesuchte Homomorphismus. □

Mit dem Homomorphiesatz 2.4 folgt daraus:

Korollar 2.7 Für jedes Gruppoid \underline{T} gibt es ein freies Gruppoid \underline{F} und eine Kongruenzrelation ≈ mit \underline{T} ≅ \underline{F}/_{≈}.

Beweis: Wähle \underline{F} = \underline{F}_{T}, φ wie im Beweis von Satz 2.6 und ker(φ) als Kongruenzrelation. □

Korollar 2.7 erlaubt es, sich bei monomorphen Typsystemen des λ-Kalküls auf freie Gruppoide mit Kongruenzen zu beschränken. Dies verschafft Vorteile in der Darstellung getypter λ-Terme.

Definition 2.8 Ein Typsystem ist ein Paar (\underline{F}, ≈), das aus einem freien Gruppoid \underline{F} und einer Kongruenzrelation ≈ besteht.

Prinzipiell gibt es zwei Möglichkeiten, Typsysteme des λ-Kalküls zu betrachten. Im ”Church-Style“ enthält dabei jeder λ-Term so viele Informationen wie möglich über seinen Typ. Dadurch ist die Frage, ob ein λ-Term einen gewissen Typ hat, auch in komplizierten Typsystemen immer entscheidbar. Im ”Curry-Style“ betrachtet man Typen als Prädikate für ungetypte λ-Terme. Dies ermöglicht, Probleme der Typisierbarkeit von Termen zu untersuchen. Solche Fragen spielen insbesondere in der Funktionalen Programmierung eine wichtige Rolle. Da wir uns mit Typisierbarkeitsfragen beschäftigen, benutzen wir den ”Curry-Style“.

Im folgenden sei X stets eine abzählbar unendliche Variablenmenge und (\underline{F}, ≈) ein Typsystem.

Definition 2.9 Eine Basis ist eine endliche Menge Γ von Ausdrücken (x : τ) mit x ∈ X und τ ∈ F, wobei es für jedes x ∈ X höchstens ein τ ∈ F mit (x : τ) ∈ Γ gibt.

Für die Definition getypter λ-Terme betrachten wir folgenden Kalkül:

\overline{(Var)} ; Γ ⊢ x : τ falls (x : τ) ∈ Γ

Γ ⊢ s : τ →σ Γ ⊢ t : τ
\overline{(App)}

Γ ⊢ st : σ

Γ, x : σ ⊢ t : τ

\overline{(Abs)}

Γ ⊢ λx.t : σ →τ

Γ ⊢ t : σ ; \overline{(Kon)} ; Γ ⊢ t : τ falls σ ≈ τ

wobei Γ, x : τ für Γ ∪ {(x : τ)} steht und es kein σ ∈ F \ {τ} mit (x : σ) ∈ F gibt. Anstelle von o / ⊢ t : τ schreibt man kurz ⊢ t : τ.

Definition 2.10 Die im obigen Kalkül herleitbaren Ausdrücke Γ ⊢ t : τ heißen Urteile. Ein bezüglich (\underline{F}, ≈) getypter λ-Term (kurz: λ_{(\underline{F},≈)}-Term) ist ein Ausdruck t : τ, für den es eine Basis Γ gibt, so daß Γ ⊢ t : τ ein Urteil ist.

Getypte λ-Terme erfüllen folgende Eigenschaften, die Rückschlüsse über den Aufbau des Terms und damit über seine Typisierbarkeit zulassen:

Lemma 2.11 (Erzeugungslemma) Sei Γ eine Basis mit Γ ⊢ t : τ für t ∈ Λ und τ ∈ F. Dann gilt:

a) Ist t = x ∈ X, so gibt es ein τ_{1} ∈ F mit τ_{1} ≈ τ und (x : τ_{1}) ∈ Γ.

b) Ist t = t_{1}t_{2}, so gibt es ein τ_{1} ∈ F mit Γ ⊢ t_{1} : τ_{1} →τ und Γ ⊢ t_{2} : τ_{1}.

c) Ist t = λx.t_{1}, so gibt es τ_{1}, τ_{2} ∈ F mit τ ≈ τ_{2} →τ_{1} und Γ, x : τ_{2} ⊢ t_{1} : τ_{1}.

Beweis: Wir beweisen alle drei Aussagen parallel mit Induktion über die Herleitung von Γ ⊢ t : τ, wobei wir nach der zuletzt angewandten Regel unterscheiden. Die Fälle (Var), (App) und (Abs) sind trivial. Im Fall

Γ ⊢ t : σ ; \overline{(Kon)} ; Γ ⊢ t : τ mit σ ≈ τ

unterscheiden wir nach der Struktur von t:

a) t = x ∈ X: Es gilt Γ ⊢ x : σ mit σ ≈ τ. Nach Induktionsannahme existiert ein τ_{1} ∈ F mit τ_{1} ≈ σ und (x : τ_{1}) ∈ Γ. Wegen der Transitivität von ≈ folgt τ_{1} ≈ τ.

b) t = t_{1}t_{2}: Es gilt Γ ⊢ t_{1}t_{2} : σ mit σ ≈ τ. Nach Induktionsannahme existiert ein τ_{1} mit Γ ⊢ t_{1} : τ_{1} → σ und Γ ⊢ t_{2} : τ_{1}. Wegen der Reflexivität und der Verträglichkeit von ≈ ist τ_{1} →σ ≈ τ_{1} →τ, also mit (Kon) auch Γ ⊢ t_{1} : τ_{1} →τ.

c) t = λx.t_{1}: Es gilt Γ ⊢ λx.t_{1} : σ mit σ ≈ τ. Nach Induktionsannahme existieren τ_{1}, τ_{2} ∈ F mit σ ≈ τ_{2} → τ_{1} und Γ, x : τ_{2} ⊢ t_{1} : τ_{1}. Wegen der Symmetrie und der Transitivität von ≈ folgt τ ≈ τ_{2} →τ_{1}.

□

Es fällt auf, daß die Verträglichkeit von ≈ nur teilweise benutzt wurde, nämlich in der Form

σ ≈ τ ⇒ τ′ →σ ≈ τ′ →τ.

Jede andere Eigenschaft von ≈ wird zum Beweis des Erzeugungslemmas in vollem Umfang benötigt.

Das Erzeugungslemma charakterisiert die Herleitungen getypter λ-Terme. Viele Beweise im getypten λ-Kalkül werden mit Induktion über den Termaufbau geführt, fast immer kommt dabei das Erzeugungslemma zum Tragen. So auch beim Beweis des folgenden Lemmas, das die Eigenschaften von Typbasen beschreibt:

Lemma 2.12 (Basislemma) Sei Γ eine Basis, t ∈ Λ und τ ∈ F.

a) Gilt Γ ⊢ t : τ und ist y ∈ X eine Variable, die weder in Γ noch in t enthalten ist, so gilt auch Γ, y : σ ⊢ t : τ für alle σ ∈ F.

b) Gilt Γ ⊢ t : τ, so gibt es für jede Variable x ∈ FV(t) einen Typ τ_{x} ∈ F mit (x : τ_{x}) ∈ Γ.

c) Gilt Γ ⊢ t : τ mit (y : σ) ∈ Γ und y ∉ FV(t), so gilt auch Γ \ {(y : σ)} ⊢ t : τ.

Beweis:

a) Induktion über den Termaufbau von t:

– t = x ∈ X: Nach dem Erzeugungslemma 2.11 gibt es ein τ_{1} ∈ F mit (x : τ_{1}) ∈ Γ ⊆ Γ, y : σ und τ_{1} ≈ τ. Mit (Var) und (Kon) folgt Γ, y : σ ⊢ x : τ.

– t = t_{1}t_{2}:

Nach dem Erzeugungslemma 2.11 gibt es ein τ_{1} ∈ F mit Γ ⊢ t_{1} : τ_{1} → τ und Γ ⊢ t_{2} : τ_{1}. Da y weder in t_{1} noch in t_{2} enthalten ist, folgt nach Induktionsannahme Γ, y : σ ⊢ t_{1} : τ_{1} → τ und Γ, y : σ ⊢ t_{2} : τ_{1}. Anwenden von (App) liefert Γ, y : σ ⊢ t_{1}t_{2} : τ.

– t = λx.t_{1}: Nach dem Erzeugungslemma 2.11 gibt es τ_{1}, τ_{2} ∈ F mit τ ≈ τ_{2} → τ_{1} und Γ, x : τ_{2} ⊢ t_{1} : τ_{1} . Nach Induktionsannahme folgt Γ, x : τ_{2}, y : σ ⊢ t_{1} : τ_{1}, Anwenden von (Abs) und (Kon) liefert Γ, y : σ ⊢ λx.t_{1} : τ.

b) Induktion über den Termaufbau von t:

– t = x ∈ X: Folgt direkt aus dem Erzeugungslemma 2.11.

– t = t_{1}t_{2}:

Alle freien Variablen von t_{1}t_{2} liegen in t_{1} oder in t_{2}. Mit dem Erzeugungslemma 2.11 folgt die Behauptung aus der Induktionsannahme.

– t = λx.t_{1}: Jede freie Variable von t ist bereits frei in t_{1}. Daher folgt die Behauptung erneut mit dem Erzeugungslemma 2.11 aus der Induktionsannahme.

c) Induktion über den Termaufbau von t:

– t = x ∈ X:

Nach dem Erzeugungslemma 2.11 gibt es ein τ_{1} ∈ F mit (x : τ_{1}) ∈ Γ und τ_{1} ≈ τ. Wegen x ≠ y ist auch (x : τ_{1}) ∈ Γ \ {(y : σ)}, Anwenden von (Var) und (Kon) liefert Γ \ {(y : σ)} ⊢ x : τ.

– t = t_{1}t_{2}:

Nach dem Erzeugungslemma 2.11 gibt es ein τ_{1} ∈ F mit Γ ⊢ t_{1} : τ_{1} → τ und Γ ⊢ t_{2} : τ_{1}. Nach Induktionsannahme gilt wegen y ∉ FV(t_{1}) ∪ FV(t_{2}) auch Γ \ {(y : σ)} ⊢ t_{1} : τ_{1} → τ und Γ \ {(y : σ)} ⊢ t_{2} : τ_{1}. Anwenden von (App) liefert Γ \ {(y : σ)} ⊢ t_{1}t_{2} : τ.

– t = λy.t_{1}:

Nach dem Erzeugungslemma 2.11 gibt es τ_{1}, τ_{2} ∈ F mit τ ≈ τ_{2} → τ_{1} und Γ, y : τ_{2} ⊢ t_{1} : τ_{1}. Da jede Variable höchstens einmal in Γ vorkommt, ist mit (y : σ) ∈ Γ also σ = τ_{2}. Damit gilt Γ, y : τ_{2} = Γ \ {(y : σ)} ∪ {(y : τ_{2})}, und es folgt Γ \ {(y : σ)} ∪ {(y : τ_{2})} ⊢ t_{1} : τ_{1}. Anwenden von (Abs) und (Kon) liefert Γ \ {(y : σ)} ⊢ λy.t_{1} : τ.

– t = λx.t_{1} mit x ≠ y: Nach dem Erzeugungslemma 2.11 gibt es τ_{1}, τ_{2} ∈ F mit τ ≈ τ_{2} → τ_{1} und Γ, x : τ_{2} ⊢ t_{1} : τ_{1}. Nach Induktionsannahme gilt Γ∪{(x : τ_{2})}\{(y : σ)} ⊢ t_{1} : τ_{1}, Anwenden von (Abs) und (Kon) liefert Γ \ {(y : σ)} ⊢ λx.t_{1} : τ.

□

Aus dem Basislemma folgt sofort:

Korollar 2.13 Zu jedem Urteil Γ ⊢ t : τ ist auch Γ′ ⊢ t : τ mit Γ′ := {(x : τ_{x}) | x ∈ FV(t)} ein Urteil.

Auch im getypten λ-Kalkül benötigt man den Begriff der Substitution. Daß diese keine Probleme bereitet, ist die Aussage des folgenden Lemmas:

Lemma 2.14 (Substitutionslemma) Sei Γ eine Basis, σ, τ ∈ F, x ∈ X und s, t ∈ Λ. Dann folgt aus Γ, x : σ ⊢ t : τ und Γ ⊢ s : σ auch Γ ⊢ t[s/x] : τ.

Beweis: Induktion über die Länge len(t):

• Induktionsanfang n = 1:

– t = x ∈ X:

Aus Γ, x : σ ⊢ x : τ folgt nach dem Erzeugungslemma 2.11 σ ≈ τ. Wegen x[s/x] = s folgt mit Γ ⊢ s : σ und (Kon) auch Γ ⊢ x[s/x] : τ.

– t = y ∈ X mit y ≠ x: Aus Γ, x : σ ⊢ y : τ folgt wegen y[s/x] = y mit dem Basislemma 2.12 Γ ⊢ y[s/x] : τ.

• Induktionsschluß:

– t = t_{1}t_{2}:

Nach dem Erzeugungslemma 2.11 existiert ein τ_{1} ∈ F mit Γ, x : σ ⊢ t_{1} : τ_{1} → τ und Γ, x : σ ⊢ t_{2} : τ_{1}. Nach Induktionsannahme gilt Γ ⊢ t_{1}[s/x] : τ_{1} → τ und Γ ⊢ t_{2}[s/x] : τ_{1}. Wegen (t_{1}t_{2})[s/x] = (t_{1}[s/x])(t_{2}[s/x]) folgt mit (App), daß Γ ⊢ (t_{1}t_{2})[s/x] : τ_{1}.

– t = λx.t_{1}:

Da Γ, x : σ ⊢ λx.t_{1} : τ, gibt es wegen (λx.t_{1})[s/x] = λx.t_{1} auch eine Herleitung für Γ, x : σ ⊢ (λx.t_{1})[s/x] : τ. Nach dem Basislemma 2.12 ist damit auch Γ ⊢ (λx.t_{1})[s/x] : τ, da x ∉ FV((λx.t_{1})[s/x]).

– t = λy.t_{1}, y ∈ X, y ≠ x : Nach dem Erzeugungslemma 2.11 gibt es τ_{1}, τ_{2} ∈ F mit Γ, x : σ, y : τ_{2} ⊢ t_{1} : τ_{1} und τ ≈ τ_{2} → τ_{1}. Sei z ∈ X eine Variable, die weder in Γ noch in s oder t enthalten ist mit (λy.t_{1})[s/x] = λz.(t_{1}[z/y][s/x]). Dann gilt nach dem Basislemma 2.12 auch Γ, x : σ, y : τ_{2}, z : τ_{2} ⊢ t_{1} : τ_{1}. Wegen Γ, x : σ, z : τ_{2} ⊢ z : τ_{2} folgt nach Induktionsannahme Γ, x : σ, z : τ_{2} ⊢ t_{1}[z/y] : τ_{1}. Da wegen des Basislemmas 2.12 mit Γ ⊢ s : σ auch Γ, z : τ_{2} ⊢ s : σ gilt, so folgt erneut aus der Induktionsannahme Γ, z : τ_{2} ⊢ t_{1}[z/y][s/x]. Dieser Schluß ist möglich, da len(t_{1}[z/y]) = len(t_{1}). Anwenden von (Abs) und (Kon) liefert wegen λz.(t[z/y][s/x]) = (λy.t_{1})[s/x] gerade Γ ⊢ (λy.t_{1})[s/x] : τ.

□

Folgendes Beispiel zeigt, daß aus Γ ⊢ s : τ und s =_{α} t nicht Γ ⊢ t : τ folgt:

Beispiel:

\overline{(Var)} ; x : σ, y : τ ⊢ x : σ

\overline{(Abs)}

y : τ ⊢ λx.x : σ → σ

ist eine korrekte Herleitung für y : τ ⊢ λx.x : σ → σ. Für σ ≠ τ ist jedoch

y : τ ⊢ / λy.y : σ →σ, obwohl λx.x =_{α} λy.y.

In etwas abgeschwächter Form gilt:

Lemma 2.15 Sei Γ eine Basis, τ ∈ F und s, t ∈ Λ mit s =_{α} t, wobei keine Variable sowohl in s als auch in t gebunden ist. Enthält Γ keine der in s gebundenen Variablen und gilt Γ ⊢ t : τ, dann auch Γ ⊢ s : τ.

Beweis: Induktion über den Termaufbau von t:

• t = x ∈ X:

Dieser Fall ist trivial, da t keine gebundenen Variablen enthält.

• t = t_{1}t_{2}:

Nach dem Erzeugungslemma 2.11 gibt es ein τ_{1} ∈ F mit Γ ⊢ t_{1} : τ_{1} → τ und

Γ ⊢ t_{2} : τ_{1}. Wegen t_{1}t_{2} =_{α} s gibt es s_{1}, s_{2} ∈ Λ mit s = s_{1}s_{2}, t_{1} =_{α} s_{1} und t_{2} =_{α} s_{2},

wobei Γ nach Voraussetzung keine der in s_{1} oder s_{2} gebundenen Variablen enthält. Nach Induktionsannahme gilt also Γ ⊢ s_{1} : τ_{1} → τ und Γ ⊢ s_{2} : τ_{1}, mit (App) folgt Γ ⊢ s : τ.

• t = λx.t_{1}:

Nach dem Erzeugungslemma 2.11 gibt es τ_{1}, τ_{2} ∈ F mit τ ≈ τ_{2} → τ_{1} und Γ, x : τ_{2} ⊢ t_{1} : τ_{1}. Wegen s =_{α} t gibt es ein s_{1} ∈ Λ mit s = λy.s_{1} und s_{1} =_{α} t_{1}[y/x], wobei y weder in Γ noch in t_{1} vorkommt (für y = x folgt die Behauptung direkt aus der Induktionsannahme). Ersetzt man in der Herleitung von Γ, x : τ_{2} ⊢ t_{1} : τ_{1} jede vorkommende Basis Γ′ durch Γ′ ∪ {(y : τ_{2})}, so erhält man Γ, x : τ_{2}, y : τ_{2} ⊢ t_{1} : τ_{1}. Nach dem Substitutionslemma 2.14 ist Γ, y : τ_{2} ⊢ t_{1}[y/x] : τ_{1} und nach Induktionsannahme auch Γ, y : τ_{2} ⊢ s_{1}[y/x] : τ_{1}. Anwenden von (Abs) und (Kon) liefert Γ ⊢ s : τ.

□

Nicht alle Kongruenzen auf freien Gruppoiden eignen sich als Typsysteme. Im allgemeinen gilt nämlich nicht, daß aus Γ ⊢ (λx.s)t : τ auch schon Γ ⊢ s[t/x] : τ folgt. Dies soll jetzt genauer untersucht werden.

Definition 2.16 Der bezüglich (\underline{F}, ≈) getypte λ_{(\underline{F},≈)}-Kalkül heißt β-typtreu, falls für eine Basis Γ und für alle τ ∈ F und s, t ∈ Λ mit s [figure: β] t gilt:

Γ ⊢ s : τ ⇒ Γ ⊢ t : τ

Satz 2.17 a) Erfüllt \underline{F} die Kürzungsregel

(K) Für alle σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F gilt: σ_{1} → τ_{1} ≈ σ_{2} → τ_{2} ⇒ σ_{1} ≈ σ_{2} und τ_{1} ≈ τ_{2},

so ist der λ_{(\underline{F},≈)}-Kalkül β-typtreu. b) Ist der λ_{(\underline{F},≈)}-Kalkül β-typtreu, so erfüllt (\underline{F}, ≈) die Regel:

(L) Für alle σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F gilt: σ_{1} → τ_{1} ≈ σ_{2} → τ_{2} ⇒ τ_{1} ≈ τ_{2}.

Beweis:

a) Wir zeigen: Γ ⊢ (λx.t)s : τ ⇒ Γ ⊢ t[s/x] : τ. Daraus folgt die Behauptung. Nach dem Erzeugungslemma 2.11 folgt aus Γ ⊢ (λx.t)s : τ, daß es ein σ ∈ F gibt mit Γ ⊢ λx.t : σ → τ und Γ ⊢ s : σ. Nochmalige Anwendung des Erzeugungslemmas 2.11 liefert σ_{1}, τ_{1} ∈ F mit σ → τ ≈ σ_{1} → τ_{1} und Γ, x : σ_{1} ⊢ t : τ_{1}. Nach Voraussetzung ist σ ≈ σ_{1} und τ ≈ τ_{1}. Mit (Kon) gilt Γ ⊢ s : σ_{1} und Γ, x : σ_{1} ⊢ t : τ und mit dem Substitutionslemma 2.14 folgt Γ ⊢ t[s/x] : τ.

b) Sei σ_{1} → τ_{1} ≈ σ_{2} → τ_{2} für σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F. Dann gibt es mit x, y, z ∈ X eine Herleitung:

\overline{(Var)} ; x : σ_{1}, y : τ_{1}, z : σ_{2} ⊢ y : τ_{1}

\overline{(Abs)}

y : τ_{1}, z : σ_{2} ⊢ λx.y : σ_{1} → τ_{1}

\overline{(Kon)}

y : τ_{1}, z : σ_{2} ⊢ λx.y : σ_{2} → τ_{2}

\overline{(Var)} y : τ_{1}, z : σ_{2} ⊢ z : σ_{2}
\overline{(App)}
y : τ_{1}, z : σ_{2} ⊢ (λx.y)z : τ_{2}

Da der λ_{(\underline{F},≈)}-Kalkül als β-typtreu angenommen wurde, gilt wegen y = y[z/x] auch y : τ_{1}, z : σ_{2} ⊢ y : τ_{2}. Folglich ist τ_{1} ≈ τ_{2}.

□

Wir haben gezeigt, daß (K) ein hinreichendes und (L) ein notwendiges Kriterium für β-Typtreue sind. Daß (L) nicht hinreichend ist, zeigt folgendes Beispiel:

Beispiel: Sei J = {ι_{n} | n ∈ ℕ} eine Menge von Grundtypen. Durch

ι_{m} → ι_{n} ∼ \{ \begin{matrix}ι_{n} & falls n = 0 \\ ι_{n+1} & sonst. \end{matrix}

sei auf dem frei erzeugten Gruppoid \underline{F}_{J} eine Relation definiert. Für σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} folgt dann aus σ_{1} →τ_{1} ≈ σ_{2} →τ_{2} auch τ_{1} ≈ τ_{2}. Folgendes ist eine korrekte Herleitung:

\overline{(Var)} ; x : ι_{0}, y : ι_{1} ⊢ x : ι_{0} ; \overline{(Kon)} ; x : ι_{0}, y : ι_{1} ⊢ x : ι_{0} → ι_{0} \overline{(Var)} ; x : ι_{0}, y : ι_{1} ⊢ x : ι_{0}
\overline{(App)}

x : ι_{0}, y : ι_{1} ⊢ xx : ι_{0}

\overline{(Abs)}

y : ι_{1} ⊢ λx.xx : ι_{0} → ι_{0}

\overline{(Kon)}

y : ι_{1} ⊢ λx.xx : ι_{1} → ι_{0} \overline{(Var)} y : ι_{1} ⊢ y : ι_{1}

\overline{(App)}
y : ι_{1} ⊢ (λx.xx)y : ι_{0}

Wäre auch y : ι_{1} ⊢ yy : ι_{0}, so gäbe es nach dem Erzeugungslemma 2.11 ein τ ∈ F_{J} mit y : ι_{1} ⊢ y : τ → ι_{0} und y : ι_{1} ⊢ y : τ. Damit wäre ι_{1} ≈ τ → ι_{0} und ι_{1} ≈ τ, also auch ι_{1} ≈ ι_{1} →ι_{0}. In \underline{F}_{J} ist jedoch ι_{1} ≈ / ι_{1} →ι_{0}, der λ_{(\underline{F}_{J} ,≈)}-Kalkül ist also nicht β-typtreu.

Keine Probleme gibt es für die η-Reduktion:

Definition 2.18 Der bezüglich (\underline{F}, ≈)-getypte λ_{(\underline{F},≈)}-Kalkül heißt η-typtreu, falls für eine Basis Γ und für alle τ ∈ F und s, t ∈ Λ mit s _{η}^{}t gilt:

Γ ⊢ s : τ ⇒ Γ ⊢ t : τ.

Satz 2.19 Für jedes Typsystem (\underline{F}, ≈) ist der λ_{(\underline{F},≈)}-Kalkül η-typtreu.

Beweis: Gelte Γ ⊢ λx.tx : τ für ein t ∈ Λ mit x ∉ FV(t). Dann gibt es nach dem Erzeugungslemma 2.11 τ_{1}, τ_{2} ∈ F mit τ ≈ τ_{2} → τ_{1} und Γ, x : τ_{2} ⊢ tx : τ_{1}. Erneut nach dem Erzeugungslemma 2.11 gibt es ein σ ∈ F mit Γ, x : τ_{2} ⊢ t : σ → τ_{1} und Γ, x : τ_{2} ⊢ x : σ, also σ ≈ τ_{2}. Nach Voraussetzung ist x ∉ FV(t), es folgt mit dem Basislemma 2.12 Γ ⊢ t : σ → τ_{1} und wegen τ ≈ τ_{2} → τ_{1} ≈ σ → τ_{1} mit (Kon) auch Γ ⊢ t : τ. □

Da also jeder λ_{(\underline{F},≈)}-Kalkül η-typtreu ist, werden wir statt β-typtreu einfach nur typtreu schreiben. Typsysteme, die die Regel (K) erfüllen, nennen wir K-Typsysteme. Viele Eigenschaften des ungetypten λ-Kalkül übertragen sich auf den λ_{(\underline{F},≈)}-Kalkül. Insbesondere gilt:

Satz 2.20 (Church-Rosser) Sei (\underline{F}, ≈) ein K-Typsystem. Dann ist die β- bzw. βη- Reduktion im λ_{(\underline{F},≈)}-Kalkül konfluent, es gilt also:

Γ ⊢ s : τ, s [figure: βη] t_{1}, s [figure: βη] t_{2} ⇒ es existiert ein u ∈ Λ mit Γ ⊢ u : t
und t_{1} [figure: βη] u, t_{2} [figure: βη] u.

(Entsprechend für [figure: β] ).

s : τ
[figure: βη; βη]
t_{1} : τ  t_{2} : τ
[figure: ..............; βη; ..............; βη]
u : τ

Beweis: Aus Γ ⊢ s : τ, s [figure: βη] t_{1}, s [figure: βη] t_{2} folgt mit Satz 2.17 und Satz 2.19 bereits Γ ⊢ t_{1} : τ und Γ ⊢ t_{2} : τ. Nach Satz 1.9 gibt es ein u ∈ Λ mit t_{1} [figure: βη] u und t_{2} [figure: βη] u, erneut aus Satz 2.17 und Satz 2.19 folgt Γ ⊢ u : τ. Für die β-Reduktion verläuft der Beweis analog. □

Dieser Beweis funktioniert nicht für den Church-Style. Natürlich gilt auch hier der Satz von Church-Rosser, obige Argumentation scheitert jedoch, siehe [MS95].

Wir werden nun untersuchen, welche Typsysteme K-Typsysteme sind. Man sieht leicht ein, daß es keine nichttrivialen endlichen K-Typsysteme gibt:

Lemma 2.21 Die Anzahl der Kongruenzklassen eines Typsystems (\underline{F}, ≈) ist 0, 1 oder unendlich.

Beweis: Sei T = \{τ_{1}, …, τ_{n}\} mit n > 1 die Trägermenge eines Gruppoids \underline{T} = (T , →). Da es n^{2} > n Möglichkeiten gibt, zwei Elemente aus T mit → zu verknüpfen, gibt es i_{0}, i_{1}, i_{2}, j_{1}, j_{2} ∈ {1, …, n}, so daß τ_{i_{0}} = τ_{i_{1}} → τ_{i_{2}} = τ_{j_{1}} → τ_{j_{2}} mit i_{1} ≠ j_{1} oder i_{2} ≠ j_{2}.

→ τ_{1}  ….  τ_{i_{2}}  ….  τ_{j_{2}}  ….  τ_{n}
τ_{1}  ⋮  ⋮
⋮  ⋮  ⋮
τ_{i_{1}} . . . . . . . .  τ_{i_{0}}  . . . . . . . . . . . . . . . .
⋮  ⋮  ⋮
τ_{j_{1}} . . . . . . . . . . . . . . . .  τ_{i_{0}}  . . . . . . . .
⋮  ⋮  ⋮
τ_{n}  ⋮  ⋮

Betrachtet man das freie Gruppoid \underline{F}_{T} mit der entsprechenden Kongruenz ≈, so erfüllt dieses die Kürzungsregel (K) nicht, (\underline{F}_{T} , ≈) ist daher kein K-Typsystem. Daraus folgt die Behauptung. □

Da das leere Gruppoid keine getypten λ-Terme erzeugt und der mit dem trivialen Typsystem (\underline{F}, ∇) getypte λ-Kalkül gerade dem ungetypten λ-Kalkül entspricht, folgt aus Lemma 2.21, daß jedes nichttriviale K-Typsystem bereits unendlich viele Klassen von Typen besitzt. Wählt man das freie Gruppoid \underline{F}_{J} mit der trivialen Kongruenz Δ als Typsystem für den λ-Kalkül, so erhält man den einfach getypten λ-Kalkül λ_{→} mit J als der Menge der Grundtypen. Da in diesem Fall die Kürzungsregel (K) trivialerweise erfüllt ist, ist λ_{→} nach Satz 2.17 typtreu.

Für eine Charakterisierung der K-Typsysteme ist folgendes Lemma aus der Allgemeinen Algebra hilfreich:

Lemma 2.22 Sei \underline{F}_{J} ein freies Gruppoid mit einer Relation ∼. Genau dann gilt σ ≈ τ, wenn man τ aus σ durch sukzessives Ersetzen einzelner Vorkommen von Teiltypen δ durch δ′ mit δ ∼ δ′ oder δ′ ∼ δ erhält.

Beweis: Sei τ′ derjenige Typ, der durch Ersetzen eines Vorkommens eines Teiltyps δ durch δ′ mit δ ∼ δ′ oder δ′ ∼ δ aus τ entsteht. Wir zeigen τ ≈ τ′, daraus folgt mit der Transitivität (Regel (t)) die Behauptung.

• τ ∈ J:

Da δ ein Teiltyp von τ ist, ist τ = δ. Dann gilt wegen δ ∼ δ′ oder δ′ ∼ δ mit Regel (c) und gegebenenfalls Regel (s) τ ≈ δ′.

• τ = τ_{1} →τ_{2}:

Im Fall δ = τ folgt die Behauptung wie oben. Andernfalls sei das Vorkommen von δ in τ, welches durch δ′ ersetzt wird, o.B.d.A. ein Teiltyp von τ_{1}. Nach Induktionsannahme erhält man aus τ_{1} dadurch ein σ_{1} mit τ_{1} ≈ σ_{1}. Mit den Regeln (r) und (v) gibt es eine Herleitung:

\begin{matrix}· \\ · \\ · \end{matrix} ; τ_{1} ≈ σ_{1}  \overline{(r)} ; τ_{2} ≈ τ_{2}
\overline{(v)}
τ_{1} → τ_{2} ≈ σ_{1} → τ_{2}

Sei umgekehrt σ ≈ τ. Wir beweisen die Aussage mit Induktion über den Aufbau der Herleitung von σ ≈ τ.

• (c) und (r): Trivial.

• (s): Gelte die Behauptung für τ ≈ σ. Nach Induktionsannahme erhält man σ durch eine Folge von Ersetzungen von Vorkommen von δ in τ durch δ′ mit δ ∼ δ′ oder δ′ ∼ δ. Führt man diese Ersetzungen in umgekehrter Reihenfolge mit σ beginnend durch, so erhält man τ.

• (t): Gelte die Behauptung für σ ≈ ρ und ρ ≈ τ. Nach Induktionsannahme erhält man ρ durch eine Folge von Ersetzungen aus σ und τ durch eine andere Ersetzungsfolge aus ρ. Führt man diese Ersetzungen nacheinander durch, so erhält τ aus σ.

• (v): Sei τ = τ_{1} → τ_{2}, σ = σ_{1} → σ_{2} und gelte die Behauptung für σ_{1} ≈ τ_{1} und σ_{2} ≈ τ_{2}. Nach Induktionsannahme erhält man τ_{1} durch eine Folge von Ersetzungen aus σ_{1} und τ_{2} aus σ_{2}. Ähnlich wie bei (t) erhält man τ_{1} → τ_{2} aus σ_{1} →σ_{2}, indem man diese Ersetzungen nacheinander durchführt.

□

Folgendes Beispiel veranschaulicht dieses Verfahren:

Beispiel: Sei J = {σ, τ, ρ} mit σ ∼ ρ → σ → τ, τ ∼ σ und ρ ∼ τ → σ. Dann gibt es eine Herleitung für (σ →ρ→σ →τ)→ τ ∼ ρ→σ:

\overline{(c)} ; ρ ≈ τ →σ \overline{(c)} ; τ ≈ σ \overline{(c)} ; σ ≈ ρ→σ →τ ; \overline{(v)} ; τ →σ ≈ σ →ρ→σ →τ ; \overline{(t)} ; ρ ≈ σ →ρ→σ →τ  \overline{(c)} ; τ ≈ σ ; \overline{(s)} ; σ ≈ τ
\overline{(v)}
ρ→σ ≈ (σ →ρ→σ →τ)→ τ
\overline{(s)}
(σ →ρ→σ →τ)→ τ ≈ ρ→σ

Über folgende Zwischenschritte erhält man ρ → σ aus (σ → ρ → σ → τ) → τ, die zu ersetzenden Teiltypen sind unterstrichen:

(σ →ρ→σ →τ)→\underline{τ} ⇝ (σ →\underline{ρ→σ →τ)}→σ
⇝ (\underline{σ} →σ)→σ
⇝ (\underline{τ →σ)}→σ
⇝ ρ→σ

Satz 2.23 Sei (\underline{F}_{J} , ≈) ein von einer symmetrischen Relation ∼ erzeugtes Typsystem. Genau dann ist (\underline{F}_{J} , ≈) ein K-Typsystem, wenn für alle σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} und ι_{1}, …, ι_{n} ∈ J mit σ_{1} →τ_{1} ∼ ι_{1} ∼ … ∼ ι_{n} ∼ σ_{2} →τ_{2} gilt: σ_{1} ≈ σ_{2} und τ_{1} ≈ τ_{2}.

Beweis: Für jedes K-Typsystem folgt aus σ_{1} → τ_{1} ∼ ι_{1} ∼ … ∼ ι_{n} ∼ σ_{2} → τ_{2} mit σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} und ι_{1}, …, ι_{n} ∈ J auch σ_{1} ≈ σ_{2} und τ_{1} ≈ τ_{2}. Zum Beweis der Umkehrung seien wieder σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ F_{J} mit σ_{1} →τ_{1} ≈ σ_{2} →τ_{2}, wir zeigen σ_{1} ≈ σ_{2} und τ_{1} ≈ τ_{2}. Nach Lemma 2.22 erhält man σ_{2} → τ_{2} durch sukzessives Ersetzen von Vorkommen von Teiltypen δ in σ_{1} →τ_{1} durch δ′ mit δ ∼ δ′. Ein Teiltyp δ von σ_{1} →τ_{1} ist entweder bereits ein Teiltyp von σ_{1} oder τ_{1} oder eben σ_{1} →τ_{1} selbst. Sei zunächst δ ein Teiltyp von σ_{1}. Durch Ersetzen erhält man ein σ′_{1} ∈ F_{J} mit σ_{1} ≈ σ′_{1}. Ist δ ein Teiltyp von τ_{1}, so erhält man analog ein τ′_{1} ∈ F_{J} mit τ_{1} ≈ τ′_{1}. Erhält man σ_{2} →τ_{2} also nur durch Ersetzungen echter Teiltypen, so gilt σ_{1} ≈ σ_{2} und τ_{1} ≈ τ_{2}. Da außerdem für jede Teilfolge σ′_{1} → τ′_{1} ⇝ ι_{1} ⇝ … ⇝ ι_{n} ⇝ σ′_{2} → τ′_{2} der Ersetzungsfolge mit ι_{1}, …, ι_{n} ∈ J nach Voraussetzung σ′_{1} ≈ σ′_{2} und τ′_{1} ≈ τ′_{2} gilt (wobei ι_{1} ⇝ … ⇝ ι_{n} auch leer sein darf), folgt σ_{1} ≈ σ_{2} und τ_{1} ≈ τ_{2}. □

Eine besondere Rolle unter den Gruppoiden spielen die in gewisser Hinsicht endlich erzeugten. Diese werden in der folgenden Definition präzisiert:

Definition 2.24 Ein Typsystem (\underline{F}_{J} , ≈) heißt endlich repräsentierbar, falls J endlich ist und es eine endliche Relation ∼ gibt, so daß ≈ die von ∼ erzeugte Kongruenz ist.

Für ein beliebiges endlich repräsentierbares Typsystem ist es entscheidbar, ob die Kürzungsregel (K) erfüllt ist. Dafür genügt es nach Satz 2.23, die (endliche) Erzeugendenrelation zu untersuchen. Das hierbei entstehende Problem, für zwei gegebene Typen σ und τ zu entscheiden, ob sie zueinander kongruent sind, wird in der Allgemeinen Algebra Wortproblem genannt. Folgender Satz besagt, daß dieses für endlich repräsentierbare Typsysteme entscheidbar ist.

Satz 2.25 Sei \underline{F} ein frei erzeugtes Gruppoid mit einer endlichen binären Relation ∼. Dann gibt es ein Entscheidungsverfahren dafür, ob σ ≈ τ für σ, τ ∈ F gilt.

Beweis: Sei S := {δ ∈ F | ∃δ′ ∈ F : δ ∼ δ′ oder δ′ ∼ δ} ∪ {σ, τ} und T die Menge aller Teiltypen von Elementen aus S. Nach Voraussetzung ist T endlich. Sei ≈′ die kleinste reflexive, symmetrische und transitive Relation auf T , die ∼ enthält und für die für alle σ_{1}, σ_{2}, τ_{1}, τ_{2} ∈ T gilt:

σ_{1} ≈′ τ_{1}, σ_{2} ≈′ τ_{2}, σ_{1} →σ_{2}, τ_{1} →τ_{2} ∈ T  ⇒  σ_{1} →σ_{2} ≈′ τ_{1} →τ_{2}.

Mit T ist auch ≈′ endlich. Gelte σ ≈ τ. Nach Lemma 2.22 gibt es σ_{0}, σ_{1}, …, σ_{n+1} ∈ F mit σ = σ_{0} ≈ σ_{1} ≈ … ≈ σ_{n+1} = τ, wobei σ_{i+1} aus σ_{i} für alle i = 0, …, n durch Ersetzen eines Teiltyps δ durch δ′ in σ_{i} mit δ ∼ δ′ oder δ′ ∼ δ entsteht, wir schreiben σ_{i} ^{}^{1}^{}σ_{i+1}. Mit Induktion über ∑_{i=0}^{n+1} len(σ_{i}) zeigen wir, daß aus σ_{0} ^{}^{1}^{}σ_{1} ^{}^{1}^{}… ^{}^{1}^{}σ_{n+1} mit σ_{0}, σ_{n+1} ∈ T auch σ_{0} ≈′ σ_{n+1} folgt. Falls es ein i = 0, …, n mit σ_{i} ∼ σ_{i+1} oder σ_{i+1} ∼ σ_{i} gibt, so folgt nach Induktionsannahme σ_{0} ≈′ σ_{i} und σ_{i+1} ≈′ σ_{n+1}, also auch σ_{0} ≈′ σ_{n+1}. Andernfalls gibt es für jedes σ_{i} mit i = 0, …, n + 1 zwei Typen φ_{i}, ψ_{i} ∈ F mit σ_{i} = φ_{i} → ψ_{i}. Es folgt φ_{0} ^{}^{1}^{}φ_{1} ^{}^{1}^{}… ^{}^{1}^{}φ_{n+1} und ψ_{0} ^{}^{1}^{}ψ_{1} ^{}^{1}^{}… ^{}^{1}^{}ψ_{n+1}, nach Induktionsannahme gilt φ_{0} ≈′ φ_{n+1} und ψ_{0} ≈′ ψ_{n+1}. Wegen der Verträglichkeit folgt σ = φ_{0} → ψ_{0} ≈′ φ_{n+1} → ψ_{n+1} = τ. Da trivialerweise mit σ ≈′ τ auch σ ≈ τ gilt, ist somit σ ≈′ τ ⇔ σ ≈ τ gezeigt. Aus der Endlichkeit von ≈′ folgt die Behauptung.

□

Folgendes Korollar beschreibt Typsysteme, die durch eine spezielle Relation erzeugt werden. Die Aussage folgt direkt aus Satz 2.23.

Korollar 2.26 Sei \underline{F}_{J} ein freies Gruppoid, zu jedem ι ∈ J gebe es genau ein τ ∈ F_{J} mit ι ∼ τ, wobei keine weiteren Elemente von F_{J} in Relation stehen. Dann ist (\underline{F}_{J} , ≈) ein K-Typsystem.

Die in Korollar 2.26 betrachteten Typsysteme sind nach Satz 2.17 typtreu. Unter den K-Typsystemen spielen sie eine wichtige Rolle: Zu jedem endlich repräsentierbaren K-Typsystem (\underline{F}_{J} , ≈) liefert folgendes Verfahren eine Relation ∼′ auf J × F_{J}, so daß F_{J} faktorisiert nach der davon erzeugten Kongruenzrelation ≈′ isomorph zu F_{J} /_{≈} ist und es zu jedem ι_{i} ∈ J genau ein τ_{i} ∈ F gibt mit ι_{i} ∼′ τ_{i}.

Sei J = {ι_{1}, …, ι_{n}} eine Menge von Grundtypen und ∼ eine endliche binäre Relation auf F_{J}. Zu beachten ist, daß im Algorithmus ∼ nicht die starre Bezeichnung der Startrelation ist, sondern in jedem folgenden Schritt verändert werden kann.

Algorithmus 2.27

(1) (a) Streiche jedes Paar σ ∼ σ mit σ ∈ F.

(b) Ersetze jedes Paar der Form σ → τ ∼ ι mit ι ∈ J, σ, τ ∈ F durch ι ∼ σ →τ.

(c) Falls ι_{i_{1}} ∼ ι_{i_{2}} ∼ … ∼ ι_{i_{n}} ∼ ι_{i_{1}} mit i_{1} < i_{2} < … < i_{n}, so streiche ι_{i_{n}} ∼ ι_{i_{1}}.

(d) Ersetze im Fall ι_{i} ∼ ι_{j} mit i, j = 1, …, n jedes Auftreten von ι_{i} in anderen Paaren von ∼ durch ι_{j}.

(e) Streiche alle mehrfachen Vorkommen von Paaren σ ∼ τ mit σ, τ ∈ F.

(2) Solange es noch Paare der Form σ_{1} → σ_{2} ∼ τ_{1} → τ_{2} gibt, streiche σ_{1} → σ_{2} ∼ τ_{1} →τ_{2}, setze σ_{1} ∼ τ_{1} und σ_{2} ∼ τ_{2} und wiederhole Schritt (1).

(3) Sei F_{i} := |{τ | ι_{i} ∼ τ}|. Solange es noch ein i ∈ {1, …, n} gibt mit F_{i} > 1:

(a) bestimme ein i ∈ {1, …, n} mit F_{i} > 1 und max{len(τ) | ι_{i} ∼ τ} ≥ max{len(τ) | ι_{j} ∼ τ, F_{j} > 1};

(b) bestimme ein φ = σ_{φ} → τ_{φ} mit ι_{i} ∼ φ und len(φ) ≥ len(τ) für alle τ mit ι_{i} ∼ τ;

(c) bestimme ein ψ = σ_{ψ} →τ_{ψ} mit ι_{i} ∼ ψ und φ ≠ ψ;

(d) streiche ι_{i} ∼ φ und setze φ ∼ ψ;

(e) wiederhole Schritt (2).

(4) Für alle i ∈ {1, …, n}, für die es keinen Typen τ mit ι_{j} ∼ τ gibt, setze ι_{i} ∼ ι_{i}. ∼′ sei die zuletzt entstandene Relation ∼.

Nach Voraussetzung von Schritt (3) existiert ein i ∈ {1, …, n}, so daß F_{i} > 1. Die vorkommenden Maxima existieren, da die Relation ∼ zu jedem Zeitpunkt des Ablaufs endlich ist. Hätte in Schritt (3b) φ nicht die Form φ = σ_{φ} → τ_{φ}, gäbe es wegen F_{i} > 1 zwei Paare ι_{i} ∼ ι_{j} und ι_{i} ∼ ι_{k} (j, k ∈ {1, …, n}, j ≠ k). Dies kann aber nicht sein, da zuvor Schritt (1) durchgeführt worden ist. Aus einem ähnlichen Grund hat ψ die Form σ_{ψ} → τ_{ψ}, da es andernfalls Paare ι_{i} ∼ φ und ι_{i} ∼ ι_{j} mit j = 1, …, n gäbe. Somit ist das Verfahren durchführbar.

Zum Nachweis der Korrektheit und der Terminierung von Algorithmus 2.27 brauchen wir noch einige Hilfsmittel:

Definition 2.28 Sei (P, ≤) eine geordnete Menge. (P, ≤) erfüllt die absteigende Kettenbedingung, falls jede Kette p_{0} ≥ p_{1} ≥ p_{2} ≥ … mit p_{n} ∈ P, n ∈ ℕ ein kleinstes Element besitzt. Auf dem Produkt P^{m} mit m ∈ M ist die lexikographische Ordnung ⊑ wie folgt definiert:

(p_{1}, …, p_{m}) ⊑ (q_{1}, …, q_{m}) :⇔ p_{1} = q_{1}, …, p_{m} = q_{m}  oder
∃i = 1, …, m : p_{1} = q_{1}, …, p_{i−1} = q_{i−1}, p_{i} < q_{i}

Lemma 2.29 Sei (P, ≤) eine geordnete Menge, die die absteigende Kettenbedingung erfüllt. Für jede natürliche Zahl m ≥ 1 erfüllt dann auch (P^{m}, ⊑) die absteigende Kettenbedingung.

Beweis: Wir beweisen die Behauptung mit Induktion über m. Der Fall m = 1 ist trivial. Angenommen P^{m} erfüllt die absteigende Kettenbedingung. Würde P × P^{m} eine unendlich absteigende Kette (p_{0}, q_{0}) ⊐ (p_{1}, q_{1}) ⊐ (p_{2}, q_{2}) … enthalten, so gäbe es nach Voraussetzung ein i ∈ ℕ mit p_{j} = p_{i} für alle j ≥ i. Damit wäre q_{i+1} > q_{i+2} > q_{i+3} > … eine unendlich absteigende Kette in P^{m}, ein Widerspruch. Wegen P^{m+1} ≅ P × P^{m} erfüllt also auch P^{m+1} die absteigende Kettenbedingung. □

Satz 2.30 Algorithmus 2.27 terminiert und ist korrekt.

Beweis: Wir zeigen zunächst die Terminierung. Da ∼ zu jedem Zeitpunkt aus endlich vielen Paaren von Typen endlicher Länge besteht, terminieren die Schritte (1) und (2). Sei l := max{len(τ) | ∃σ ∈ F_{J} : σ ∼ τ oder τ ∼ σ} die maximale Länge aller zu Beginn des Algorithmus in ∼ vorkommenden Typen. Für alle k = 2, …, l sei

m_{k} := |{τ ∈ F_{J} | len(τ) ≥ k und es ex. ein i = 1, …, n mit ι_{i} ∼ τ oder τ ∼ ι_{i}}|.

Wir zeigen, daß m := (m_{l}, m_{l−1}, …, m_{2}) ∈ ℕ^{l−1} mit jedem Durchlaufen der Schritte (3a) bis (3e) bezüglich der lexikographischen Ordnung kleiner wird. Die Schritte (3a) bis (3c) terminieren immer, haben jedoch keinen Einfluß auf m. (3d) erhöht m_{len(ψ)} um eins und läßt m ansonsten unverändert. In Schritt (3e) werden m_{len(φ)} und m_{len(ψ)} reduziert, damit wird insgesamt auch m kleiner. Nach Lemma 2.29 erfüllt ℕ^{l−1} die absteigende Kettenbedingung, m kann also nicht unendlich oft vermindert werden. Da aber m bei jedem Durchlauf von (3a) bis (3e) verringert wird, terminiert Schritt (3). Es ist klar, daß auch Schritt (4) terminiert.

Nun kommen wir zum Beweis der Korrektheit. Wir zeigen zunächst, daß keiner der Schritte (1) bis (4) die von ∼ erzeugte Kongruenz ≈ verändert:

• Schritt (1): Wegen Regel (r) ist Teil (a) völlig unproblematisch. Das Ersetzen von Paaren der Gestalt σ → τ ∼ ι durch ι ∼ σ → τ in Schritt ändert wegen Regel (s) sicherlich auch nichts an der erzeugten Kongruenz. Wegen Regel (t) hat in Teil (c) das Streichen von ι_{i_{n}} ∼ ι_{i_{1}} keine Konsequenzen. Aus Regel (v) folgt mit Induktion über den Aufbau von τ, daß auch das Ersetzen von ι_{i} durch ι_{j} in τ mit ι_{i} ∼ ι_{j} die erzeugte Kongruenz nicht verändert.

• Schritt(2): Mit den Regeln (K) und (v) ist σ_{1} →σ_{2} ≈ τ_{1} →τ_{2} genau dann, wenn σ_{1} ≈ τ_{1} und σ_{2} ≈ τ_{2} gelten. Daraus folgt die Behauptung.

• Schritt(3): Unter der Annahme ι ≈ ψ gilt mit den Regeln (s) und (t) auch sicherlich ι ≈ φ genau dann, wenn φ ≈ ψ gilt. Daraus folgt die Behauptung.

• Schritt (4): Wegen der Regel (r) macht auch dieser Fall keine Probleme. Da nach Beendigung des Algorithmus F_{i} = 1 für alle i = 1, …, n gilt, hat die Relation ∼′ gerade die gewünschte Form. Wegen obigen Überlegungen ist \underline{F}_{J} /_{≈} ≅ \underline{F}_{J} /_{≈′}. □

Diesen Algorithmus wollen wir an einem Beispiel veranschaulichen: Beispiel: Sei J = {ι_{1}, ι_{2}, ι_{3}, ι_{4}, ι_{5}} und ∼ wie folgt definiert:

ι_{2} ∼ ι_{5}
ι_{1} →ι_{2} ∼ (ι_{2} →ι_{1})→ι_{3} →ι_{5}
ι_{1} →ι_{4} ∼ ι_{4}
ι_{3} →ι_{3} ∼ ι_{3} →ι_{3}
ι_{2} →((ι_{1} →ι_{4})→ι_{3})→ι_{1} →ι_{4} ∼ ι_{2} →ι_{3} →ι_{4}
ι_{5} ∼ ι_{2}
(ι_{2} →ι_{4})→ι_{1} ∼ ((ι_{3} →ι_{5})→(ι_{2} →ι_{1})→ι_{4})→ι_{5} →ι_{1}
ι_{3} →ι_{2} ∼ (ι_{4} →ι_{3})→ι_{2}

Schritt (1) von Algorithmus 2.27 formt diese Relation um in:

ι_{2} ∼ ι_{5}
ι_{1} →ι_{5} ∼ (ι_{5} →ι_{1})→ι_{3} →ι_{5}
ι_{4} ∼ ι_{1} →ι_{4}
ι_{5} →((ι_{1} →ι_{4})→ι_{3})→ι_{1} →ι_{4} ∼ ι_{5} →ι_{3} →ι_{4}
(ι_{5} →ι_{4})→ι_{1} ∼ ((ι_{3} →ι_{5})→(ι_{5} →ι_{1})→ι_{4})→ι_{5} →ι_{1}
ι_{3} →ι_{5} ∼ (ι_{4} →ι_{3})→ι_{5}

Schritt (2) liefert:

ι_{2} ∼ ι_{5}
ι_{1} ∼ ι_{5} →ι_{1}
ι_{5} ∼ ι_{3} →ι_{5}
ι_{4} ∼ ι_{1} →ι_{4}
ι_{3} ∼ (ι_{1} →ι_{4})→ι_{3}
ι_{4} ∼ (ι_{5} →ι_{1})→ι_{4}
ι_{3} ∼ ι_{4} →ι_{3}

Die Schritte (a) bis (d) des ersten Durchlaufs von Schritt (3) bewirken lediglich, daß ι_{3} ∼ (ι_{1} → ι_{4}) → ι_{3} durch (ι_{1} → ι_{4}) → ι_{3} ∼ ι_{4} → ι_{3} ersetzt wird. Nach Schritt (3e) erhält man:

ι_{2} ∼ ι_{5}
ι_{1} ∼ ι_{5} →ι_{1}
ι_{5} ∼ ι_{3} →ι_{5}
ι_{4} ∼ ι_{1} →ι_{4}
ι_{4} ∼ (ι_{5} →ι_{1})→ι_{4}
ι_{3} ∼ ι_{4} →ι_{3}

Nach einem zweiten Durchlauf endet der Algorithmus schließlich nach Schritt (4) mit:

ι_{1} ∼′ ι_{5} →ι_{1}
ι_{2} ∼′ ι_{5}
ι_{3} ∼′ ι_{4} →ι_{3}
ι_{4} ∼′ ι_{1} →ι_{4}
ι_{5} ∼′ ι_{3} →ι_{5}

Algorithmus 2.27 liefert einen konstruktiven Beweis für die Umkehrung von Korollar 2.26 im Falle endlich repräsentierbarer Typsysteme. Dies wird durch folgendes Korollar ausgedrückt:

Korollar 2.31 Jedes endlich repräsentierbare K-Typsystem ist zu einem von einer Relation \{ι_{i} ∼ τ_{i} | i = 1, …, n, ι_{i} ∈ J, τ_{i} ∈ F_{J} \} erzeugten Typsystem (\underline{F}_{J} , ≈) isomorph.

3 Starke Normalisierbarkeit monomorph getypter λ-Terme

In der Funktionalen Programmierung betrachtet man λ-Terme als Programme, die zu gewissen Eingaben entsprechende Ausgaben liefern. Die Berechnung der Ausgaben vollzieht sich im λ-Kalkül durch β- bzw. βη-Reduktionen. Dies legt es nahe, den Begriff der Normalform einzuführen, mit dem Endergebnisse von β- bzw. βη-Reduktionen bezeichnet werden. Aber auch aus mathematischer Sicht ist dieser Begriff von Interesse: Normalformen sind kanonische Repräsentanten der β- bzw. βη-Äquivalenzklassen von λ-Termen. In diesem Kapitel soll untersucht werden, bezüglich welcher monomorphen Typsysteme β- und βη-Reduktionen von λ-Termen stets terminieren.

Definition 3.1 Ein λ-Term ist in β-Normalform, falls er keinen β-Redex enthält. Entsprechend ist ein λ-Term in η-Normalform bzw. in βη-Normalform, falls er keinen η- bzw. βη-Redex enthält.

Jeder λ-Term läßt sich durch eine endliche Folge von η-Reduktionen in η-Normalform überführen, da jede η-Reduktion die Länge des Terms verkürzt. Somit hat jeder λ-Term, der eine β-Normalform besitzt, auch eine βη-Normalform. Im folgenden sei daher mit Normalform stets βη-Normalform gemeint.

Definition 3.2 Ein λ-Term t heißt normalisierbar, falls es einen λ-Term s in Normalform gibt mit t [figure: βη] s. Falls jede Folge von Reduktionen in t terminiert, heißt t stark normalisierend. Der bezüglich (\underline{F}, ≈) getypte λ_{(\underline{F},≈)}-Kalkül heißt stark normalisierend, falls alle mit (\underline{F}, ≈) typisierbaren λ-Terme stark normalisierend sind.

Natürlich ist jeder stark normalisierende λ-Term auch normalisierbar.

Beispiel:

a) (λxyz.xz(yz))(λxy.x) ist stark normalisierend:

(λxyz.xz(yz))(λxy.x) _{β}^{}λyz.(λxy.x)z(yz) [figure: β] λyz.z

Dies ist die einzig mögliche Folge von Reduzierungen. b) Ω := (λx.xx)(λx.xx) ist nicht normalisierbar:

Ω [figure: β] Ω [figure: β] Ω [figure: β] ….

c) (λxy.y)Ω(λz.z) ist normalisierbar, aber nicht stark normalisierend:

(λxy.y)Ω(λz.z)
[figure: β; β]
(λy.y)(λz.z)  (λxy.y)Ω(λz.z)
[figure: β; β; β]
λz.z  (λy.y)(λz.z)  (λxy.y)Ω(λz.z)
[figure: β; β; β]
λz.z  (λy.y)(λz.z)  (λxy.y)Ω(λz.z)
.............  .............  .............

Die Forderung, daß syntaktisch korrekte funktionale Programme stets terminieren, findet sich im λ-Kalkül in der starken Normalisierbarkeit wieder. Ziel ist es, eine möglichst allgemeine Charakterisierung derjenigen Typsysteme zu finden, die starke Normalisierbarkeit garantieren. Vorher benötigen wir jedoch noch einige Definitionen. Wie in Kapitel 2 betrachten wir Typsysteme der Form (\underline{F}_{J} , ≈).

Definition 3.3 Zu einem Typ τ ∈ F betrachten wir die induktiv definierten Mengen Pos(τ) und Neg(τ). Für Grundtypen ι ∈ J ist

Pos(ι) = {ι}
Neg(ι) = o /

und für Funktionentypen σ →τ gilt:

Pos(σ →τ) = {σ →τ} ∪ Neg(σ) ∪ Pos(τ)
Neg(σ →τ) = Pos(σ) ∪ Neg(τ)

σ kommt positiv in τ vor, falls σ ∈ Pos(τ); analog tritt σ negativ in τ auf, falls σ ∈ Neg(τ).

Man kann Positivität auch anders verstehen, wenn man Typen als binäre Bäume betrachtet:

Definition 3.4 Sei J die Erzeugendenmenge von \underline{F} und τ ∈ F. Der Typbaum T(τ) ist induktiv definiert durch:

T(τ) = τ für τ ∈ J

T(τ) = [figure: →; T(τ_{1})  T(τ_{2})] für τ = τ_{1} → τ_{2}

Der oberste Pfeil eines Typbaums heißt Wurzel.

Damit wird jedem Typ eineindeutig ein Typbaum zugeordnet.

Lemma 3.5 Ein Vorkommen eines Teiltyps σ eines Typs τ ∈ F ist genau dann positiv, falls im Kantenzug von T(σ) zur Wurzel im Typbaum T(τ) die Anzahl der Kanten von links unten nach rechts oben gerade ist.

Beweis: Der Beweis verläuft mit Induktion über den Typaufbau von τ. □

Beispiel: Der Typbaum von τ = ((σ →ρ)→(φ→ψ))→θ ist:

→

[figure]
→  θ
[figure]
→  →
[figure]
σ  ρ  φ  ψ

Daher sind ρ, φ, θ und σ →ρ genau die positiv auftretenden Teiltypen von τ.

Definition 3.6 Eine Relation ∼ heißt negativ, falls es σ, τ ∈ F_{J} mit σ ≈ τ derart gibt, daß σ negativ in τ auftritt. Andernfalls heißt ∼ positiv.

Nun sind wir in der Lage, ein notwendiges Kriterium für die starke Normalisierbarkeit des bezüglich (\underline{F}, ≈) getypten λ-Kalküls zu formulieren:

Satz 3.7 Ist für ein Typsystem (\underline{F}, ≈) der λ_{(\underline{F},≈)}-Kalkül stark normalisierend, so ist die Relation ≈ positiv.

Beweis: Wir nehmen an, es gibt σ, τ ∈ F mit σ ≈ τ, wobei σ negativ in τ auftritt. Daraus konstruieren wir einen nicht stark normalisierenden λ_{(\underline{F},≈)}-Term.

Da σ negativ in τ auftritt, ist nach Lemma 3.5 im Typbaum T(τ) die Anzahl der Kanten von links unten nach rechts oben im Kantenzug von T(σ) zur Wurzel ungerade. Damit steht rechts von σ eine ungerade Anzahl von Typen σ_{i}, die ihrerseits wieder in mehrere Teiltypen zerfallen können. Unter Berücksichtigung der Typen links von σ, läßt sich τ also darstellen als

τ = τ_{2k+1} = ρ_{2k+1}^{1} → … → ρ_{2k+1}^{n_{2k+1}} → τ_{2k} → σ_{2k+1}

mit

τ_{2k} = ρ_{2k}^{1} → … → ρ_{2k}^{n_{2k}} → τ_{2k−1} → σ_{2k},
⋮
τ_{1} = ρ_{1}^{1} → … → ρ_{1}^{n_{1}} → τ_{0} → σ_{1},
τ_{0} = ρ_{0}^{1} → … → ρ_{0}^{n_{0}} → σ.

Zu jedem Typ τ_{i} mit i = 0, …, 2k+1 geben wir einen λ-Term t_{i} an, so daß t_{i} bezüglich einer festen Basis Γ mit τ_{i} typisierbar ist. Daraus wird ein nicht normalisierbarer λ-Term t konstruiert. Setze

t_{0} = λx_{0}^{1}…. x_{0}^{n_{0}}.t_{2k+1}
t_{1} = λx_{1}^{1}…. x_{1}^{n_{1}}y_{0}.v(y_{0}z_{0}^{1} … z_{0}^{n_{0}}z_{2k+1}^{1} … z_{2k+1}^{n_{2k+1}}y_{2k})

und für k > 0:

t_{2} = λx_{2}^{1}…. x_{2}^{n_{2}}y_{1}.w_{1}(y_{1}z_{1}^{1} … z_{1}^{n_{1}}t_{0})
⋮
t_{2k+1} = λx_{2k+1}^{1}…. x_{2k+1}^{n_{2k+1}}y_{2k}.w_{2k}(y_{2k}z_{2k}^{1} … z_{2k}^{n_{2k}}t_{2k−1}).

Dies ist keine zyklische Definition. Jeder λ-Term t_{i} mit i > 1 enthält nur t_{i−2} explizit als Teilterm. Die Definition von t_{0} greift lediglich auf t_{2k+1} zurück, so daß alle oben definierten Terme nur aus Variablen und t_{1} bestehen. Da t_{1} seinerseits nur aus Variablen besteht, wird tatsächlich für jedes i = 0, …, 2k + 1 durch t_{i} ein λ-Term definiert. Setze

t = t_{2k+1}z_{2k+1}^{1} … z_{2k+1}^{n_{2k+1}}t_{2k}.

Da keine der Variablen y_{0}, …, y_{2k−1} in einem der t_{0}, …, t_{2k+1} frei vorkommt, gilt s[t_{i}/y_{i}] = s für jede Substitution s[t_{i}/y_{i}] mit i < 2k. Somit ist t nicht stark normalisierend, denn es gilt:

t [figure: β] w_{2k}(t_{2k}z_{2k}^{1} … z_{2k}^{n_{2k}}(t_{2k−1}[t_{2k}/y_{2k}]))
[figure: β] w_{2k}(w_{2k−1}(t_{2k−1}[t_{2k}/y_{2k}])z_{2k−1}^{1} … z_{2k−1}^{n_{2k−1}}t_{2k−2}))
[figure: β] w_{2k}(w_{2k−1}(w_{2k−2}(t_{2k−2}z_{2k−2}^{1} … z_{2k−2}^{n_{2k−2}}(t_{2k−3}[t_{2k}/y_{2k}]))))
[figure: β] ⋯
[figure: β] w_{2k}(w_{2k−1} … (w_{2}(w_{1}((t_{1}[t_{2k}/y_{2k}])z_{1}^{1} … z_{1}^{n_{1}}t_{0}))) ⋯)
[figure: β] w_{2k}(w_{2k−1} … (w_{2}(w_{1}(v(t_{0}z_{0}^{1} … z_{0}^{n_{0}}z_{2k+1}^{1} … z_{2k+1}^{n_{2}k+1}t_{2k})))) ⋯)
[figure: β] w_{2k}(w_{2k−1} … (w_{2}(w_{1}(v(t_{2k+1}z_{2k+1}^{1} … z_{2k+1}^{n_{2k+1}}t_{2k})))) ⋯),

also

t [figure: β] w_{2k}(w_{2k−1} … (w_{2}(w_{1}(vt))) ⋯).

Jeder der obigen reduzierten λ-Terme hat genau einen Redex, somit ist t nicht normalisierbar und damit auch nicht stark normalisierend. Nichtsdestotrotz ist typisierbar: Sei

Γ := {(v : σ_{2k+1} →σ_{1})} ∪ {(w_{i} : σ_{i} →σ_{i+1}) | i = 1, …, 2k}
∪ {(y_{i} : τ_{i}) | i = 0, …, 2k} ∪ {(z_{i}^{j} : ρ_{i}^{j}) | i = 0, …, 2k + 1, j = 1, …, n_{i}}

und

Γ^{∗} := Γ ∪ {(x_{i}^{j} : ρ_{i}^{j}) | i = 0, …, 2k + 1, j = 1, …, n_{i}}.

Daraus folgt

Γ^{∗} ⊢ y_{0} : ρ_{0}^{1} →…→ρ_{0}^{n_{0}} →σ und Γ^{∗} ⊢ z_{0}^{i} : ρ_{0}^{i}

für i = 1, …, n_{0}. Mehrfaches Anwenden von (App) liefert

Γ^{∗} ⊢ y_{0}z_{0}^{1} … z_{0}^{n_{0}} : σ

und mit (Kon) erhält man

Γ^{∗} ⊢ y_{0}z_{0}^{1} … z_{0}^{n_{0}} : ρ_{2k+1}^{1} → … → ρ_{2k+1}^{n_{2k+1}} → τ_{2k} → σ_{2k+1}.

Wie oben folgt

Γ^{∗} ⊢ y_{0}z_{0}^{1} … z_{0}^{n_{0}}z_{2k+1}^{1} … z_{2k+1}^{n_{2k+1}}y_{2k} : σ_{2k+1}

und weiter

Γ^{∗} ⊢ v(y_{0}z_{0}^{1} … z_{0}^{n_{0}}z_{2k+1}^{1} … z_{2k+1}^{n_{2k+1}}y_{2k}) : σ_{1}.

Mehrfaches Anwenden von (Abs) liefert

Γ ⊢ λx_{1}^{1} … x_{1}^{n_{1}}y_{0}.v(y_{0}z_{0}^{1} … z_{0}^{n_{0}}z_{2k+1}^{1} … z_{2k+1}^{n_{2k+1}}y_{2k}) : ρ_{1}^{1} → … → ρ_{1}^{n_{1}} → τ_{0} → σ_{1},

also Γ ⊢ t_{1} : τ_{1}. Sukzessive erhält man mit analoger Vorgehensweise Γ ⊢ t_{3} : τ_{3}, Γ ⊢ t_{5} : τ_{5}, …, Γ ⊢ t_{2k+1} : τ_{2k+1}, Γ ⊢ t_{0} : τ_{0}, Γ ⊢ t_{2} : τ_{2}, …, Γ ⊢ t_{2k} : τ_{2k}, also Γ ⊢ t_{i} : τ_{i} für alle i = 0, …, 2k + 1. Schließlich folgt Γ ⊢ t : σ_{2k+1}. Damit ist t ein bezüglich (\underline{F}, ≈) typisierbarer λ-Term, der nicht normalisierbar ist; daraus folgt die Behauptung. □

Die Idee dieses Beweises stammt von N. Mendler, siehe [Men91]. Leider schränkt Satz 3.7 die Mächtigkeit monomorpher Typsysteme etwas ein:

Korollar 3.8 Es gibt kein Typsystem (\underline{F}, ≈), so daß die λ_{(\underline{F},≈)}-Terme genau den stark normalisierenden Termen entsprechen.

Beweis: Sicherlich ist t = xx mit x ∈ X stark normalisierend, da t bereits in Normalform ist. Wäre t typisierbar, so gäbe es nach dem Erzeugungslemma 2.11 eine Basis Γ und τ_{1}, τ_{2} ∈ F mit Γ ⊢ x : τ_{1} →τ_{2} und Γ ⊢ x : τ_{1}. Erneut nach 2.11 gibt es ein τ ∈ F mit τ_{1} →τ_{2} ≈ τ ≈ τ_{1}, also τ_{1} →τ_{2} ≈ τ_{1}. Da τ_{1} negativ in τ_{1} →τ_{2} vorkommt, ist der λ_{(\underline{F},≈)}-Kalkül nach Korollar 3.8 nicht stark normalisierend. □

Folgender Satz liefert ein Kriterium für starke Normalisierbarkeit. Nach Korollar 2.31 bedeutet die im Satz gemachte Voraussetzung für endlich repräsentierbare K-Typsysteme keine große Einschränkung.

Satz 3.9 Sei \underline{F}_{J} ein freies Gruppoid, zu jedem ι_{i} ∈ J = \{ι_{i} | i ∈ I\} gebe es genau ein τ_{i} ∈ F_{J} mit ι_{i} ∼ τ_{i}. Ist ∼ positiv, so ist der λ_{(\underline{F},≈)}-Kalkül stark normalisierend.

Beweis: Siehe [Men91]. □

Leider ist es oft nicht offensichtlich, ob eine Relation der Form {ι_{i} ∼ τ_{i} | i ∈ I} auf einem freien Gruppoid \underline{F}_{J} positiv ist. Um ein Kriterium für die Positivität der Relation ∼ zu geben, wollen wir zusätzlich τ_{i} ∉ J für alle i ∈ I fordern. Dies ist keine wesentliche Einschränkung, da es für jedes Gruppoid \underline{F}_{J} /_{≈} eine Menge J′ mit einer Relation ∼′ gibt, so daß \underline{F}_{J} /_{≈} und \underline{F}_{J′}/_{≈′} isomorph sind und ∼′ die obige Voraussetzung erfüllt.

Definition 3.10 Sei ∼ eine Relation auf dem Gruppoid \underline{F}_{J}. Der Typengraph G_{J}^{∼} ist ein mit {−1, 1} bewerteter gerichteter Graph mit der Eckenmenge F_{J} und der wie folgt definierten Kantenmenge:

• σ ^{−1}^{}τ, falls σ negativ in τ vorkommt

• σ ^{1}^{}τ, falls σ ≠ τ und σ positiv in τ vorkommt

• σ ^{}^{1}^{}τ, falls σ ≠ τ und τ dadurch entsteht, daß in σ das Vorkommen eines Teiltyps φ durch ψ ersetzt wird, wobei φ ∼ ψ oder ψ ∼ φ.

Für σ [figure: 1; 1] τ schreiben wir einfach σ ^{}^{1}^{}τ. Der Typengraph von \underline{F}_{J} /_{≈} enthält keine Schleifen τ ^{x}^{}τ (x ∈ {1, −1}) und keine negativ bewerteten Doppelkanten σ [figure: −1; −1] τ.

Sei \underline{F}_{J} ein von J = \{ι_{i} | i ∈ I\} frei erzeugtes Gruppoid und \{ι_{i} ∼ τ_{i} | i ∈ I, ι_{i} ∈ J , τ_{i} ∈ F_{J} \ J } eine Relation. Falls eines der ι_{i} negativ in τ_{i} für i ∈ I vorkommt so ist ∼ offensichtlich negativ. Daher wollen wir voraussetzen, daß ∼ diese Eigenschaft nicht hat.

Sei σ^{k} die Abkürzung für

σ_{k,1} ^{}^{1}^{}σ_{k,2} ^{}^{1}^{}… ^{}^{1}^{}σ_{k,n_{k}}

mit k = 1, …, m. Folgendes Verfahren findet zu einem geschlossenen Kantenzug

K = σ_{1,n_{1}} ^{x_{1}}^{}σ^{2} ^{x_{2}}^{}… ^{x_{m−1}}^{}σ^{m} ^{x_{m}}^{}σ^{1}

mit x_{k} ∈ {−1, 1}, k = 1, …, m, im Typengraph G_{J}^{∼} einen Kantenzug

ι_{i_{1}}  ^{y_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{y_{2}}^{}… ^{}^{1}^{}ι_{i_{n}}  ^{y_{n}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}}

mit ι_{i_{j}} ∈ J und τ_{i_{j}} ∈ F_{J}, j = 1, …, n, so daß x_{1} · . . . · x_{m} = y_{1} · . . . · y_{n}. Die Tatsache, daß in diesem Kantenzug nur Doppelkanten der Form τ ^{}^{1}^{}ι mit τ ∈ F_{J} und ι ∈ J enthalten sind, wird für den Beweis der Gültigkeit des Kriteriums zur Charakterisierung der Positivität entscheidend sein.

Algorithmus 3.11

• Solange K noch Kanten σ ^{}^{1}^{}σ′ mit σ ∼ / σ′ und σ′ ∼ / σ enthält:

(1) Ersetze alle Kanten der Form ι_{i} ^{}^{1}^{}τ_{i} ^{}^{1}^{}ι_{i} durch ι_{i} und alle Kanten der Form τ_{i} ^{}^{1}^{}ι_{i} ^{}^{1}^{}τ_{i} durch τ_{i}.

(2) Falls K einen Kantenzug τ_{i} ^{}^{1}^{}ι_{i} ^{x}^{}σ ^{}^{1}^{}σ′ mit σ′ ∉ J enthält, so gibt es vier mögliche Fälle:

(a) x = 1 und ι_{i} kommt positiv in σ′ vor:

ersetze τ_{i} ^{}^{1}^{}ι_{i} ^{1}^{}σ ^{}^{1}^{}σ′ durch τ_{i} ^{}^{1}^{}ι_{i} ^{1}^{}σ′.

(b) x = −1 und ι_{i} kommt negativ in σ′ vor:

ersetze τ_{i} ^{}^{1}^{}ι_{i} ^{−1}^{}σ ^{}^{1}^{}σ′ durch τ_{i} ^{}^{1}^{}ι_{i} ^{−1}^{}σ′.

(c) σ′ entsteht durch Ersetzen eines τ_{j} durch ι_{j} in σ, und ι_{i} ist für x = 1 nicht positiv und für x = −1 nicht negativ in σ′ enthalten: ersetze τ_{i} ^{}^{1}^{}ι_{i} ^{x}^{}σ ^{}^{1}^{}σ′ durch τ_{i} ^{}^{1}^{}ι_{i} ^{y}^{}τ_{j} ^{}^{1}^{}ι_{j} ^{z}^{}σ′ mit y = x und z = 1, falls das zu ersetzende Vorkommen von τ_{j} in σ positiv ist, andernfalls mit y = −x und z = −1.

(d) σ′ entsteht durch Ersetzen von ι_{i} durch τ_{i} in σ, und ι_{i} ist kein Teiltyp

von τ_{i}: ersetze τ_{i} ^{}^{1}^{}ι_{i} ^{x}^{}σ ^{}^{1}^{}σ′ durch τ_{i} ^{x}^{}σ′.

(3) Falls K keine Ecke aus J enthält, so ist σ_{k,i} = φ_{k,i} → ψ_{k,i} für alle k = 1, …, m, i = 1, …, n_{k}.

(a) Setze k = 1.

(b) Solange k ≤ m: ersetze

σ^{k} ^{x_{k}}^{}φ_{k+1,1}→ψ_{k+1,1} ^{}^{1}^{}… ^{}^{1}^{}φ_{k+1,n_{k+1}}→ψ_{k+1,n_{k+1}} ^{x_{k+1}}^{}σ^{k+2}

durch · σ^{k} ^{−x_{k}}^{}φ_{k+1,1} ^{}^{1}^{}… ^{}^{1}^{}φ_{k+1,n_{k+1}} ^{−x_{k+1}}^{}σ^{k+2}, falls σ^{k} in φ_{k+1,k} enthalten ist, · σ^{k} ^{x_{k}}^{}ψ_{k+1,1} ^{}^{1}^{}… ^{}^{1}^{}ψ_{k+1,n_{k+1}} ^{x_{k+1}}^{}σ^{k+2}, falls σ^{k} in ψ_{k+1,k} enthalten ist,

und erhöhe k um 1.

(c) Ersetze alle Ausdrücke der Form σ ^{}^{1}^{}σ durch σ.

(4) Ersetze alle aufeinanderfolgenden einfachen Kanten σ_{1} ^{x}^{}σ_{2} ^{y}^{}σ_{3} durch σ_{1} ^{x·y}^{}σ_{3}.

• Ersetze alle Kanten ι_{i} ^{}^{1}^{}τ_{i} ^{}^{1}^{}ι_{i} durch ι_{i} und alle Kanten τ_{i} ^{}^{1}^{}ι_{i} ^{}^{1}^{}τ_{i} durch τ_{i}.

Satz 3.12 Algorithmus 3.11 terminiert und ist korrekt.

Beweis: Es ist klar, daß jeder einzelne Schritt des Verfahrens terminiert. Zum Beweis der Terminierung des gesamten Algorithmus muß also gezeigt werden, daß K nach endlich vielen Schritten keine Kante σ ^{}^{1}^{}σ′ mit σ ∼ / σ′ und σ′ ∼ / σ enthält. Die Schritte (1) und (4) beeinflussen diese Eigenschaft sicherlich nicht. In jedem der vier Fälle von Schritt (2) wird die Anzahl der Kanten σ ^{}^{1}^{}σ′ mit σ ∼ / σ′ und σ′ ∼ / σ um eins reduziert. In Schritt (3) wird die Länge der durch ^{}^{1}^{}benachbarten Typen gekürzt, eventuell auch hier die Anzahl der Kanten reduziert. Da in jedem Durchlauf des Algorithmus einer der Fälle (2a), (2b), (2c), (2d) oder (3) eintritt, bricht die Schleife nach endlicher Zeit ab, und der Algorithmus terminiert.

Die strukturelle Eigenschaft des Kantenzugs, keine zwei aufeinanderfolgenden einfachen Pfeile zu beinhalten, bleibt in jedem Schleifendurchlauf erhalten. Am Ende wird sichergestellt, daß keine aufeinander folgenden Doppelpfeile im Kantenzug enthalten sind. Auch das Produkt der Bewertungen ist in jedem Schritt des Algorithmus invariant. Zu zeigen ist, daß zu jedem Zeitpunkt nur dann eine Kante σ ^{1}^{}τ in K enthalten ist, wenn σ positiv in τ vorkommt und σ ^{−1}^{}τ nur dann, wenn σ negativ in τ auftritt. Dies gilt zu Beginn des Ablaufs des Algorithmus und ändert sich sicherlich nicht in den Schritten (1), (2a), (2b) und (4). In Schritt (2c) unterscheiden wir zwei Fälle: Kommt das zu ersetzende τ_{j} positiv in σ vor, so ist das Vorkommen von ι_{i} in τ_{j} genauso wie das von ι_{i} in σ, und ι_{j} kommt auch positiv in σ′ vor. Andernfalls ist das Vorkommen von ι_{i} in τ_{i} anders als das von ι_{i} in σ, und ι_{j} kommt negativ in σ′ vor. Dies wird durch die Gleichungen y = x und z = 1 bzw. y = −x und z = −1 ausgedrückt. In Schritt (2d) kommt τ_{j} genauso in σ′ wie ι_{i} in σ vor. Der für obige Frage einzig relevante Teilschritt in Schritt (3) ist Teil (b). Im ersten Fall ist das Vorkommen von σ_{k,n_{k}} in φ_{k+1,1} bzw. von φ_{k+1,n_{k+1}} in σ_{k+2,1} anders als das von σ_{k,n_{k}} in φ_{k+1,1} → ψ_{k+1,1} bzw. von φ_{k+1,n_{k+1}} → ψ_{k+1,n_{k+1}} in σ_{k+2,1}. Im zweiten Fall ändert sich nichts. Damit ist auch die Korrektheit von Algorithmus 3.11 bewiesen. □

Wir kommen nun zu dem zentralen Ergebnis, das die Positivitätseigenschaft eines Typsystems charakterisiert:

Satz 3.13 Sei {ι_{i} ∼ τ_{i} | i ∈ I, ι_{i} ∈ J , τ_{i} ∈ F_{J} \ J } eine Relation auf dem Gruppoid \underline{F}_{J}. Der Erzeugendengraph E_{J}^{∼} von F_{J} besteht aus der Eckenmenge J ∪ \{τ ∈ F | ∃ι ∈ J: ι ∼ τ} und den Kanten

• σ ^{−1}^{}τ, falls σ negativ in τ vorkommt,

• σ ^{1}^{}τ, falls σ ≠ τ und σ positiv in τ vorkommt,

• σ ^{}^{1}^{}τ, falls σ ≠ τ und σ ∼ τ oder τ ∼ σ.

(Wieder mit der Konvention: σ ^{}^{1} ^{}τ statt σ [figure: 1; 1] τ). Dann ist ∼ genau dann positiv, wenn für jeden Kreis

ι_{i_{1}}  ^{x_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{x_{2}}^{}… ^{}^{1}^{}ι_{i_{n}}  ^{x_{n}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}}

in E_{J}^{∼} gilt: x_{1} · . . . · x_{n} = 1.

Beweis: Bezeichne σ[φ/ψ] den Typ, der entsteht, wenn in σ jedes Vorkommen von ψ durch φ ersetzt wird. Sei

ι_{i_{1}}  ^{x_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{x_{2}}^{}… ^{}^{1}^{}ι_{i_{n}} ^{x_{n}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}}

ein Kreis in E_{J}^{∼} für den x_{1} · . . . · x_{n} = −1 gilt. Dann kommt ι_{i_{1}} negativ in

τ_{i_{1}}[τ_{i_{n}}[τ_{i_{n−1}} … [τ_{i_{2}}/ι_{i_{2}}]/ … /ι_{i_{n−1}}]/ι_{n}]

vor.

Sei umgekehrt ∼ negativ. Es gibt also σ_{1}, σ_{2} ∈ F_{J} mit σ_{1} ≈ σ_{2}, so daß σ_{1} negativ in σ_{2} vorkommt. Da ≈ die von ∼ erzeugte Kongruenzrelation ist, gibt es im Typengraph G_{J}^{∼} einen Kantenzug

σ_{1} ^{−1}^{}σ_{2} ^{}^{1}^{}σ_{3} … ^{}^{1}^{}σ_{n} ^{}^{1}^{}σ_{1}.

Algorithmus 3.11 liefert einen Kantenzug

ι_{i_{1}}  ^{x_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{x_{2}}^{}… ^{}^{1}^{}ι_{i_{n}} ^{x_{n}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}}

mit x_{1} · . . . · x_{n} = −1. □

Aus Satz 3.13 folgt direkt:

Korollar 3.14 Es gibt ein Entscheidungsverfahren dafür, ob eine endliche Relation {ι_{i} ∼ τ_{i} | i = 1, …, n, ι_{i} ∈ J, τ_{i} ∈ F_{J} } positiv oder negativ ist.

Beweis: Transformiere J in J′ und ∼ in eine Relation {ι_{i} ∼′ τ_{i} | i = 1, …, m, ι_{i} ∈ J′, τ_{i} ∈ F_{J′} \ J′}, so daß F_{J} /_{≈} ≅ F_{J′}/_{≈′}. Anschließend bestimme im Erzeugendengraph E_{J}^{∼′} alle Kreise der Gestalt

ι_{i_{1}}  ^{x_{1}}^{}τ_{i_{2}} ^{}^{1}^{}ι_{i_{2}}  ^{x_{2}}^{}… ^{}^{1}^{}ι_{i_{m}} ^{x_{m}}^{}τ_{i_{1}} ^{}^{1}^{}ι_{i_{1}},

berechne das Produkt x_{1} · . . . · x_{n} der Bewertungen und wende Satz 3.13 an. □

Folgendes Beispiel veranschaulicht Korollar 3.14 und die Wirkungsweise von Algorithmus 3.11: Beispiel: Sei J = {ι_{1}, ι_{2}, ι_{3}} und ∼ wie folgt definiert:

ι_{1} ∼ (ι_{2} →ι_{3})→ι_{1}
ι_{2} ∼ ι_{3} →ι_{3}
ι_{3} ∼ (ι_{2} →ι_{2})→ι_{1}

Obwohl keines der ι_{i} negativ in τ_{i} mit i = 1, 2, 3 vorkommt, ist ι_{1} negativ in

τ := ((((ι_{2} →ι_{2})→ι_{1})→ι_{3})→(ι_{2} →ι_{2})→ι_{1})→ι_{1} ≈ ι_{1}

enthalten. Der entsprechende Zyklus im Typengraph G_{J}^{∼} ist:

((ι_{3} →ι_{3})→ι_{3})→ι_{1}
[figure: 1; 1]

(ι_{2} →ι_{3})→ι_{1}  ((ι_{3} →ι_{3})→(ι_{2} →ι_{2})→ι_{1})→ι_{1}
[figure: 1; 1]
ι_{1}  \overline{−1  ^{}}τ

In den Schleifendurchläufen wird dieser Kantenzug wie folgt verändert:

1. Durchlauf: Schritt (2b)

((ι_{3} →ι_{3})→ι_{3})→ι_{1}
[figure: 1; 1]

(ι_{2} →ι_{3})→ι_{1}  ((ι_{3} →ι_{3})→(ι_{2} →ι_{2})→ι_{1})→ι_{1}
[figure: 1; −1; .........................; 1]

ι_{1} ..........................^{−1  ^{}}τ

2. Durchlauf: Schritt (2c)

((ι_{3} →ι_{3})→ι_{3})→ι_{1}
[figure: 1; ..................................; 1]
ι_{3}^{−1}

(ι_{2} →ι_{3})→ι_{1}  [figure: 1] (ι_{2} →ι_{2})→ι_{1} ((ι_{3} →ι_{3})→(ι_{2} →ι_{2})→ι_{1})→ι_{1}
[figure: 1; 1; ......................................................; −1]

ι_{1}

3. Durchlauf: Schritt (2b)

((ι_{3} →ι_{3})→ι_{3})→ι_{1}
[figure: ..................................; 1]
ι_{3} . . . . . . . . . . ; −1
[figure: −1]
(ι_{2} →ι_{3})→ι_{1}  [figure: 1] (ι_{2} →ι_{2})→ι_{1}
[figure: 1; 1]

ι_{1}

Nach drei Durchläufen endet die Schleife. Der entstandene Kantenzug ist auch ein Kreis im Erzeugendengraph E_{J}^{∼}:

ι_{2}

[figure: ...........................; 1; ............................................................; −1; ............................................................; 1]

[figure: ι_{3} →ι_{3}; (ι_{2} →ι_{3})→ι_{1}; 1; . . . . . . . . . . . . . . . . . .; 1; ι_{1}; 1; (ι_{2} →ι_{2})→ι_{1}]

[figure: ...........................; 1; ...........................; −1; 1]

ι_{3}^{−1}

Wie im Ausgangsgraphen ist das Produkt der Bewertungen dieses Zyklus -1.

Zusammen mit Satz 2.30 und Satz 3.9 folgt aus Korollar 3.14:

Korollar 3.15 Es gibt ein Entscheidungsverfahren dafür, ob der λ_{(\underline{F}_{J} ,≈)}-Kalkül zu einem endlich repräsentierbaren K-Typsystem (\underline{F}_{J} , ≈) stark normalisierend ist.

Beispiel: Der Erzeugendengraph E_{J}^{∼′} der Relation ∼′ aus dem Beispiel zu Algorithmus 2.27 ist:

[figure: ι_{5} →ι_{1}; 1; ι_{1}; −1; ι_{1} →ι_{4}]
[figure: −1; 1]
ι_{2} [figure: 1] ι_{5}  ι_{4}
[figure: 1; −1]
[figure: ι_{3} →ι_{5}; −1; ι_{3}; 1; ι_{4} →ι_{3}]

Mit Satz 3.13 sieht man sehr leicht, daß ∼′ und damit auch die ursprüngliche Relation ∼ positiv sind. Satz 3.9 garantiert für dieses Typsystem starke Normalisierbarkeit.

Folgende Beispiele zeigen, daß durch die Einführung von positiven Typkongruenzen tatsächlich mehr λ-Terme typisiert werden können als im einfach getypten λ_{→}-Kalkül:

Beispiel: Der λ-Term

t = λxy.x(y(xy))

ist in λ_{→} nicht typisierbar. Wäre dies der Fall, so gäbe es eine Basis Γ und ein Typsystem (\underline{F}, =) mit τ ∈ F und Γ ⊢ x(y(xy)) : τ. Nach dem Erzeugungslemma 2.11 gäbe es ein τ′ ∈ F mit Γ ⊢ x : τ′ → τ und Γ ⊢ y(xy) : τ′. Erneut nach dem Erzeugungslemma 2.11 existierte ein σ ∈ F mit Γ ⊢ y : σ → τ′ sowie Γ ⊢ xy : σ. Schließlich folgt nochmals aus dem Erzeugungslemma 2.11 die Existenz eines σ′ mit Γ ⊢ x : σ′ →σ und Γ ⊢ y : σ′. Es gilt also τ′ →τ = σ′ →σ, also auch τ′ = σ′. Wegen σ′ = σ →τ′ folgt τ′ = σ →τ′, ein Widerspruch.

Mit F := {ι_{1}, ι_{2}}, ι_{1} ∼ ι_{2} →ι_{1} und Γ = {(x : ι_{1} →ι_{2}), (y : ι_{1})} gibt es jedoch eine Herleitung \overline{(Var)} Γ ⊢ x : ι_{1} →ι_{2}

\overline{(Var)} ; Γ ⊢ y : ι_{1}

\overline{(Kon)}

Γ ⊢ y : ι_{2} →ι_{1}

\overline{(Var)} ; Γ ⊢ x : ι_{1} →ι_{2} \overline{(Var)} ; Γ ⊢ y : ι_{1}
\overline{(App)}
Γ ⊢ xy : ι_{2}
\overline{(App)}
Γ ⊢ y(xy) : ι_{1}
\overline{(App)}
Γ ⊢ x(y(xy)) : ι_{2}
\overline{(Abs)}
x : ι_{1} →ι_{2} ⊢ λy.x(y(xy)) : ι_{1} →ι_{2}
\overline{(Abs)}
⊢ λxy.x(y(xy)) : (ι_{1} →ι_{2})→ι_{1} →ι_{2}

für ⊢ λxy.x(y(xy)) : (ι_{1} → ι_{2}) → ι_{1} → ι_{2}. Mit Satz 3.13 sieht man anhand des Erzeugendengraphen E_{J}^{∼}

ι_{2} → ι_{1}
[figure: 1; −1]
ι_{1}  ι_{2}

schnell ein, daß ∼ positiv ist.

Beispiel: P. Urzyczyn hat in [Urz95] gezeigt, daß der λ-Term \overline{2}(\overline{2}k) mit \overline{2} := λyx.y(yx) und K := λxy.x weder in λ_{→} noch in System F typisierbar ist. Mit F und ∼ wie im vorhergehenden Beispiel und Γ′ := {(x : ι_{1}), (y : ι_{1} → ι_{1})} gibt es jedoch Herleitungen:

\overline{(Var)} ; x : ι_{1}, y : ι_{2} ⊢ x : ι_{1}

\overline{(Abs)}

x : ι_{1} ⊢ λy.x : ι_{2} →ι_{1}

\overline{(Kon)}

x : ι_{1} ⊢ λy.x : ι_{1}

\overline{(Abs)}

⊢ K : ι_{1} →ι_{1}

und

\overline{(Var)} Γ′ ⊢ y : ι_{1} →ι_{1}

\overline{(Var)} ; Γ′ ⊢ y : ι_{1} →ι_{1}  \overline{(Var)} ; Γ′ ⊢ x : ι_{1}
\overline{(App)}
Γ′ ⊢ yx : ι_{1}
\overline{(App)}
Γ′ ⊢ y(yx) : ι_{1}
\overline{(Abs)}
y : ι_{1} →ι_{1} ⊢ λx.y(yx) : ι_{1} →ι_{1}
\overline{(Abs)}
⊢ \overline{2} : (ι_{1} →ι_{1})→ι_{1} →ι_{1}

Zweifaches Anwenden der Regel (App) liefert schließlich ⊢ \overline{2}(\overline{2}K) : ι_{1} →ι_{1}.

J. B. Wells konnte in [Wel94] zeigen, daß das Typisierbarkeitsproblem in System F unentscheidbar ist. Im Kalkül der positiven Typkongruenzen ist dies anders, zum Beweis dafür benötigen wir folgendes Lemma:

Lemma 3.16 Seien t ein λ-Term, Γ bezüglich eines K-Typsystems (\underline{F}, ≈) eine Basis, die alle Variablen von t enthält und Γ ⊢ t : σ und Γ ⊢ t : τ Urteile mit σ, τ ∈ F. Dann gilt σ ≈ τ.

Beweis: Induktion über den Aufbau von t:

• t = x ∈ X:

Nach dem Erzeugungslemma 2.11 gibt es ein ρ ∈ F mit (x : ρ) ∈ Γ, σ ≈ ρ und τ ≈ ρ. Daraus folgt σ ≈ τ.

• t = t_{1}t_{2}:

Nach dem Erzeugungslemma 2.11 gibt es σ_{1}, τ_{1} ∈ F mit Γ ⊢ t_{1} : σ_{1} → σ und Γ ⊢ t_{1} : τ_{1} → τ. Nach Induktionsannahme gilt σ_{1} → σ ≈ τ_{1} → τ, mit der Kürzungsregel (K) folgt σ ≈ τ.

• t = λx.t_{1}:

Nach dem Erzeugungslemma 2.11 gibt es σ_{1}, τ_{1}, ρ ∈ F mit (x : ρ) ∈ Γ, Γ ⊢ t_{1} : σ_{1}, Γ ⊢ t_{1} : τ_{1}, σ ≈ ρ → σ_{1} und τ ≈ ρ → τ_{1}. Nach Induktionsannahme gilt σ_{1} ≈ τ_{1}, daraus folgt σ ≈ τ.

□

Korollar 3.17 Es gibt ein Entscheidungsverfahren dafür, ob es zu einem gegebenen ungetypten λ-Term t ein von einer positiven Relation ∼ erzeugtes K-Typsystem (\underline{F}, ≈) gibt, mit dem t typisierbar ist.

Beweis: Sei {x_{i} | i ∈ I} die Menge aller in t enthaltenen Variablen, wobei o.B.d.A. keine Variable x_{i} in t mehrfach gebunden oder sowohl frei als auch gebunden ist. Setze J := {ι_{i} | i ∈ I} und Γ := {(x_{i} : ι_{i}) | i ∈ I}. Für jeden Teilterm s von t führe man ausgehend von denjenigen mit minimaler Länge folgendes Verfahren durch. Dabei heißt eine Typvariable frisch, falls sie nicht in J enthalten ist und während des Ablaufs des Verfahrens noch nicht benutzt wurde.

• Falls s eine Variable ist mit (s : ι) ∈ Γ, setze σ_{s} := ι.

• Falls s eine Applikation s_{1}s_{2} ist, wähle eine frische Variable κ, setze σ_{s} := κ und σ_{s_{1}} ∼ σ_{s_{2}}→κ.

• Falls s eine Abstraktion λx.s_{1} ist mit (x : ι) ∈ Γ, setze σ_{s} := ι→σ_{s_{1}}.

K sei die Menge der in obigen Verfahren frisch eingeführten Variablen. Nach Konstruktion gilt für jeden Teilterm s von t auch Γ ⊢ s : σ_{s}, insbesondere ist t also bezüglich des Typsystems (\underline{F}_{J ∪K}, ≈) typisierbar. Sei (\underline{F}_{L}, ≈′_{L}) ein K-Typsystem, Γ′ eine Basis und τ′ ∈ F_{L} ein Typ, so daß Γ′ ⊢ t : τ′ ein Urteil ist. O.B.d.A. enthalte Γ′ genau die in t vorkommenden Variablen. Dann definiert φ: \underline{F}_{J ∪K} → F_{L} mit

φ(τ) = \{ \begin{matrix}ρ & falls (x : τ) ∈ Γ und (x : ρ) ∈ Γ′ \\ ρ & falls τ = σ_{s_{1}s_{2}} für ein beliebiges ρ ∈ F_{L} mit Γ′ ⊢ s_{1}s_{2} : ρ \\ φ(τ_{1})→φ(τ_{2}) & falls τ = τ_{1} →τ_{2} \end{matrix}

einen Gruppoidhomomorphismus. Für jeden Teilterm s von t wird Γ′ ⊢ s : φ(σ_{s}) mit Induktion über den Termaufbau von s gezeigt:

• s = x ∈ X: Wegen (x : σ_{x}) ∈ Γ folgt (x : φ(σ_{x})) ∈ Γ′ und somit Γ′ ⊢ x : φ(σ_{x}).

• s = s_{1}s_{1}: Nach Definition von φ gilt Γ′ ⊢ s_{1}s_{2} : φ(σ_{s_{1}s_{2}}).

• s = λx.s_{1}: Da x in Γ′ enthalten ist, gilt nach Induktionsannahme Γ′ ⊢ s_{1} : φ(σ_{s_{1}}) und (x : φ(σ_{x})) ∈ Γ′. Daraus folgt Γ′ ⊢ λx.s_{1} : φ(σ_{x})→φ(σ_{s_{1}}), also mit σ_{s} = σ_{x} →σ_{s_{1}} und φ(σ_{x})→φ(σ_{s_{1}}) = φ(σ_{x} →σ_{s_{1}}) auch Γ ⊢ λx.s_{1} : φ(σ_{s}).

Wir zeigen nun, daß aus σ ∼ σ′ mit σ, σ′ ∈ F_{J ∪K}, auch φ(σ) ≈′ φ(σ′) folgt. Nach Definition von ∼ gibt es einen Teilterm s = s_{1}s_{2} von t und ein κ ∈ K mit σ_{s_{1}} = σ, σ′ = σ_{s_{2}} → κ und σ_{s} = κ. Wie oben gezeigt, gilt Γ′ ⊢ s_{1} : φ(σ), Γ′ ⊢ s_{2} : φ(σ_{s_{2}}) und Γ′ ⊢ s_{1}s_{2} : φ(κ). Nach dem Erzeugungslemma 2.11 gibt es ein ρ ∈ F_{L} mit Γ′ ⊢ s_{1} : ρ→φ(κ) und Γ′ ⊢ s_{2} : ρ. Wegen Lemma 3.16 gilt daher φ(σ) ≈′ ρ→φ(κ) und φ(σ_{s_{2}}) ≈′ ρ, es folgt φ(σ) ≈′ φ(σ_{s_{2}})→φ(κ) = φ(σ_{s_{2}} →κ) = φ(σ′).

Sei ^{⌣}^{⌣}^{⌣} die symmetrische, transitive K-Hülle von ∼, also die kleinste symmetrische und transitive Relation, die die Kürzungsregel (K) erfüllt. Nach Satz 2.23 ist (\underline{F}_{J ∪K}, _{⌣}_{⌣}_{⌣}^{⌣}^{⌣}^{⌣}) mit der von ^{⌣}^{⌣}^{⌣} erzeugten Kongruenz _{⌣}_{⌣}_{⌣}^{⌣}^{⌣}^{⌣} wieder ein K-Typsystem. Da auch (\underline{F}_{L}, _{⌣}_{⌣}_{⌣}^{⌣}^{⌣}^{⌣}) ein K-Typsystem ist, folgt aus σ ∼ σ′ ⇒ φ(σ) ≈′ φ(σ′) auch σ _{⌣}_{⌣}_{⌣}^{⌣}^{⌣}^{⌣} σ′ ⇒ φ(σ) ≈′ φ(σ′). Falls für σ, τ ∈ F_{J ∪K} gilt, daß σ negativ in τ vorkommt, kommt auch φ(σ) negativ in φ(τ) vor. Ist also _{⌣}_{⌣}_{⌣}^{⌣}^{⌣}^{⌣} negativ, so auch die jedem anderen t typisierenden Typsystem zugrunde liegende Kongruenzrelation. Da mit ∼ auch ^{⌣}^{⌣}^{⌣} endlich ist, ist nach Korollar 3.14 entscheidbar, ob _{⌣}_{⌣}_{⌣}^{⌣}^{⌣}^{⌣} positiv oder negativ ist. Mit Satz 3.7 und Satz 3.9 folgt die Behauptung. □

4 Zusammenfassung

In dieser Arbeit wird untersucht, welche Typsysteme Typtreue bewahren. Satz 2.17 besagt, daß die Bedingung (K) hierfür ein hinreichendes Kriterium ist, wobei offen bleibt, ob sie auch notwendig ist. In Kapitel 3 wird diskutiert, wann alle Terme eines mit einem K-Typsystem (\underline{F}_{J} , ≈) getypten λ_{(\underline{F}_{J} ,≈)}-Kalküls stark normalisierend sind. Dies ist genau dann der Fall, wenn die Erzeugendenrelation ∼ positiv ist. Korollar 3.14 liefert ein graphentheoretisches notwendiges und hinreichendes Kriterium zum Nachweis der Positivität von endlichen Erzeugendenrelationen der Form {ι_{i} ∼ τ_{i} | i = 1, …, n, ι_{i} ∈ J, τ_{i} ∈ F_{J} }. Mit Algorithmus 2.27 ist ein Verfahren angegeben, das beliebige endlich repräsentierbare K-Typsysteme in Typsysteme der obigen Form übersetzt, so daß auch dann die Positivitätsbedingung nachgewiesen oder widerlegt werden kann. Dadurch wird eine Klasse von Typsystemen spezifiziert, mit denen neben den einfach typisierbaren λ-Termen noch weitere Terme typisiert werden können und dennoch starke Normalisierbarkeit garantiert ist. Nach Korollar 3.17 ist die Menge dieser Terme entscheidbar.

Es soll noch erwähnt werden, daß es auch andere Formen monomorpher Typsysteme gibt. Eng verwandt mit dem Begriff der Typkongruenzen und K-Typsystemen ist der der rekursiven Typen. Dabei verzichtet man auf Typkongruenzen und führt stattdessen Typvariablen und Ausdrücke der Form μα.τ ein, wobei α eine Typvariable und τ ein Typ ist, in dem α nicht negativ vorkommt. Anstelle der Regel (Kon) gibt es zwei Regeln:

Γ ⊢ t : τ[μα.τ/α] \overline{(Fold)} Γ ⊢ t : μα.τ Γ ⊢ t : μα.τ \overline{(Unfold)}

Γ ⊢ t : τ[μα.τ/α]

P. Urzyczyn konnte in [Urz95] zeigen, daß dieser Kalkül im folgenden Sinn äquivalent zum Kalkül der Typkongruenzen ist: Ein ungetypter λ-Term t läßt sich mit rekursiven Typen genau dann typisieren, wenn es eine positive Relation ∼ auf einem freien Gruppoid \underline{F} gibt, so daß t bezüglich (\underline{F}, ≈) typisierbar ist.

Literatur

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

[Bar92] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 118–309. Clarendon Press, 1992.

[HS86] J. R. Hindley and J. P. Seldin. Introduction to Combinators and λ-Calculus. Cambridge University Press, 1986.

[Ihr88] Th. Ihringer. Allgemeine Algebra. Teubner-Verlag, 1988.

[Men91] N. P. Mendler. Inductive types and type constraints in the second-order lambda-calculus. Annals of Pure and Applied Logic, 51:159–172, 1991.

[MS95] M. Marz and P. Selinger. A very well known theorem. Semsoc Newsletter, 4:7–8, 1995.

[Tak92] M. Takahashi. Parallel reductions in λ-calculus. Technical report, Tokyo Institute of Technology, 1992.

[Urz95] P. Urzyczyn. Positive recursive type assignment. Technical Report 95-03(203), Instytut Informatyki, Uniwersytet Warszawski, 1995.

[Wel94] J. B. Wells. Typability and type checking in the second order λ-calculus are equivalent and undecidable. In 9th LICS conference, pages 176–185. IEEE Computer Society Press, 1994.