Ein Kalkül für polymorphe Objekte

mit Untertypen

Diplomarbeit von Dirk Thierbach

Betreuer: Prof. Dr. K. Keimel Fachbereich Mathematik

�

Technische Hochschule Darmstadt Juli 1997

Inhaltsverzeichnis

1 Einleitung 2

2 Der Grundkalkül 4 2.1 Syntax und Reduktionsregeln . . . . . . . . . . . . . . . . . . 4 2.2 Beispiele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Diskussion der Modellierung . . . . . . . . . . . . . . . . . . . 9 2.4 Die Church-Rosser Eigenschaft . . . . . . . . . . . . . . . . . . 10 2.5 Das Typsystem . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.6 Typerhaltung . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.7 Zusammenfassung der Eigenschaften . . . . . . . . . . . . . . 25

3 Initialisierung 26 3.1 Explizite Initialisierung . . . . . . . . . . . . . . . . . . . . . . 26 3.2 Implizite Initialisierung . . . . . . . . . . . . . . . . . . . . . . 30

4 Polymorphismus 34 4.1 Syntax und Reduktionsregeln . . . . . . . . . . . . . . . . . . 34 4.2 Das Typsystem . . . . . . . . . . . . . . . . . . . . . . . . . . 37

5 Vollständigkeit 44 5.1 Funktionen als Objekte . . . . . . . . . . . . . . . . . . . . . . 44 5.2 Übersetzen des Lambda-Kalküls . . . . . . . . . . . . . . . . . 46

6 Diskussion 49 6.1 Mögliche Ergänzungen . . . . . . . . . . . . . . . . . . . . . . 50 6.2 Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . 51

Literaturverzeichnis 52

A Übersicht über alle Typregeln 54

Kapitel 1

Einleitung

Language shapes the way we think, and determines what we can think about.

B. L. Whorf

Objekt-orientiertes Programmieren ist immer noch eines der derzeit aktuellen Schlagwörter der Informatik. Dennoch sind die mathematischen Grundlagen, die diesem Paradigma zu Grunde liegen, noch nicht besonders gut verstanden. In den letzten Jahren gab es viele teilweise sehr erfolgreiche Versuche, dieses Paradigma mit den mathematischen Methoden, die man für das funktionale Programmieren kennt, zu erfassen [GM94, Bru94, PT94, QKB96].

Diese Arbeit versucht, sich dem Problem von einer anderen Seite zu nähren. Um objekt-orientiertes Programmieren zu verstehen, ist es wichtig, die minimalen Grundbegriffe zu identifizieren, auf denen es beruht. Diese Grundbegriffe werden hier in Form eines Kalküls formalisiert. Der Kalkül liegt irgendwo zwischen imperativem und funktionalem Programmieren, da er einerseits noch mit Kopierregeln bei der Reduktion arbeitet, es andererseits aber nicht möglich ist, Funktionen direkt im Kalkül anzugeben. Es handelt sich also nicht einfach um eine Erweiterung des Lambda-Kalküls, sondern um einen eigenständigen Ansatz.

Fast noch wichtiger als einen passenden Kalkül zu finden ist es, für diesen Kalkül ein angemessenes Typsystem zu formulieren. Typen unterstützen den Programmierer, indem sie ihn Fehler früher erkennen lassen. Daher kann man von dem Typsystem fordern, daß es bestimmte Arten von Fehlern auszuschließen helfen soll. Die andere wichtige Anforderung ist natürlich, daß das Typsystem stark genug sein soll, um alle wichtigen Programme auch erfassen zu können.

Als Indikator dafür, wann das Typsystem umfassend genug ist, wurde hier die Darstellbarkeit der Formalismen aus dem funktionalen Programmieren im getypten Objektkalkül benutzt. Dies ist keine triviale Forderung, da der Kalkül eben auf einem völlig anderen Ansatz als der Lambda-Kalkül beruht.

Um das Verständnis zu erleichtern werden wir den Kalkül in mehreren Schritten einführen. Wir beginnen mit einer einfachen Grundversion. Diese wird dann zunächst um den Begriff der Initialisierung erweitert und schließlich noch polymorph gemacht. Danach zeigen wir, daß das Typsystem jetzt umfassend genug ist, um auch den polymorphen Lambda-Kalkül interpretieren zu können. Schließlich fassen wir die wichtigsten Erkenntnisse noch einmal zusammen.

An dieser Stelle möchte ich mich noch recht herzlich bei Herrn Prof.Dr. Keimel für die geduldige Betreuung während bei der Entstehung dieser Arbeit bedanken.

Der Grundkalkül

In diesem Kapitel wird zum besseren Verständnis eine vereinfachte Version des Gesamtkalküls eingeführt, der dann in den folgenden Kapiteln erweitert wird. Für den Kalkül wird ein Typsystem in erklärt und einige wichtige Eigenschaften des Kalküls und des Typsystems bewiesen. Der Grundkalkül selbst wird in zwei Schritten definiert, wobei der zweite Schritt zunächst durch das Typsystem motiviert wird.

2.1 Syntax und Reduktionsregeln

Ein Objekt in unserem Kalkül hat zwei verschiedene Arten von Attributen, nämlich Felder und Methoden. Die Felder entsprechen Daten, die Methoden Programmen (oder Prozeduren). Beide Arten von Attributen werden innerhalb eines Objektes durch Namen gekennzeichnet. Auf die Felder eines Objektes kann wie auf die Felder eines Records (Verbundes) zugegriffen werden, das heißt, ein Feld kann gelesen und überschrieben werden. Eine Methode dagegen kann ausgeführt werden und bewirkt damit eine Zustandsänderung des Objektes. Dazu ist es nötig, innerhalb einer Methode auf das gesamte Objekt zugreifen zu können (Selbst-Referenz).

Damit sind schon alle grundlegenden Konzepte erklärt, die zur Modellierung benötigt werden. Wir notieren die Terme unseres Kalküls durch die Buchstaben A, B, C, … und Namen allgemein durch N, M. Konkrete Namen wie move oder new position werden dagegen klein geschrieben. Zur Unterscheidung zwischen Methoden und Feldern wird Methoden ein kleines σ vorangestellt, das einerseits an das λ für Funktionen aus dem Lambda-Kalkül erinnern soll und andererseits für state change steht. Die Selbst-Referenz wird durch $ notiert; dies ist gleichzeitig die einzige Variable in dem Kalkül. Ein Objekt schließlich besteht aus einer Liste L von Attributdefinitionen in eckigen Klammern. Dabei sind diese Attributslisten nur eine Notationsvereinfachung und kein konzeptionell eigenständiger Bestandteil des Kalküls. Das Lesen eines Feldes wird durch A.N, das Überschreiben mit einem neuen Wert B durch A.N◁−B und das Ausführen einer Methode durch A.σN gekennzeichnet. Schließlich führen wir noch ein Fehlersymbol ♢ ein, damit wir später Aussagen über das Reduktionsverhalten getypter Terme machen können.

Als eine weitere Notationsvereinfachung werden wir das mehrfache Auftreten gleichartiger Ausdrücke durch Indizes kennzeichenen und die zugehörige Bereichsangabe meist weglassen. Also steht N_{i}=A_{i} zum Beispiel für die Attributsliste N_{1}=A_{1}, N_{2}=A_{2}, …, N_{k}=A_{k} für ein geeignetes k. Für Listen schreiben wir auch einfach L. Damit können wir jetzt die (vorläufige) Syntax des Kalküls angeben:

Definition 2.1 Ein Term A des Kalküls wird nach folgender Grammatik gebildet:

\begin{aligned}A & ::= & A.N | A.N◁−A′ | A.σN | [L] | $ | ♢ \\ L & ::= & N_{i}=A_{i}, σM_{j}=B_{j} \end{aligned}

Für die Reduktionsregeln benötigen wir die Substitution A [$ := B], die weiter unten definiert wird und jedes Vorkommen von $ in A außerhalb einer Methode durch B ersetzt. Außerdem muß die Reduktion das Fehlersymbol ♢ berücksichtigen.

Definition 2.2 Ein Redex ist ein Term bestehend aus einem Objekt oder dem Fehlersymbol, jeweils gefolgt von einer Lese-, Schreib- oder Ausführoperation. Es sei L eine Liste, die keine Definition für N beziehungsweise σN enthält. Dann kontrahiert ein Redex auf eine der folgenden Arten:

\begin{aligned}[N=A, L].N & → & A \\ [N=A, L].N◁−B & → & [N=B, L] \\ [σN=A, L].σN & → & A [$ := [σN=A, L]] \end{aligned}

Ist die linke Seite des Redex von der Form C ≡ [L] oder C ≡ ♢, dann kontrahiert der Redex zu ♢:

\begin{aligned}C.N & → & ♢ \\ C.N◁−B & → & ♢ \\ C.σN & → & ♢ \end{aligned}

Es tritt also eine Fehler auf, sobald ein Objekt das geforderte Attribut nicht enthält, und dieser Fehler pflanzt sich fort. Nachzutragen ist noch die Definition der Substitution.

Definition 2.3 Die Substitution A [$ := C] ist induktiv definiert wie folgt (für die syntaktische Gleichheit schreiben wir ≡):

\begin{aligned}♢ [$ := C] & ≡ & ♢ \\ $ [$ := C] & ≡ & C \\ (A.N) [$ := C] & ≡ & A [$ := C] .N \\ (A.N◁−B) [$ := C] & ≡ & A [$ := C] .N◁−B [$ := C] \\ (A.σN) [$ := C] & ≡ & A [$ := C] .σN \\ [N_{i}=A_{i}, σM_{j}=B_{j}] [$ := C] & ≡ & [N_{i}=A_{i} [$ := C], σM_{j}=B_{j}] \end{aligned}

Es wird also $ in allen Teiltermen ersetzt, außer innerhalb von Methodendefinitionen. In diesem Sinne kann man sagen, daß Methodendefinitionen die Variable $ binden.

Schließlich wollen wir noch die Kontraktion eines Redex in jedem Kontext ermöglichen. Dazu erweitern wir die Notation → zu einer Relation zwischen beliebigen Termen:

Definition 2.4 Ein Term A reduziert in einem Schritt zu einem Term A′ — in Symbolen A → A′ — wenn A einen Redex B enthält, dieser zu B′ kontrahiert und A′ aus A entsteht, indem man B in A durch B′ ersetzt.

Wir schreiben → → für die reflexive und transitive Hülle von →.

Die Kontextregeln kann man auf die übliche Art und Weise auch rekursiv definieren, vergleiche auch Definition 2.12.

2.2 Beispiele

Das Standard-Beispiel, das für solche Kalküle immer wieder verwendet wird, ist der Punkt als graphisches Objekt:

Beispiel 2.5 Ein zweidimensionaler Punkt habe als Zustand seine x- und y-Koordinate und als Methode eine Prozedure move, die ihn um eine Distanz delta — die wieder ein Punkt ist — verschiebt. Dabei kann man sich Zahlenwerte zunächst durch geeignete Terme dargestellt denken, und außerdem gebe es eine Infix-Operation +, die Zahlen verknüpft. Dann sei

POINT≡ [x=0, y=0, delta=♢,
σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)]

Als eine Beispielreduktion betrachten wir

POINT.delta◁−[x=2, y=3, z=4].σmove

→ [x=0, y=0, delta=[x=2, y=3, z=4],

σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)

].σmove
→ → [x=0, y=0, delta=[x=2, y=3, z=4],

σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)

].x◁−(0 + [x=2, y=3, z=4].x).y◁−(0 + [x=2, y=3, z=4].y)
→ → [x=0, y=0, delta=[x=2, y=3, z=4],

σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)

].x◁−(0 + 2).y◁−(0 + 3)
→ → [x=0, y=0, delta=[x=2, y=3, z=4],

σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)

].x◁−(2).y◁−(3)
→ [x=2, y=0, delta=[x=2, y=3, z=4],

σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)

].y◁−(3)
→ [x=2, y=3, delta=[x=2, y=3, z=4],

σmove=$.x◁−($.x + $.delta.x).y◁−($.y + $.delta.y)]

Man beachte, daß der Parameter delta als ein zusätzliches Feld modelliert wurde. Dafür wollen wir eine eigene Notation einführen: Eingabeparameter von, sagen wir, der Methode m werden mit einem hochgestellten Minus m^{−} gekennzeichnet, Ausgabewerte mit einem hochgestellten Plus m^{+}. Die Exponenten sind dabei zunächst als Bestandteil des Namens zu betrachen.

Zu erklären ist auch noch, wie der Infix-Operator + modelliert wird. Man kann dies zum Beispiel wie in Smalltalk erreichen, indem die Objekte für Zahlen mit einer Methode add zusammen mit einem Eingabeparameter add^{+} versehen werden. Etwas weiter unten werden wir einen konkreten Term in dieser Art angeben. Damit wir auch einstellige Prozeduren demonstrieren können, nehmen wir außerdem eine Methode abs hinzu, die den Absolutbetrag einer Zahl berechnet. Damit können wir das Beispiel von eben vollständig im Kalkül notieren:

Beispiel 2.6 Der Punkt aus 2.5, um eine Methode norm für die 1-Norm mit Ausgabeparameter erweitert, sieht vollständig so aus:

POINT ≡ [x=0, y=0,

move^{−}=♢,

σmove= $.x◁−(($.x).add^{−}◁−($.delta.x).σadd)
.y◁−(($.y).add^{−}◁−($.delta.y).σadd),

norm^{+}=0,

σnorm=$.norm^{+}◁−(($.x.σabs.abs^{+}).add^{−}◁−($.y.σabs.abs^{+}).σadd) ]

Man sieht, daß die so im Kalkül notierten Funktionen nicht sonderlich gut lesbar sind. Später werden wir Abkürzungen für Funktionsaufrufe mit Parametern einführen, nachdem allgemein untersucht wurde, wie Funktionen in das Gesamtbild hineinpassen.

Als weiteres Beispiel demonstrieren wir, wie sich zwei grundlegende Datentypen in dem Kalkül darstellen lassen:

Beispiel 2.7 Der Datentyp Boolean wird zunächst durch zwei Objekte FALSE und TRUE modelliert, die auf eine Nachricht σif hin zwischen den zwei Argumenten then und else auswählt:

TRUE ≡[then=♢, else=♢, if^{+}=♢, σif=$.if^{+}◁−($.then)]
FALSE≡[then=♢, else=♢, if^{+}=♢, σif=$.if^{+}◁−($.else)]

Beispiel 2.8 Die natürlichen Zahlen kann man aus einem Objekt ZERO konstruieren, das die Nachfolgeoperation succ, die Vorgängerabfrage pred^{+} und den Test iszero^{+} versteht:

ZERO≡ [iszero^{+}=TRUE,
σsucc=($.iszero^{+}◁−(FALSE).pred^{+}◁−$),
pred^{+}=♢]

Mit diesen drei Attributen lassen sich sehr leicht die Methoden add, sub und mul definieren:

ZERO ≡ […,
add^{−}=♢, σadd=($.add^{−}).iszero^{+}.then◁−($)
.else◁−($.add^{−}◁−($.add^{−}.pred^{+}).σadd.σsucc).σif.if^{+}
sub^{−}=♢, σsub=($.add^{−}).iszero^{+}.then◁−($)
.else◁−($.add^{−}◁−($.add^{−}.pred^{+}).σsub.σpred).σif.if^{+}
mul^{−}=♢, σmul=($.add^{−}).iszero^{+}.then◁−($.add^{−})
.else◁−($.add^{−}($.mul^{−}◁−($.mul^{−}.pred^{+})).σadd).σif.if^{+}]

Man beachte, daß für die Rekursion keine besondere Vorkehrung nötig ist.

Nun versuchen wir, auch für den Datentyp Boolean Methoden zu definieren. Dabei ergibt sich zunächst eine Schwierigkeit: Die Methoden in TRUE müssen unter Umständen den Term FALSE benutzen, und umgekehrt. Es tritt also gegenseitige Rekursion auf. Dieses Problem kann man lösen, indem man beide Terme auch verfügbar macht. Wir benennen also TRUE und FALSE in TRUE′ und FALSE′ um und definieren neu:

Beispiel 2.9 Der Datentyp Boolean mit den Methoden and, or und not läßt sich modellieren als

TRUE ≡ [self=TRUE′, other=FALSE′, then=♢, else=♢,

if^{+}=♢, σif=$.if^{+}◁−($.self.then◁−($.then).else◁−($.else).σif.if^{+}) and^{−}=♢, and^{+}=♢, σand=

$.and^{+}◁−($.self.then◁−($.and^{−}).else◁−($)) or^{−}=♢, or^{+}=♢, σor=

$.or^{+}◁−($.self.then◁−($).else◁−($.or^{−})) not^{+}=♢, σnot=$.not^{+}◁−($.self◁−($.other).other◁−($.self)) ]

und FALSE genauso, nur daß self=FALSE′ und other=TRUE′ gesetzt wird.

In [MMS95] wurde das Problem der gegenseitigen Referenz ebenfalls erkannt, aber auf eine etwas andere Weise gelöst.

Verallgemeinert man diese Beispiele, so sieht man, daß man beliebige induktive Datentypen darstellen kann. Dies ist auch nicht weiter verwunderlich, da wir in einem späteren Kapitel aufzeigen werden, wie der komplette Lambda-Kalkül simuliert werden kann.

2.3 Diskussion der Modellierung

Die Notation der Syntax orientiert sich an dem in [AC94, AC96] entwickelten ς-Kalkül. Auf den ersten Blick ist der Unterschied zwischen beiden Kalkülen nicht allzu groß. Der Hauptunterschied ist, daß die Variable für die Selbstreferenz bei Abadi und Cardelli benannt ist, während hier nur eine einzige Variable $ benötigt wird. Tatsächlich wird in [AC96] sogar behauptet, daß verschiedene Namen nötig sind, um zum Beispiel die natürlichen Zahlen darstellen zu können. Wie man aber an den obigen Beispielen sieht, ist das nicht der Fall. Das liegt daran, daß im ς-Kalkül nicht explizit zwischen Feldern und Methoden unterschieden wird. Ist dieser Unterschied in Hinblick auf das Binden von $ gegeben, so sind die verschiedenen Namen des ς-Kalküls nicht mehr nötig.

Dieser Effekt ist auch symptomatisch für den Unterschied im Modellierungsansatz zwischen beiden Kalkülen. Bei Abadi und Cardelli wird immer noch funktional gedacht: Eine Methode ist im Prinzip eine Funktion mit einem ausgezeichneten Parameter. Sie gehen später sogar so weit, daß sie die übliche λ-Abstraktion — nachdem sie sie im ungetypten Kalkül kodiert haben — als primitive Konstruktion ansehen und eigene Typregeln dafür angeben. Leider stimmen diese Regeln nicht mit denen überein, die sich aus der Kodierung ergeben würden. In diesem Sinn ist also der getypte ς-Kalkül eigentlich eine Erweiterung des getypten Lambda-Kalküls. Man merkt auch noch an anderen Stellen, daß Abadi und Cardelli eher funktional modellieren, so zum Beispiel, wenn sie Klassen als eine Funktion definieren, die aus einer Sammlung von Funktionen (trait) ein Objekt macht.

Will man aber das Wesentliche des objekt-orientierten Paradigmas erfassen, dann darf man nicht von Funktionen ausgehen. Fundamental für Objekte ist ihr Zustand und die Zustandsänderungen. Und genau diese beiden, und nur diese beiden, werden hier modelliert. Es ist auch wesentlich für Objekte, daß sie geschützt sind: Man kann ihre Methoden nicht verändern und auch in ihre Felder nicht direkt hineingreifen. Genau dies wäre aber möglich, wenn man freie Variablen für die Selbstreferenz zuläßt.

Es ist typisch für imperatives Programmieren, daß Programme und Daten getrennt sind, und für funktionales Programmieren, daß zwischen ihnen nicht unterschieden wird. Das hier gewählt Modell liegt in der Mitte: Sie werden zwar konzeptionell getrennt, sind aber beide in einem Objekt vereint, das dann als Datenwert auch Programme enthalten kann.

Schließlich ist noch anzumerken, daß die oben geschilderten Beispiele von Datentypen eher untypisch sind. Die meisten dieser Beispiele sind induktive Datentypen, die oftmals binäre (also eigentlich keine zustandsändernde) Operationen haben. Auch ist die hier gewählte Modellierung nicht unbedingt die beste Variante. Sie zeigt nur, daß der Kalkül ausdrucksstark genug ist, und illustriert außerdem, wie das zustandsbasierte Programmieren in diesem Kalkül vor sich geht.

2.4 Die Church-Rosser Eigenschaft

Eine wichtige Eigenschaft, die jeder Kalkül zur Modellierung einer Programmiersprache erfüllen sollte, ist die sogenannte Church-Rosser-Eigenschaft. Hat der Kalkül diese Eigenschaft, dann kommt es (anschaulich gesprochen) auf die Reduktionsreihenfolge nicht an. Es sind also verschiedene Auswertungsstrategien möglich.

Es ist an dieser Stelle sinnvoll, sich noch nicht auf eine Auswertungsstrategie festzulegen, da sich beim Lambda-Kalkül gezeigt hat, daß bei den darauf basierenden funktionalen Sprachen dann in der Praxis auch verschiedene Strategien verwendet werden, jede mit ihren Vor- und Nachteilen.

Wir zeigen zunächst einige Hilfssätze, bevor wir die Church-Rosser-Eigenschaft formulieren und beweisen. Dabei gehen wir analog zu der in [Tak92] beschriebenen Tait-Methode für den Lambda-Kalkül vor.

Hilfssatz 2.10 Es gilt D [$ := C [$ := B] ] ≡ D [$ := C] [$ := B].

Beweis: Eine einfache Induktion über den Termaufbau von D. □

Lemma 2.11 (Substitutionslemma) Gilt A → A′, dann folgt

A [$ := B] → → A′ [$ := B] .

Beweis: Wieder eine einfache Induktion über den Termaufbau von A. Reduziert A → A′ nach den Kontextregeln, dann ist der Induktionsschritt offensichtlich. Auch bei der Reduktion durch Kontraktion eines Redex ist — außer beim Ausführen einer Methode — alles klar. Beim Ausführen einer Methode ist A von der Form A ≡ C.σN mit C ≡ [σN=D, L], und somit A′ ≡ D [$ := C]. Aber dann ist

\begin{aligned}A [$ := B] & ≡ & [σN=D, L].σN [$ := B] ≡ [σN=D, L [$ := B] ].σN \\ & → & D [$ := C [$ := B] ] ≡ D [$ := C] [$ := B] ≡ A′ [$ := B] \end{aligned}

nach dem vorigen Hilfssatz und mittels Induktion. □ Die Schlüsselidee für den nachfolgenden Beweis ist der Begriff der parallelen Reduktion. Intuitiv gesehen reduziert ein Term A parallel zu einem Term A′, wenn mehrere der in A vorhandenen Redexe (die auch verschachtelt sein dürfen) gleichzeitig kontrahiert werden können, aber nicht diejenigen Redexe, die bei diesem Prozeß neu entstehen.

Definition 2.12 (Parallele Reduktion) Die Relation ⇒ zwischen Termen wird induktiv definiert wir folgt: Gilt A ⇒ A′, A_{i} ⇒ A′_{i} und B ⇒ B′, und ist L ≡ N_{i}=A_{i}, σM_{j}=B_{j} sowie L′ ≡ N_{i}=A′_{i}, σM_{j}=B_{j} (wobei alle N_{i} und M_{j} von N verschieden sind), dann gilt auch

\begin{aligned}(1) & ♢ & ⇒ & ♢ \\ (2) & $ & ⇒ & $ \\ (3.1) & [N=A, L].N & ⇒ & A′ \\ (3.2) & [L].N & ⇒ & ♢ \\ (3.3) & ♢.N & ⇒ & ♢ \\ (3.4) & A.N & ⇒ & A′.N \end{aligned}

\begin{aligned}(4.1) & [N=A, L].N◁−B & ⇒ & [N=B′, L] \\ (4.2) & [L].N◁−B & ⇒ & ♢ \\ (4.3) & ♢.N◁−B & ⇒ & ♢ \\ (4.4) & A.N◁−B & ⇒ & A′.N◁−B′ \\ (5.1) & [σN=A, L].σN] & ⇒ & A′ [$ := [σN=A′, L′]] \\ (5.2) & [L].σN & ⇒ & ♢ \\ (5.3) & ♢.σN & ⇒ & ♢ \\ (5.4) & A.σN & ⇒ & A′.σN \\ (6) & [L] & ⇒ & [L′] \end{aligned}

Diese Definition ist leider etwas aufwendiger, da der Kalkül doch schon recht kompliziert ist und hier alle der in dem Kalkül vorhandenen Ausdrucksmittel auf einmal explizit gemacht werden müssen. In dieser Definition stecken auch die oben erwähnten Kontextregeln für die Reduktion.

Man beachte, daß die Relation ⇒ schon reflexiv ist.

Lemma 2.13 Für die paralle Reduktion ⇒ gelten folgende Aussagen:

(i) Aus A → A′ folgt A ⇒ A′.

(ii) Aus A ⇒ A′ folgt A → → A′.

(iii) Gilt A ⇒ A′, dann auch A [$ := B] ⇒ A′ [$ := B].

(iv) Gilt B ⇒ B′, dann auch A [$ := B] ⇒ A [$ := B′].

Beweis: Alle vier Aussagen zeigt man durch Induktion über den Termaufbau von A. Aussage (i) ist klar, da die Definition von ⇒ alle Kontextregeln und alle Kontraktionsregeln von → enthält. Für Aussage (ii) muß man die Reduktionen, die parallel ausgeführt werden, hintereinander ausführen. Dazu muß man in den Fällen (3.1), (4.1) und (5.1) die Induktionsannahme und die Kontextregeln für → verwenden; alle anderen Fälle sind offensichtlich. Aussage (iii) zeigt man genau wie das Substitutionslemma 2.11, nur gibt es hier mehr triviale Fälle. Für den Methodenaufruf (5.1) kann man wieder Hilfssatz 2.10 verwenden. Aussage (iv) ist offensichtlich: Man muß jeweils nur gemäß der Definition der Substitution und der parallelen Reduktion umformen. □

Eine Konsequenz dieses Lemmas ist, daß ⇒ (gesehen als Paarmenge) zwischen → und → → liegt. Insbesondere ist → → die transitive Hülle von ⇒.

Um nun die Church-Rosser-Eigenschaft nachzuweisen, genügt es, die sogenannte diamond-property (Karo-Eigenschaft) von ⇒ zu beweisen:

(⋄) Aus B_{1} ⇐ A ⇒ B_{2} folgt B_{1} ⇒ C ⇐ B_{2} für ein C

Durch Zerlegen von → → in ⇒-Schritte und Aneinanderkleben der Karos folgt dann, daß (♢) auch für → → gilt, was genau die Aussage des Satzes von Church-Rosser ist.

Es ist allerdings einfacher, eine noch stärkere Aussage als (♢) zu zeigen:

(∗) Aus A ⇒ B folgt B ⇒ A^{∗} .

Dabei wird A^{∗} durch A bestimmt, ist aber unabhängig von B ist. Genauer gesagt bekommt man A^{∗}, indem man alle in A vorhandenen Redexe gleichzeitig kontrahiert:

(1^{∗}) ♢^{∗}  ≡ ♢
(2^{∗}) $^{∗}  ≡ $
(3^{∗}.1) ([N=A, L].N)^{∗}  ≡ A^{∗}
(3^{∗}.2) ([L].N)^{∗}  ≡ ♢
(3^{∗}.3) (♢.N)^{∗}  ≡ ♢
(3^{∗}.4) (A.N)^{∗}  ≡ A^{∗}.N

falls keiner der anderen Fälle zutrifft

(4^{∗}.1) ([N=A, L].N◁−B)^{∗} ≡ [N=B^{∗}, L]
(4^{∗}.2) ([L].N◁−B)^{∗}  ≡ ♢
(4^{∗}.3) (♢.N◁−B)^{∗}  ≡ ♢
(4^{∗}.4) (A.N◁−B)^{∗}  ≡ A^{∗}.N◁−B^{∗}

falls keiner der anderen Fälle zutrifft

(5^{∗}.1) ([σN=A, L].σN])^{∗} ≡ A^{∗} [$ := [σN=A, L]^{∗}]
(5^{∗}.2) ([L].σN)^{∗}  ≡ ♢
(5^{∗}.3) (♢.σN)^{∗}  ≡ ♢
(5^{∗}.4) (A.σN)^{∗}  ≡ A^{∗}.σN

falls keiner der anderen Fälle zutrifft

(6)  [N_{i}=A_{i}, σM_{j}=B_{j}]^{∗} ≡ [N_{i}=A_{i}^{∗}, σM_{j}=B_{j}]

Satz 2.14 Die Relation → erfüllt (∗) und hat damit die Church-Rosser-Eigenschaft.

Beweis: Die Idee für den Beweis ist die folgende: Reduziert A zu B, indem irgendwo tief innen in A ein Redex kontrahiert wird, dann ist zu zeigen, daß sich alle Kontraktion weiter außen, die bei der Bildung von A^{∗} erforderlich sind, nachholen lassen. Die Aussagen (iii) und (iv) von Lemma 2.13 stellen dabei sicher, daß sich Substitution und Reduktion gegenseitig nicht stören.

Formal läuft der Beweis mittels einer Induktion über den Termaufbau von A, wobei noch nach der Regel unterschieden wird, wegen der A ⇒ B gilt:

Fall 1 Gilt A ≡ ♢ ⇒ B, dann muß auch B ≡ ♢ sein, da nur Fall (1) der Reduktion zutreffen kann. Also gilt auch B ⇒ ♢ ≡ A^{∗}.

Fall 2 Für A ≡ $ analog.

Fall 3.1 Ist A ≡ [N=C, L].N und außerdem B ≡ C′ nach (3.1), dann gilt auch C ⇒ C′. Da C ein Teilterm von A ist, gilt nach Induktionsvoraussetzung C′ ⇒ C^{∗}. Das heißt aber B ≡ C′ ⇒ C^{∗} ≡ A^{∗}.

Fall 3.2 Ist A ≡ [L].N (wobei N in L nicht definiert wird), dann muß B ≡ ♢ nach (3.2) sein. Das bedeutet B ≡ A^{∗}, also auch B ⇒ A^{∗}.

Fall 3.3 Analog.

Fall 3.4 Direkt durch Induktion.

Fall 4 Genauso wie Fall 3.

Fall 5 Bis auf (5.1) geht wieder alles wie vorher in den Fällen 3 und 4. Der Fall (5.1) ist auch am interessantesten, da hier die eigentliche Arbeit geleistet wird. Zur Abkürzung setzen wir D=[σN=C, L]. Ist nun aber A ≡ [D.σN] und B ≡ C′ [$ := D′] mit C ⇒ C′ und D ⇒ D′, dann gilt nach Induktionsvoraussetzung C′ ⇒ C^{∗} sowie D′ ⇒ D^{∗}. Aus 2.13 folgt weiter B ⇒ C^{∗} [$ := D′] ⇒ C^{∗} [$ := D^{∗}] ≡ A^{∗} wie gewünscht.

Fall 6 Wieder direkt durch Induktion. □

2.5 Das Typsystem

Ein Typsystem für unseren Objekt-Kalkül muß im wesentlichen darüber Buch führen, welche Attribute auf welcher Stufe zur Verfügung stehen, genau wie Typsysteme für den Lambda-Kalkül angeben, auf welche Art von Argumenten man einen Term anwenden kann. Das ist aber noch nicht alles: Ein wichtige Eigenschaft des objekt-orientierten Ansatzes ist es, auch mit Objekten umgehen zu können, die erst später zum Beispiel durch Vererbung zustande kommen und somit zum Zeitpunkt der Erstellung eines bestimmten Objektes noch gar nicht bekannt sind. Dies wird formal durch eine Untertypen-Beziehung beschrieben: Ein Typ T umfaßt einen Typen S, in Symbolen T ≤ S, wenn der Typ T alle Attribute (und eventuell sogar mehr) bereitstellt, die auch der Typ S enthält. Um die später entstandenen Objekte dann auch einsetzen zu können, soll es immer möglich sein, den Typ eines Terms abzuschwächen, also auf einen weniger umfassenden Typ einzuschränken.

Damit das auch bei Typen höherer Ordnung funktioniert, muß man zwischen kovarianten und kontravarianten Feldern unterscheiden. Kontravariante Felder (Notation N^{−}) dienen nur zur Eingabe, kovariante Felder (Notation N^{+}) dienen nur zur Ausgabe (man erinnere sich an die obigen Beispiele). Die alte Notation N wird beibehalten und besagt, daß es keine Rolle spielt, ob das Feld ko- oder kontravariant ist. Allerdings muß man noch berücksichtigen, daß man innerhalb von Methoden Eingabefelder auch lesen und Ausgabefelder schreiben muß. Diese Verwendung müssen wir besonders kennzeichnen. Dazu erweitern wir die Syntax unseres Kalküls:

Definition 2.15 Ein Term A wird gebildet wie in 2.1, wobei zusätzlich

A ::= … | A.↓N | A.↓N◁−A′

Die Reduktionsregeln für A.↓N sind genau dieselben wie für A.N, und die Regeln für A.↓N◁−B sind dieselben wie für A.N◁−B. Die Substitutionsregeln werden erweitert um

\begin{aligned}(A.↓N) [$ := C] & ≡ & A [$ := C] .N \\ (A.↓N◁−B) [$ := C] & ≡ & A [$ := C] .N◁−B [$ := C] \end{aligned}

Bei der Substitution fällt also die Zusatzinformation, daß es sich im ein eigenes Feld handeln soll, weg.

Nun können wir auch die korrekte Benutzung von Feldern formalisieren, da wir jetzt zwischen dem Zugriff auf eigene Felder und dem Zugriff auf Felder von außen unterscheiden können:

Definition 2.16 Ein Term heißt varianzkonsistent oder kurz konsistent, falls die Felder richtig verwendet werden, also keine Teilterme der Art A.N^{−} oder A.N^{+}◁−B vorkommen.

Man beachte, daß all diese neuen Notationen eigentlich nur Zusatzinformation für die Typisierung liefern und die Reduktion nicht beeinflussen.

Wir wollen jetzt Typen formal einführen. Wir verwenden für sie die Buchstaben T, S und R. Typen können auch Typvariablen enthalten, für die wir kleine griechische Buchstaben benutzen:

Definition 2.17 Ein Typ T ist entweder eine Typvariable α, β, … oder ein Ausdruck {N_{i} : T_{i}, σM_{j}}. Damit ist gemeint, daß das zugehörige Objekt die Methoden M_{j} und die Felder N_{i} zur Verfügung stellt, wobei die Felder jeweils den Typ T_{i} haben (wie schon oben lassen wir die Indexbereiche weg).

Wir schreiben N ∈ S beziehungsweise σM ∈ S, falls das Feld N beziehungsweise die Methode M in S vorkommt. Genauso schreiben wir S.N = T, falls das Feld N in S vorkommt und den Typ T hat. Als Abkürzung für eine Liste von Attributtypen verwenden wir den Buchstaben F, ähnlich wie L bei Objekten.

Folgende Aussagen sind also wahr:

N ∈ {N : T, F } σM ∈ {σM, F } {N : T, F }.N = T

Typaussagen werden immer relativ zu einem Typkontext Γ gemacht, der Typvariablen mit Typen in Verbindung setzt:

Definition 2.18 Ein Typkontext oder kurz Kontext ist eine geordnete Liste

Γ = α_{1} : T_{1}, …, α_{n} : T_{n}

Wir schreiben auch für den leeren Kontext.

Nun müssen wir noch sagen, was die freien Typvariablen eines Typs und eines Kontextes sind:

Definition 2.19 Die freien Variablen FV(T) eines Typs T sind alle Typvariablen, die in T vorkommen. Die freien Variablen FV(Γ) eines Kontextes Γ sind alle Variablen, die in dem Kontext deklariert werden. Formal:

FV( ) = {} FV(α : T, Γ) = {α} ∪ FV(Γ)

Die Kontexte sind deshalb geordnet, weil später deklarierte Typvariablen als freie Variablen nur die weiter vorne deklarierten enthalten sollen:

Definition 2.20 Ein Kontext Γ heißt wohlgeformt, wenn er die folgenden beiden Bedingungen erfüllt: Erstens dürfen keine Variablen doppelt deklariert werden. Zweites soll er entweder leer sein oder von der Form Γ = Γ′, α : T, wobei Γ′ auch wohlgeformt und die Bedingung FV(T) ⊆ FV(Γ′) erfüllt ist. Ab sofort werden wir nur noch wohlgeformte Kontexte betrachten.

Diese Definition rechtfertigt auch die Begriffsbildung freie Variablen eines Kontextes. Darunter könnte man sich zunächst auch die Vereinigung aller freien Variablen der dort deklarierten Typen vorstellen. Bei wohlgeformten Kontexten Γ umfaßt aber FV(Γ) diese Vereinigung.

\frac{type var}{Γ, α : T, Γ′ ⊢ α type}

                                             type obj

Γ ⊢ T_{i} type

Γ ⊢ {N_{i} : T_{i}, σM_{j}} type

Abbildung 2.1: Der Grundkalkül: Typwohlgeformtheit

sub refl ; Γ ⊢ S type ; Γ ⊢ S ≤ S

                  sub trans

Γ ⊢ S ≤ R Γ ⊢ R ≤ T

Γ ⊢ S ≤ T

\frac{sub var}{Γ, α : T, Γ′ ⊢ α ≤ T}

  sub obj

Γ ⊢ S′_{i} ≤ S_{i} Γ ⊢ T_{j} ≤ T′_{j}

Γ ⊢ {N_{i}^{−} : S_{i}, N_{j}^{+} : T_{j}, σM_{k}} ≤ {N_{i}^{−} : S′_{i}, N_{j}^{+} : T′_{j}, σM_{k}}

                                                 sub ext

Γ ⊢ {F′} type

Γ ⊢ {F, F′} ≤ {F }

Abbildung 2.2: Der Grundkalkül: Untertypen

Bemerkung 2.21 Wir wollen später die Aussage Γ ⊢ A : T so verstehen, daß der Term A im Kontext Γ getypt werden kann und mindestens den Typ T umfaßt, aber unter Umständen sogar einen stärkeren Typ S ≥ T. Genauso ist auch die Deklaration α : T zu verstehen: Die Typvariable α steht für Typen, die mindestens den Typ T umfassen.

Man hätte dafür auch die Notation α ≤ T wählen können, aber im Hinblick auf spätere Erweiterungen des Kalküls erschien diese Notation passender.

Definition 2.22 Es gibt drei Arten von Regeln, die bei der Typisierung eine Rolle spielen. Wir formalisieren sie als Urteile.

• Ein Typ T heißt wohlgeformt im Kontext Γ, wenn in T nur Variablen vorkommen, die in Γ auch erklärt werden. Das schreiben wir Γ ⊢ T type und formalisieren es durch die beiden Regeln in Abbildung 2.1.

• Die oben erwähnte Untertyprelation wird ausgedrückt durch das Urteil Γ ⊢ S ≤ T. Der Typ S umfaßt oder subsumiert also im Kontext Γ den Typ T, wenn dies durch die Regeln in Abbildung 2.2 hergeleitet werden kann. Man beachte, daß die Relation explizit reflexiv und transitiv gemacht wird.

• Einem Term A kann im Kontext Γ der Typ T zugewiesen werden, wenn Γ ⊢ A : T nach den Regeln in Abbildung 2.3 bewiesen werden kann. Aus

val subs

Γ ⊢ A : S Γ ⊢ S ≤ T

Γ ⊢ A : T

\frac{val self}{Γ, α : S ⊢ $ : α}

val read

Γ ⊢ A : S S.N = T

Γ ⊢ A.N : T

                                      val read'

Γ, α : S ⊢ A : α S.N = T

Γ, α : S ⊢ A.↓N : T

val write

Γ ⊢ B : T Γ ⊢ A : S S.N = T

Γ ⊢ A.N◁−B : S

                                      val write'

Γ, α : S ⊢ B : T

Γ, α : S ⊢ A : α S.N = T

Γ, α : S ⊢ A.↓N◁−B : α

val exec

Γ ⊢ A : S σM ∈ S

Γ ⊢ A.σM : S

                                       val exec'

Γ, α : S ⊢ A : α σM ∈ S

Γ, α : S ⊢ A.σM : α

val obj

Γ, α : S ⊢ B_{j} : α  α ∉ FV(Γ)
Γ ⊢ A_{i} : T_{i} S = {N_{i} : T_{i}, σM_{j}}
Γ ⊢ [N_{i}=A_{i}, σM_{j}=B_{j}] : S

Abbildung 2.3: Der Grundkalkül: Termtypen der val subs-Regel ergibt sich sofort, daß jeder Term auch mit einem abgeschwächten Typ versehen werden kann. Die Aussage Γ ⊢ A : T bedeutet also nicht, daß T der einzige Typ für A ist, sondern daß es möglicherweise auch noch stärkere geben kann.

Die Namen für die Regeln orientieren sich an denen in [AC96].

Man beachte den symmetrischen Aufbau für die gestrichenen und ungestrichenen read, write und exec-Regeln.

Damit ist das Typsystem für die Grundversion unsers Objektkalküls vollständig. In [AC94] wird argumentiert, daß die gleichzeitige Verwendung von ko- und kontravarianten Feldern nicht möglich ist, da sie zu Widersprüchen führt. Das ist zwar für das dort konstruierte Typsystem richtig, aber, wie wir im nächsten Abschnitt beweisen werden, ist dies nicht der Fall für das eben definierte Typsystem. In [QKB96] wird aus demselben Grund für die Eingabeparameter Invarianz verlangt, wobei argumentiert wird, daß in der Praxis kontravariante Eingabeparameter nie benötigt werden. Selbst wenn dies stimmen sollte, ist es aber es sicherlich von Vorteil, wenn man auch den allgemeineren Fall formal behandeln kann.

2.6 Typerhaltung

In diesem Abschnitt wollen wir zeigen, daß der Typ eines Terms bei der Reduktion erhalten bleibt. Daraus werden wir im nächsten Abschnitt einige interessante Eigenschaften des getypten Kalküls herleiten.

Im vorigen Abschnitt haben wir dazu den Begriff des varianzkonsistenten Terms eingeführt. Und nur für diese Terme können wir die Typerhaltung auch zeigen. Das ist allerdings keine wirkliche Einschränkung, da jeder Term, der von einem in der Praxis auftretenden Programm herrührt, auch konsistent sein wird.

Bei dem Versuch, die Typerhaltung für konsistente Terme direkt zu beweisen, ergibt sich aber das Problem, daß die Konsistenz selbst von der Reduktion nicht erhalten wird. Die Lösung besteht darin, zu etwas stärkeren Typregeln überzugehen, die für konsistente Terme mit den alten Typregeln übereinstimmen, aber noch genügend zusätzliche Information beinhalten, um die Typerhaltung beweisen zu können. Für das stärkere Typsystem benutzen wir ⊢⊢ statt ⊢.

Definition 2.23 Das Urteil Γ ⊢ A : T wird aufgeteilt in die zwei Urteile Γ ⊢⊢ A :: T und Γ ⊢⊢ A : T. Die Intuition dabei ist die folgende: Das Urteil Γ ⊢⊢ A :: T soll gelten, falls die Herleitung ohne die Abschwächungsregel

val subs

Γ ⊢⊢ A : S Γ ⊢ S ≤ T

Γ ⊢⊢ A : T

\frac{val self}{Γ, α : S ⊢⊢ $ :: α}

val read

Γ ⊢⊢ A : S S.N^{+} = T

Γ ⊢⊢ A.N^{+} : T

                                          val write

Γ ⊢⊢ B : T

Γ ⊢⊢ A : S S.N^{−} = T

Γ ⊢⊢ A.N^{−}◁−B : S

val read'

Γ, α : S ⊢⊢ A :: α S.N = T

Γ, α : S ⊢⊢ A.↓N : T

                                     val write'

Γ, α : S ⊢⊢ B : T

Γ, α : S ⊢⊢ A :: α S.N = T

Γ, α : S ⊢⊢ A.↓N◁−B :: α

val read''

Γ ⊢⊢ A :: S S.N = T

Γ ⊢⊢ A.N : T

                                          val write''

Γ ⊢⊢ B : T

Γ ⊢⊢ A :: S S.N = T

Γ ⊢⊢ A.N◁−B :: S

val exec

Γ ⊢⊢ A : S σM ∈ S

Γ ⊢⊢ A.σM : S

                                      val exec'

Γ, α : S ⊢⊢ A :: α σM ∈ S

Γ, α : S ⊢⊢ A.σM :: α

val exec''

Γ ⊢⊢ A :: S σM ∈ S

Γ ⊢⊢ A.σM :: S

val conv ; Γ ⊢⊢ A :: S ; Γ ⊢⊢ A : S

val obj

Γ, α : S ⊢⊢ B_{j} :: α  α ∉ FV(Γ)
Γ ⊢⊢ A_{i} : T_{i} S = {N_{i} : T_{i}, σM_{j}}
Γ ⊢⊢ [N_{i}=A_{i}, σM_{j}=B_{j}] :: S

Abbildung 2.4: Der Reduktionskalkül: Termtypen val subs ausgekommen ist. Dagegen ist es erlaubt, bei der Herleitung von Γ ⊢⊢ A : T den Typ T abzuschwächen. Die Regeln sind in Abbildung 2.4 aufgelistet.

Man erhält die neuen aus den alten Regeln, indem man jeweils das passende der beiden Urteile auswählt. Außerdem muß bei den ungestrichenen read, write und exec-Regeln sowohl die konsistente Verwendung von Feldern, möglicherweise mit der Abschwächungsregel, als auch die beliebige Verwendung von Feldern ohne die Abschwächungsregel erlaubt werden.

Den Zusammenhang zwischen beiden Typsystemen zeigt das folgende

Lemma 2.24 Sei A konsistent. Dann gilt Γ ⊢ A : T genau dann, wenn Γ ⊢⊢ A : T oder Γ ⊢⊢ A :: T gilt.

Beweis: Durch Inspektion der Regeln erkennt man, daß bei konsistenten Regeln die Herleitungen ineinander überführt werden können. □

Typvariablen können auf die übliche Art und Weise substituiert werden:

Definition 2.25 Wir schreiben S [α := T] für den Typ, der entsteht, wenn man in S alle Vorkommen von α durch T ersetzt.

Das es in Typen keine Bindung von Typvariablen gibt, muß man hier vor der Substitution auch nicht umbenennen. Für die Typsubstitution gilt wie üblich ein Vertauschungslemma:

Lemma 2.26 (Vertauschbarkeit der Typsubstitution) Es gilt

R [α := S] [β := T] = R [β := T] [α := S [β := T] ]

Beweis: Eine einfache Induktion über den Aufbau des Typs R. □

Als nächstes zeigen wir ein Substitutionslemma für alle drei Arten von Typregeln:

Lemma 2.27 (Substitutionslemma für Typen) Aus

Γ, α : S, Γ′ ⊢ T type  und  Γ, Γ′ ⊢ S type

folgt die Aussage Γ, Γ′ ⊢ T [α := S] type .

Beweis: Man induziert über die Herleitung von T. Bei Anwendung der Regel type var fährt man fort mit der gegebenen Herleitung von S. Bei der Regel type obj verwendet man die induktive Definition der Typsubstitution und die Induktionsvoraussetzung. Auf diese Weise erhält man eine Herleitung von T [α := S]. □

Lemma 2.28 (Substitutionslemma für Untertypen) Ist der Typ S im Kontext Γ wohlgeformt, das heißt, gilt Γ ⊢ S type, und weiß man außerdem Γ, α : S ⊢ R ≤ T, dann folgt Γ ⊢ R [α := S] ≤ T [α := S].

Beweis: Induktion über die Herleitung von R ≤ T: Die Regel sub refl ist klar. Bei der Regel sub var treten zwei Fälle auf. Ist die Variable β in sub var von α verschieden, dann muß α ∉ FV(T) gelten, da der Kontext wohlgeformt ist. Damit ist R [α := S] = β [α := S] = β, und T [α := S] = T, weshalb die Behauptung gilt. Ist andererseits β gleich α, dann ergibt die Substitution S ≤ S, was durch sub refl hergeleitet werden kann. Die Regeln sub obj und sub trans lassen sich wieder direkt durch Induktion abhandeln. Bei der Regel sub ext benutzt man zusätzlich das vorherige Lemma 2.27. □

Lemma 2.29 (Substitutionslemma für Termtypen) Es gelte das Urteil Γ ⊢⊢ A :: S, und es sei α ∉ FV(Γ) ∪ FV(S). Dann folgt:

\begin{aligned}(i) & Γ, α : S ⊢⊢ B : T & ⟹ & Γ ⊢⊢ B [$ := A] : T [α := S] \\ (ii) & Γ, α : S ⊢⊢ B :: T & ⟹ & Γ ⊢⊢ B [$ := A] :: T [α := S] \end{aligned}

Beweis: Wieder mit Induktion über die Herleitung von B : T beziehungsweise von B :: T. Zur Abkürzung sei Γ′ = Γ, α : S. Wir unterscheiden nach der zuletzt verwendeten Regel:

val subs Es gelte Γ′ ⊢ R ≤ T und Γ′ ⊢⊢ B : R. Aus dem vorigen Lemma folgt dann Γ ⊢ R [α := S] ≤ T [α := S]. Mittels Induktion erhält man außerdem Γ ⊢ B [$ := A] : R [α := S]. Das heißt aber Γ ⊢⊢ B [$ := A] : T [α := S].

val self Führt man die Substitution aus, so erhält man genau die Voraussetzung Γ ⊢⊢ A :: S.

val read Ist B ≡ C.N^{+} und Γ′ ⊢⊢ C : R mit R.N^{+} = T, dann folgt mittels Induktion Γ ⊢⊢ C [$ := A] : R [α := S]. Da aber R [α := S] .N^{+} =

T [α := S], erhält man Γ′ ⊢⊢ B [$ := A] : T [α := S].

val read' Gilt B ≡ C.↓N, dann muß die Prämisse Γ′ ⊢⊢ C :: α lauten, und es gilt S.N = T. Mit Induktion folgt Γ ⊢⊢ C [$ := A] :: S, und durch Anwenden der Regel val read'' erhält man Γ ⊢⊢ B [$ := A] : T. Da aber α ∉ FV(S) ⊇ FV(T), gilt auch Γ ⊢⊢ B [$ := A] : T [α := S].

val read'' Analog zu val read.

val write Ist B ≡ C.N◁−C′ und gilt Γ′ ⊢⊢ C : R sowie Γ′ ⊢⊢ C′ : R′, dann folgt mit Induktion Γ ⊢⊢ C [$ := A] : R [α := S] und Γ ⊢⊢ C′ [$ := A] :

R′ [α := S]. Durch Anwenden der Regel val write erhält man dann das gewünschte Ergebnis.

val write' Gilt wieder B ≡ C.N◁−C′, dann muß die Prämisse hier von der Form Γ′ ⊢⊢ C :: α sein, wobei außerdem S.N = T gilt. Da wieder α ∉ FV(T), kommt man analog zum Fall val read' durch Anwenden der Regel val write'' zum Ziel.

val write'' Analog zu val write.

val exec Direkt durch Induktion.

val exec' Analog zu val read' und val write' durch Ausführen der Substitution und Anwenden der Regel val exec''.

val exec'' Wieder direkt durch Induktion.

val obj Sei B = [N_{i}=C_{i}, σM_{j}=D_{j}] und T = {N_{i} : R_{i}, σM_{j}}. Mit der Induktionsannahme erhält man Γ ⊢⊢ C_{i} [$ := A] : R_{i} [α := S]. Daraus folgt mit der Regel val obj Γ ⊢⊢ B [$ := A] : T [α := S].

val conv Trivial. □

Bevor wir jetzt die Typerhaltung zeigen können, müssen wir noch beweisen, daß bei Objekttypen die möglicherweise mehrfache Anwendung der Abschwächungsregel auf eine kanonische Anwendung zurückgeführt werden kann:

Lemma 2.30 Falls Γ ⊢⊢ [L] : S′, dann kann man einen Typ S finden, so daß schon Γ ⊢⊢ [L] :: S und Γ ⊢ S ≤ S′.

Beweis: Durch Inspektion der Regeln erkennt man, daß die Herleitung von Γ ⊢⊢ [L] : S′ nur dadurch zustande gekommen sein kann, daß zuvor unter Umständen mehrmals die Regel val subs, davor die Regel val conv, und schließlich davor die Regel val obj angewandt worden ist. Die Regel val obj liefert eine Herleitung für Γ ⊢⊢ [L] :: S, und durch Zusammenfassen der Abschwächungen in den Anwendungen von val subs mittels sub trans erhält man Γ ⊢ S ≤ S′. □

Satz 2.31 (Typerhaltung) Es gelte A → A′. Dann folgt:

\begin{aligned}(i) & Γ ⊢⊢ A : S & ⟹ & Γ ⊢⊢ A′ : S \\ (ii) & Γ ⊢⊢ A :: S & ⟹ & Γ ⊢⊢ A′ :: S \end{aligned}

Beweis: Wir unterscheiden zunächst nach der Reduktionsregel und dann nach der Typregel, durch die man Γ ⊢⊢ A : S beziehungsweise Γ ⊢⊢ A :: S erhalten hat. Die Kontextregeln der Reduktion kann man jeweils durch die offensichtliche Induktion behandeln. Keiner dieser Fälle ist sonderlich interessant. Die Regeln für die Redexe sehen so aus:

val read Ist A ≡ [N^{+}=B, L].N^{+} sowie A′ ≡ B, und wurde Γ ⊢⊢ A : S mit val read hergeleitet, dann muß Γ ⊢⊢ [N^{+}=B, L] : T und T.N^{+}=S gelten. Aus Lemma 2.30 folgt, daß es einen Typ T′ gibt mit Γ ⊢⊢ [N^{+}=B, L] :: T′ und Γ ⊢ T′ ≤ T. Sei S′=T′.N^{+}. Nach der Herleitung von T′ muß dann gelten Γ ⊢⊢ B : S′. Da N^{+} kovariant ist, gilt ferner Γ ⊢ S′ ≤ S. Durch Anwenden der Regel val subs bekommt man dann eine Herleitung für Γ ⊢⊢ B : S′.

val read' Kann nicht vorkommen, da [L].↓N kein Redex ist.

val read'' Hier kann man argumentieren wie bei val read, nur daß Lemma 2.30 und die Abschwächung nicht verwendet werden müssen, weshalb hier auch nicht benötigt wird, daß das Feld kovariant ist.

val write Ist A ≡ [N^{−}=B, L].N^{−}◁−C und A′ ≡ [N^{−}=C, L], dann muß wegen der Herleitung von S auch Γ ⊢⊢ [N^{−}=B, L] : S mit S.N^{−} = T gelten. Wie oben findet man nach Lemma 2.30 einen Typ S′ mit Γ ⊢⊢ [N^{−}=B, L] :: S′ und Γ ⊢ S′ ≤ S. Es sei S′.N^{−} = T′. Um die Herleitung für [N^{−}=C, L] : S zu konstruieren, nehmen wir die Herleitung für [N^{−}=B, L] :: S′ gefolgt von einer Abschwächung auf S, wobei man dann aber statt Γ ⊢⊢ B : T′ zeigen muß, daß Γ ⊢⊢ C : T′. Bei der ursprünglichen Herleitung von S wurde schon Γ ⊢⊢ C : T gezeigt. Da N^{−} kontravariant ist, kann man aber Γ ⊢ T ≤ T′ aus Γ ⊢ S′ ≤ S folgern. Also erhält man mit einer weiteren Abschwächung wie gewünscht Γ ⊢⊢ C : T′.

val write' Kann nicht vorkommen, da [L].↓N◁−B kein Redex ist.

val write'' Man geht vor wie bei val write'', nur daß man keine Abschwächungen betrachten muß. Daher spielt es auch wieder keine Rolle, ob das Feld kontravariant ist.

val exec Es sei zur Abkürzung B ≡ [σM=C, L]. Falls dann A ≡ B.σM und A′ ≡ C [$ := B] ist, dann muß wegen der Herleitung von S schon Γ ⊢⊢ B : S gegolten haben. Nach Lemma 2.30 findet sich wieder ein Typ S′ mit Γ ⊢ S′ ≤ S und Γ ⊢⊢ B :: S′. Daher muß auch Γ, α : S′ ⊢⊢ C :: α gegolten haben, wobei α ∉ FV(Γ) ∪ FV(S′). Nach dem Substitutionslemma 2.29 folgt dann aber Γ ⊢⊢ C [$ := B] :: α [α := S′]. Durch Abschwächung erhält man schließlich Γ ⊢⊢ C [$ := B] : S.

val exec' Kann nicht vorkommen, da [L] :: α nicht herleitbar ist, wie man durch Inspektion von val obj sieht.

val exec'' Können wir wieder genauso wie val exec bewiesen, ohne Lemma 2.30 und Abschwächung zu benutzen. □

2.7 Zusammenfassung der Eigenschaften

Wir wollen noch einmal die Eigenschaften des Objektkalküls zusammenstellen:

• Der Kalkül hat die Church-Rosser-Eigenschaft, das heißt, verschiedene Auswertungsstrategien liefern dasselbe Ergebnis.

• Läßt sich für einen Term A ein Typ T durch ⊢⊢ A : T finden, dann läßt sich derselbe Typ auch für diejenigen Terme finden, die aus A durch Reduktion hervorgehen.

• Da der Fehler ♢ nicht typisierbar ist, folgt daraus, daß ein typisierbarer Term nicht zu einem Fehler reduzieren kann.

• Für konsistente Terme A reicht es dabei schon, wenn man durch ⊢ A : T für sie einen Typ finden kann.

• Schließlich folgt aus der Abschwächungsregel sofort, daß man in jedem Kontext einen Term durch einen anderen Term mit stärkerem Typ ersetzen kann.

Damit haben wir unsere wesentlichen Ziele erreicht: Durch das Typsystem kann man sicherstellen, daß bei der Ausführung kein Fehler entsteht, und man kann die Wiederverwendbarkeitsidee des objekt-orientierten Ansatzes im Typsystem wiederspiegeln.

Noch nicht klar ist, ob man auch alle Terme typisieren kann, die in der Praxis auftretenden Programmen entsprechen. Und in der Tat gibt es hier ein Problem: In den Beispielen in diesem Kapitel hatten wir Felder immer mit dem Fehlerterm ♢ belegt, wenn noch kein Wert bekannt war. Aber dann ist die Typisierung nicht möglich. Im nächsten Kapitel werden wir dazu eine Lösung entwickeln.

Initialisierung

3.1 Explizite Initialisierung

Wir erweitern das im letzten Kapitel vorgestellten Typsystem um den Begriff der zu initialisierenden Typen. In funktionalen Sprachen müssen den Funktionen Argumente gegeben werden, damit sie berechnet werden können. Bei Objekten entspricht dies der Forderung, daß Felder mit Werten überschrieben werden müssen, bevor eine Methode ausgeführt wird.

Die neuen Typen bilden wir wie folgt:

Definition 3.1 Ein Typ T wird nach der Grammatik

T ::= α | {N_{i} : T_{i}, σM_{j}} | ΛN.T

gebildet. ΛN.T soll bedeuten, daß im Typ T des Feld N noch überschrieben werden muß. Will man notieren, daß mehrere Felder überschrieben werden müssen, so kann man ΛN_{1}.ΛN_{2}. · · · ΛN_{k}.T durch ΛN_{i}.T abkürzen, wobei wir wieder den Bereich i ∈ {1, …, k} weglassen. Wenn wir einen Typ in dieser abgekürzten Form ΛN_{i}.T hinschreiben, dann meinen wir damit ab sofort, daß T nicht von der Form ΛN.T′ ist, das heißt, die Liste ΛN_{i} schon alle zu überschreibenden Felder enthält.

Weiter spielt die Reihenfolge der ΛN keine Rolle: Die Typen ΛN.ΛN′.T und ΛN′.ΛN.T sind gleich. Man kann diese Gleichheit auch formal in die Typregeln einbauen, aber wir werden sie der Einfachheit halber ab sofort in der Notation unterdrücken.

Für die Typisierung geben wir gleich die Regeln für den Reduktionskalkül an. Die vereinfachten Regeln für konsistente Terme kann man sich sofort aus diesen Regeln herleiten.

type init

Γ ⊢ T type Γ ⊢ ΛN.T type

                       sub init right

Γ ⊢ S ≤ ΛN.S

                                               sub init both

Γ ⊢ S ≤ T

Γ ⊢ ΛN.S ≤ ΛN.T

Abbildung 3.1: Der Initialisierungskalkül: Zusatzregeln für (Unter)-Typen

val subs

Γ ⊢⊢ A : S Γ ⊢ S ≤ T Γ ⊢⊢ A : T

\frac{val self}{Γ, α : S ⊢⊢ $ :: α}

val read

Γ ⊢⊢ A : ΛN_{i}.S S.N^{+} = T N^{+} ≠ N_{i} Γ ⊢⊢ A.N^{+} : T

                                          val write

Γ ⊢⊢ B : T S.N^{−} = T Γ ⊢⊢ A : ΛN^{−}.ΛN′_{i}.S Γ ⊢⊢ A.N^{−}◁−B : ΛN′_{i}.S

val read'

Γ, α : S ⊢⊢ A :: α S.N = T Γ, α : S ⊢⊢ A.↓N : T

                                     val write'

Γ, α : S ⊢⊢ B : T S.N = T Γ, α : S ⊢⊢ A :: ΛN.ΛN′_{i}.α Γ, α : S ⊢⊢ A.↓N◁−B :: ΛN′_{i}.α

val read''

Γ ⊢⊢ A :: ΛN_{i}.S S.N = T N ≠ N_{i} Γ ⊢⊢ A.N : T

                                           val write''

Γ ⊢⊢ B : T S.N = T Γ ⊢⊢ A :: ΛN.ΛN′_{i}.S Γ ⊢⊢ A.N◁−B :: ΛN′_{i}.S

val exec

Γ ⊢⊢ A : S σM ∈ S S ≠ ΛN.S Γ ⊢⊢ A.σM : S

                                      val exec'

Γ, α : S ⊢⊢ A :: α σM ∈ S Γ, α : S ⊢⊢ A.σM :: α

val exec''

Γ ⊢⊢ A :: S σM ∈ S Γ ⊢⊢ A.σM :: S

                           val obj

Γ, α : S ⊢⊢ B_{j} :: α  α ∉ FV(Γ)
Γ ⊢ T_{i} type S = {N_{i} : T_{i}, σM_{j}}
Γ ⊢⊢ [N_{i}=A_{i}, σM_{j}=B_{j}] :: ΛN_{i}.S

val init

Γ ⊢⊢ A : T S.N=T Γ ⊢⊢ [N=A, L] :: ΛN.ΛN_{i}.S Γ ⊢⊢ [N=A, L] :: ΛN_{i}.S

val conv ; Γ ⊢⊢ A :: S ; Γ ⊢⊢ A : S

Abbildung 3.2: Der Initialisierungskalkül: Termtypen Definition 3.2 Für den Typkalkül mit expliziter Initialisierung fügen wir zu den type und sub-Regeln für den Grundkalkül die Regeln in Abbildung 3.1 hinzu. Ein Term des Grundkalküls kann dann nach den val-Regeln in Abbildung 3.2 getypt werden.

Die Untertyp-Regeln ermöglchen es, jederzeit durch Abschwächung die Forderung hinzuzufügen, daß noch Felder zu initialisieren sind. Dies paßt einerseits in das Konzept dessen, was durch die Untertyprelation ausgedrückt werden soll (ein Term eines umfassenderen Typs soll überall da eingesetzt werden können, wo ein Term eines schwächeren Typs steht) und erleichtert andererseits die Formulierung der übrigen Regeln.

Diese erlauben ein Lesen von Feldern nur, wenn das Feld bereits initialisiert ist, das heißt, N in val read von allen N_{i} verschieden ist. Bei Überschreiben eines Feldes N ist es möglich, das zugehörige ΛN im Typ zu entfernen. Eine Methode schließlich darf nur ausgeführt werden, wenn keine Felder mehr initialisiert werden müssen. Nach der Regel val init kann man bei einem Objekttyp ein ΛN entfernen, wenn man nachweisen kann, daß das Feld den passenden Typ hat. Dies vereinfacht auch die Regel val obj, bei der nur noch geprüft werden muß, ob die Feldtypen in Γ auch wohlgeformt sind.

Beispiel 3.3 Mit Hilfe der Initialisierung kann man auch Terme typen, die den Fehler ♢ enthalten. So findet man zum Beispiel für den Term

ID ≡ [arg^{−}=♢, res^{+}=♢, σid=$.res^{+}◁−($.arg^{−})]

den Typ

Λarg^{−}.Λres^{+}.{arg^{−} : T, res^{+} : T, σid}

für jeden beliebigen Typ T.

Obwohl es also sein kann, daß das Fehlersumbol ♢ in einem typbaren Term vorkommt, so soll der Term dennoch nicht zu einem Fehler reduzieren können. Dazu müssen wir für den neuen Typkalkül wieder die Typerhaltung bei der Reduktion beweisen.

Lemma 3.4 Das Vertauschbarkeitslemma 2.26 und die Substitutionslemmas 2.27, 2.28 und 2.29 gelten auch für den neuen Typkalkül.

Beweis: Die Anwesenheit von ΛN in den Typen ändert nichts am Beweis der Lemmas. Die neue Regel val init erfordert eine triviale Anwendung der Induktionsbehauptung, und bei val obj muß man zusätzlich auf Lemma 2.27 verweisen. Auch das Zurückführen der einfach gestrichenen Regeln auf die zweifach gestrichenen Regeln nach der Substitution bereitet keine Schwierigkeiten, da man in den zweifach gestrichenenen Regeln den leeren ΛN_{i}-Präfix wählen kann. □

Das Lemma über Objekttypen benötigen wir jetzt in etwas stärkerer Form:

Lemma 3.5 Es gelte Γ ⊢⊢ [L] : ΛN_{i}.S, wobei alle N_{i} auch in S vorkommen sollen. Dann gibt es einen Typ S′, so daß Γ ⊢⊢ [L] :: ΛN_{i}.ΛN′_{j}.S′ und Γ ⊢ S′ ≤ S. Außerdem ist [L] von der Form [L] ≡ [N′_{j}=A_{j}, L′], und es gilt Γ ⊢⊢ A_{j} : S.N′_{j} für jedes j.

Beweis: Man erkennt durch Inspektion der Regeln, daß die Herleitung von Γ ⊢⊢ [L] : ΛN_{i}.S geendet haben muß mit mehrmaliger oder keinmaliger Anwendung von val subs nach einer Anwendung von val conv. Davor wurde val init unter Umständen mehrfach auf das Ergebnis von val obj angewendet.

Die mehrmalige Anwendung von val subs läßt sich wieder mittels sub trans zu einer Anwendung zusammenfassen. Diese Regel habe als Prämisse Γ ⊢ T ≤ ΛN_{i}.S. Dann sind auch alle Felder N_{i} in T vorhanden, da die Regel sub ext höchstens Felder zu T hinzufügen kann. Die Regel val obj muß also eine Herleitung der Form Γ ⊢⊢ [L] :: ΛN_{i}.ΛN′_{j}.S′ liefern, da alle N_{i} in T vorhanden waren und nachfolgenden val init-Regeln nur voranstehende ΛN beeinflussen. Alle ΛN′_{j} müssen aber irgendwann durch val init Regeln entfernt werden. Also gilt Γ ⊢⊢ A_{j} : S.N′_{j} für diese Felder. Schließlich ergibt sich Γ ⊢ S′ ≤ S, wenn man die zusammengefaßte Abschwächung betrachtet und dabei die sub init-Regeln ignoriert. □

Und schließlich muß die Typerhaltung neu bewiesen werden:

Satz 3.6 Auch für den erweiterten Typkalkül gilt: Reduziert A in einem Schritt zu A′, dann folgt

\begin{aligned}(i) & Γ ⊢⊢ A : S & ⟹ & Γ ⊢⊢ A′ : S \\ (ii) & Γ ⊢⊢ A :: S & ⟹ & Γ ⊢⊢ A′ :: S \end{aligned}

Beweis: Wir listen nur noch die Fälle für die ungestrichenen Typregeln auf. Die anderen Typregeln kann man wie in Satz 2.31 auf deren Beweis zurückführen, sofern sie überhaupt vorkommen können.

val read Falls A ≡ [N^{+}=B, L].N^{+} und A′ ≡ B, dann gilt wegen val read auch Γ ⊢⊢ [N^{+}=B, L] : ΛN_{i}.T und T.N^{+}=S. Daher folgt aus Lemma 3.5, daß es einen Typ T′ gibt mit Γ ⊢⊢ [N^{+}=B, L] :: ΛN_{i}.ΛN′_{j}.T′ und Γ ⊢ T′ ≤ T. Da N von allen N_{i} verschieden ist, muß außerdem Γ ⊢⊢ B : T′.N^{+} gelten. Nun ist N^{+} kovariant, also hat man Γ ⊢ T′.N^{+} ≤ T.N^{+}. Durch Anwenden der Regel val subs bekommt man dann eine Herleitung für Γ ⊢⊢ B : S′.

val write Ist A ≡ [N^{−}=B, L].N^{−}◁−C und A′ ≡ [N^{−}=C, L], dann ist S von der Form S = ΛN.ΛN_{i}.R, und es gilt Γ ⊢⊢ [N^{−}=B, L] : S mit R.N^{−} = T. Lemma 3.5 liefert einen Typ S′ = ΛN.ΛN_{i}.ΛN_{j}.R′ mit Γ ⊢⊢ [N^{−}=B, L] :: S′ und Γ ⊢ R′ ≤ R. Es sei T′ = R′.N^{−}.

Wir wollen eine Herleitung für [N^{−}=C, L] : S konstruieren. Dazu starten wir mit der Herleitung für [N^{−}=B, L] :: S′. Im Beweis von Lemma 3.5 haben wir gesehen, daß darauf Anwendungen von val init und schließlich eine Anwendung von val conv folgen. Wir fügen eine zusätzliche Anwendung von val init ein, die das ΛN entfernt. Dazu benötigen wir eine Herleitung von Γ ⊢⊢ C : T′. Diese existiert, da wegen der Kontravarianz von N^{−} gilt Γ ⊢ T ≤ T′ und wir daher die Prämisse Γ ⊢⊢ C : T aus der ursprünglichen val write-Regel nehmen und abschwächen können. Schließlich schwächen wir nach der val conv-Regel noch S′ auf S ab und erhalten so Γ ⊢⊢ [N^{−}=C, L] : S.

val exec Der Beweis verläuft genau wie in Satz 2.31, nur daß man bei der Anwendung von 2.30 bemerken muß, daß die val init-Regel für alle Felder angewandt worden ist, so daß man sie auch nach der Substitution wieder für alle Felder anwenden kann.

□

3.2 Implizite Initialisierung

In einem weiteren Schritt wollen wir den Kalkül so erweitern, daß auch beim Aufruf von Methoden eine implizite Initialisierung durchgeführt werden kann. Insbesondere soll kenntlich gemacht werden, welche Ausgabefelder eine Methode auf jeden Fall überschreibt und welche Eingabefelder sie normalerweise erwartet. Damit ist der Typkalkül dann stark genug, um Funktionen, die als Objekte ausgedrückt werden, wirklich typisieren zu können.

Definition 3.7 Ein Typ kann jetzt auf folgende Art gebildet werden:

T ::= α | {N_{i} : T_{i}, σM_{j}(N_{jk}→N_{jl})} | ΛN.T

Dabei sollen die Feldnamen hinter einer Methode ausdrücken, welche Felder N_{jk} beim Aufruf Werte erhalten sollen und welche Felder N_{jl} auf jeden Fall durch die Methode überschrieben werden.

Wir schreiben σM(N_{i}) ∈ S, wenn S garantiert, daß die Methode σM die Felder N_{i} überschreibt, also S von der Form S = {σM(N′_{j}→N_{i}), …} ist.

\frac{val self}{Γ, α : ΛN_{i}.S ⊢⊢ $ :: ΛN_{i}.α}

  val read'

Γ, α : ΛN_{i}.S ⊢⊢ A :: ΛN_{i}.α

S.N = T N ≠ N_{i}

Γ, α : ΛN_{i}.S ⊢⊢ A.↓N : T

                                   val write'

Γ, α : ΛN_{i}.S ⊢⊢ B : T S.N = T Γ, α : ΛN_{i}.S ⊢⊢ A :: ΛN.ΛN′_{j}.α

Γ, α : ΛN_{i}.S ⊢⊢ A.↓N◁−B :: ΛN′_{j}.α

  val exec

Γ ⊢⊢ A : ΛN_{i}.S

σM(N_{i}) ∈ S

Γ ⊢⊢ A.σM : S

                      val exec'

Γ, α : ΛN_{i}.S ⊢⊢ A :: ΛN′_{j}.α σM(N′_{j}) ∈ S

Γ, α : ΛN_{i}.S ⊢⊢ A.σM :: α

                                                    val exec''

Γ ⊢⊢ A :: ΛN_{i}.S σM(N_{i}) ∈ S

Γ ⊢⊢ A.σM :: S

  val obj

Γ, α : ΛN_{jk}.S ⊢⊢ B_{j} :: α  α ∉ FV(Γ)
Γ ⊢ T_{i} type S = {N_{i} : T_{i}, σM_{j}(N_{jk})}
Γ ⊢⊢ [N_{i}=A_{i}, σM_{j}=B_{j}] :: ΛN_{i}.S

Abbildung 3.3: Der implizite Initialisierungskalkül

Bemerkung 3.8 Für die Typherleitung Bedeutung werden dabei nur die Feldnamen hinter dem Pfeil haben. Die Feldnamen vor dem Pfeil werden aus folgendem Grund eingeführt: Die Schreibweise

A.σM(N_{1}◁−A_{1}, N_{2}◁−A_{2}, …, N_{n}◁−A_{n})

die an einen Funktionenaufruf mit den benannten Argumenten A_{1} bis A_{n} erinnern soll, kann als Abkürzung dienen für den Term

A.N_{1}◁−A_{1}.N_{2}◁−A_{2}. · · · .N_{n}◁−A_{n}.σM

Die in dieser Abkürzung erlaubten Feldnamen sind diejenigen, die beim dem Methodentyp vor dem Pfeil stehen.

Für den Rest des Kapitels werden wir diesen syntaktischen Zucker der Einfachheit halber weglassen und nur noch die Feldnamen hinter dem Pfeil berücksichtigen.

Die Typregeln, die diesmal geändert werden müssen, sind im wesentlichen die Regeln für die Methodenausführung und für den Zugriff auf eigene Felder innerhalb von Methoden.

Definition 3.9 Für den Typkalkül mit impliziter Initialisierung verändern wir die Typregeln gemäß Abbildung 3.3.

Die Herleitung wurde dahingehend verändert, daß für eine Methode mit Ergebnisfeldern N_{i} beim Auftreten von $ innerhalb des Methodenrumpfes ΛN_{i}.α als Typ gewählt wird. Diese ΛN_{i} müssen dann erst durch Überschreiben in val write' entfernt werden, damit die Regel val obj zur Anwendung kommen kann.

Beispiel 3.10 Wir können jetzt die Identitätsfunktion ID aus Beispiel 3.3 wirklich als Funktion darstellen und typisieren: Der Term

ID ≡ [arg^{−}=♢, res^{+}=♢, σid=$.res^{+}◁−($.arg^{−})]

erhält den Typ

Λarg^{−}.Λres^{+}.{arg^{−} : T, res^{+} : T, σid(arg^{−}→res^{+})}

Wenden wir nun ID beispielsweise auf X=[x : []] an: Der Term X hat den Typ X : {x : {}}, und auch das Ergebnis der Anwendung läßt sich durch

ID.σid(arg^{−}◁−X).res^{−} : {x : {}}

typisieren, was vorher nicht möglich war.

Wiederum ist die Typerhaltung zu zeigen. Alle Lemmas außer dem Substitutionslemma übertragen sich sofort.

Lemma 3.11 Das Substitutionslemma 2.29 gilt auch für den Typkalkül mit impliziter Initialisierung.

Beweis: Außer den in Lemma 3.4 angesprochenen Veränderungen bleibt der Beweis gleich. Die einfach gestrichenen Regeln passen nun exakt zu den zweifach gestrichenen Regeln, so daß es auch hier bei der Zurückführung der einen auf die anderen nach der Substitution keine Schwierigkeiten gibt. □

Satz 3.12 Für den Kalkül mit impliziter Initialisierung gilt die Typerhaltung.

Beweis: Alle Fälle bis auf die val exec-Regeln bleiben gleich. Sei also mit den Bezeichnungen von 3.6 A ≡ B.σM und A′ ≡ C [$ := B], wobei B eine Abkürzung für das Objekt B ≡ [σM=C, L] ist. Wegen der Voraussetzung Γ ⊢⊢ B.σM : S muß auch Γ ⊢⊢ B : ΛN_{i}.S gelten. Mit Lemma 3.5 finden wir einen Typ S′, so daß Γ ⊢⊢ B :: ΛN′_{j}.S′ und Γ ⊢ S′ ≤ S. Da außerdem σM(N_{i}) ∈ S, ist auch σ(N_{i}) ∈ S′. Also wurde in val obj die Prämisse Γ, α : ΛN_{i}.S ⊢⊢ C :: α bewiesen. Weil zusätzlich auch α ∉ FV(Γ) ∪ FV(S′), kann man das Substitutionslemma anwenden, welches Γ ⊢⊢ C [$ := B] :: α [α := S′] liefert. Durch Abschwächung erhält man dann Γ ⊢⊢ C [$ := B] : S.

Der Beweis für die val exec'' Regel verläuft wieder ganz analog, aber ohne Abschwächung; die val exec'-Regel kommt wie schon vorher nicht in Frage. □

Die Eigenschaften, die wir im zweiten Kapitel für den getypten Kalkül zusammengefaßt hatten, übertragen sich wörtlich auf den Kalkül mit Initialisierung.

Polymorphismus

Das Ziel dieses Kapitels soll es sein, den Kalkül mit einem Typsystem höherer Ordnung zu versehen, so daß man für im funktionalen Sinn polymorphe Terme (wie zum Beispiel die Identitätsfunktion) passende Typen finden kann. Für die Darstellung dieses Typsystems ist es dabei einfacher, vom Curry-Stil der letzten beiden Kapitel zum Church-Stil des Typisierens überzugehen, das heißt, die Typen mit in die Terme aufzunehmen.

Wie soll nun ein Typsystem höherer Ordnung für unseren Kalkül aussehen? Bei den Typsystemen höherer Ordnung für den Lambda-Kalkül ist der wesentliche Schritt, die Lambda-Abstraktion statt nur für Terme auch für Typen einzuführen. Überträgt man diese Idee auf unseren Kalkül, so bedeutet das, daß ein Objekt nicht nur Felder für Terme, sondern auch für Typen haben muß und dieser Typzustand die Typen der Felder beeinflussen kann. Diese Idee wollen wir nun umsetzen.

4.1 Syntax und Reduktionsregeln

Zuerst führen wir Terme und Typen ein.

Definition 4.1 Terme A und Typen T des Kalküls werden nach folgender Grammatik gebildet:

A ::= A.N | A.N◁−A′ | A.σN | [L | H] | $ | ♢ |
A.↓N | A.↓N◁−A′ | A.β◁−T
L ::= N_{i} : T_{i}=A_{i}, σM_{j}=B_{j}
H ::= β_{i}=T_{i}
T ::= α | {N_{i} : T_{i} | H}

Die Bezeichnungen sind fast die gleichen wie im zweiten Kapitel. L ist eine Liste von Felddefinitionen, die jetzt aber Typen haben, und von Methodendefinitionen. H ist eine Liste von Typfeldern. Ein Objekt ist nun in zwei Teile geteilt, und enthält Typfelder sowie Termfelder und Methoden. Auch der Typ eines Objektes hat passend dazu zwei Teile. Schließlich gibt es zusätzlich eine Operation, die Typfelder überschreiben kann.

Beispiel 4.2 Es sei A irgendein Term vom Typ T. Der Term ID, der die Identitätsfunktion darstellt, sieht in der polymorphen Version mit schon vorbelegten Felder so aus:

ID ≡ [arg^{−}:α=A, res^{+}:α=A, σid=$.res◁−($.arg) | α=T]

und hat den Typ

{arg^{−}:T, res^{+}:T, σid | α=T }

Bevor wir die Reduktionsregeln angeben können, müssen wir zunächst freie Variablen für Typen und Terme definieren:

Definition 4.3 Die freien Variablen FV(T) eines Typs T sind alle Typvariablen, die in T vorkommen, sofern sie nicht als Typfelder auftreten. Formal:

FV(α) = {α}

FV({N_{i} : T_{i}, σM_{j} | β_{k} : R_{k}}) = (⋃_{i} FV(T_{i}) − ⋃_{k}{β_{k}}) ∪ ⋃_{k} FV(R_{k})

Genauso sind die freien Typvariablen FV(A) eines Terms A diejenigen Typvariablen, die nicht durch ein darüberliegendes Typfeld gebunden sind, also:

FV([N_{i} : T_{i}=A_{i}, σM_{j}=B_{j} | β_{k}=R_{k}]) = (⋃_{i} FV(T_{i}) − ⋃_{k}{β_{k}}) ∪ ⋃_{k} FV(R_{k})
FV(A.N)  = FV(A)
FV(A.N◁−A′)  = FV(A) ∪ FV(A′)
FV(A.σN)  = FV(A)
FV(A.↓N)  = FV(A)
FV(A.↓N◁−A′)  = FV(A) ∪ FV(A′)
FV(A.β◁−T)  = FV(A) ∪ FV(T)
FV($)  = {|}
FV(♢)  = {|}

Als nächstes müssen wir zwei Substitutionen definieren:

Definition 4.4 Die Substitution von $ in einem Term A durch einen Term B wird wie schon vorher durch A [$ := B] notiert. Sie entspricht genau der in Definition 2.3 eingeführten Substitution.

Außerdem können wir auch eine Typvariable α in einem Term A durch einen Typ T ersetzen, was durch A [α := S] ausgedrückt wird. Dabei müssen wie üblich die gebundenen Typvariablen in A unter Umstanden umbenannt werden. Eine Typvariable, die als Teilterm eines Feldes auftritt, wird dabei durch ein entsprechendes Typfeld im Objekt gebunden. Formal:

[L | β_{k}=R_{k}] [α := S] ≡ [L [α := S] | β_{k}=R_{k} [α := S] ]
falls ⋃_{k}{β_{k}} ∩ FV(S) ≠ ∅
(A.N) [α := S]  ≡ A [α := S] .N
(A.N◁−A′) [α := S] ≡ A [α := S] .N◁−A′ [α := S]
(A.σN) [α := S]  ≡ A [α := S] .σN
(A.↓N) [α := S]  ≡ A [α := S] .↓N
(A.↓N◁−A′) [α := S] ≡ A [α := S] .↓N◁−A′ [α := S]
(A.α◁−T) [α := S] ≡ A [α := S] .α◁−T [α := S]
$ [α := S]  ≡ $
♢ [α := S]  ≡ ♢

wobei für L ≡ N_{i} : T_{i}=A_{i}, σM_{j}=B_{j} der substituierte Term L [α := S] gegeben ist durch N_{i}:T_{i} [β := S] =A_{i} [β := S], σM_{j}=B_{j} [β := S].

Die parallele Substitution A [β_{1} := T_{1}, …, β_{n} := T_{n}] ist analog definiert. Ist H ≡ β_{1}=T_{1}, …, β_{n}=T_{n} eine Liste von Typfeldern, dann schreiben wir die obige Substitution auch abkürzend als A [H].

Die Reduktionsregeln sind ebenfalls fast dieselben wie in 2.2:

Definition 4.5 Ein Redex des Kalküls kontrahiert auf folgende Weise:

\begin{aligned}[N=A, L | H].N & → & A [H] \\ [N=A, L | H].N◁−B & → & [N=B, L] \\ [σN=A, L | H].σN] & → & A [$ := [σN=A, L]] \\ [L | β=T, H].β◁−S & → & [L | β=S, H] \end{aligned}

Außerdem erhält man wie schon in Definition 2.2 auch dann einen Redex, wenn man in einer der obigen Regeln das Objekt durch das Fehlersymbol ♢ ersetzt. In diesem Fall kontrahiert der Redex zu ♢.

Der Hauptunterschied zum Grundkalkül ist, daß beim Lesen eines Feldes die Typvariablen durch die aktuellen Werte ersetzt werden und zusätzlich natürlich das Überschreiben von Typfeldern geeignet kontrahiert.

Satz 4.6 Der wie oben erweiterte Kalkül hat immer noch die Church-Rosser Eigenschaft.

Der Beweis dazu verläuft genau analog zum Beweis für den Grundkalkül. Man sieht sofort, daß sich Typsubstitution und die Substitution der Selbst-Referenz gegenseitig nicht beeinflussen. Also kann man die entsprechenden Substitutionslemmata ohne Probleme beweisen. Mit deren Hilfe zeigt man dann die Konfluenz der Reduktion wieder mit der Tait-Methode.

Von den dazu benötigten Lemmas formulieren wir nur eines, da wir es später noch einmal benötigen:

Lemma 4.7 (Vertauschbarkeit der Typsubstitution) Es gilt

R [α := S] [β := T] = R [β := T] [α := S [β := T] ]

Beweis: Eine einfache Induktion über den Aufbau des Typs R. □

4.2 Das Typsystem

Für das Typsystem müssen wir zunächst alle Konzepte aus dem zweiten Kapitel um die Typfelder erweitern. Zuerst führen wir eine zweite Art von Kontexten ein:

Definition 4.8 Ein Kontext Δ für freie Typvariablen besteht aus einer ungeordneten Liste von Typvariablen.

Definition 4.9 Ein Paar von Kontexten Δ; Γ heißt wohlgeformt, wenn Γ wohlgeformt ist im Sinne von Definition 2.20, wobei jede Deklaration in Γ aber auch freie Typvariable aus Δ enthalten kann. Außerdem darf keine der Typvariablen aus Δ in Γ deklariert werden.

Die freien Variablen FV(Δ; Γ) sind gegeben durch FV(Δ) ∪ FV(Γ). Für wohlgeformte Kontexte, auf die wir uns wieder ab sofort beschränken wollen, stimmt das mit der intuitiven Begriffsbildung überein: Es sind alle Typvariablen, die in den Deklarationen von Γ frei vorkommen.

Definition 4.10 Ist β; Γ wohlgeformt, dann wollen wir die Substitution in allen Deklarationen eines Kontextes Γ durch Γ [β := S] notieren. Formal gilt:

[β := S] = und (Γ, α : T) [β := S] = (Γ [β := S], α : T [β := S])

Für die Typregeln gehen wir zunächst wieder vom Grundkalkül aus, da man so die wesentlichen Unterschiede klarer sieht. Wir versuchen es zunächst mit den Regeln in den Abbildungen 4.1, 4.2 und 4.3. Dabei sind die Termtypregeln am interessantesten:

Bei den Lese- und Schreibregeln wird der Typ des betroffenen Feldes immer mit den aktuellen Inhalten der bindenden Typfelder substituiert. Daher

\frac{type var}{Δ; Γ, α : T, Γ′ ⊢ α type}  \frac{type free}{Δ, β; Γ ⊢ β type}

type obj

Δ; Γ ⊢ S_{k} type Δ, β_{k}; Γ, ⊢ T_{i} type Δ; Γ ⊢ {N_{i} : T_{i}, σM_{j} | β_{k} : S_{k}} type

Abbildung 4.1: Der polymorphe Kalkül: Typwohlgeformtheit

sub refl ; Δ; Γ ⊢ S type ; Δ; Γ ⊢ S ≤ S  sub trans ; Δ; Γ ⊢ S ≤ R ; Δ; Γ ⊢ R ≤ T ; Δ; Γ ⊢ S ≤ T  \frac{sub var}{Δ; Γ, α : T, Γ′ ⊢ α ≤ T}

sub obj

Δ, β_{l}; Γ ⊢ S′_{i} ≤ S_{i} Δ, β_{l}; Γ ⊢ T_{j} ≤ T′_{j} Δ; Γ ⊢ {N_{i}^{−} : S_{i}, N_{j}^{+} : T_{j}, σM_{k} | β_{l} : R_{l}}

≤ {N_{i}^{−} : S′_{i}, N_{j}^{+} : T′_{j}, σM_{k} | β_{l} : R_{l}}

                                        sub ext

Δ; Γ ⊢ {F′ | H} type

Δ; Γ ⊢ {F, F′ | H} ≤ {F | H}

Abbildung 4.2: Der polymorphe Kalkül: Untertypen

val subs

Δ; Γ ⊢ A : S Δ; Γ ⊢ S ≤ T Δ; Γ ⊢ A : T

\frac{val self}{Δ; Γ, α : S ⊢ $ : α}

val read

Δ; Γ ⊢ A : S S = {F | H} S.N [H] = T Δ; Γ ⊢ A.N : T

                                     val write

Δ; Γ ⊢ B : T Δ; Γ ⊢ A : S S = {F | H} S.N [H] = T Δ; Γ ⊢ A.N◁−B : S

val read'

Δ; Γ, α : S ⊢ A : α S = {F | H} S.N [H] = T Δ; Γ, α : S ⊢ A.↓N : T

                                     val write'

Δ; Γ, α : S ⊢ B : T Δ; Γ, α : S ⊢ A : α S = {F | H} S.N [H] = T Δ; Γ, α : S ⊢ A.↓N◁−B : α

val exec

Δ; Γ ⊢ A : S σM ∈ S Δ; Γ ⊢ A.σM : S

                                    val exec'

Δ; Γ, α : S ⊢ A : α σM ∈ S Δ; Γ, α : S ⊢ A.σM : α

val obj

Δ, β′_{k}; Γ, α : S′ ⊢ B_{j} : α α, β′_{k} ∉ FV(Δ; Γ) Δ; Γ ⊢ R_{k} type S = {N_{i} : T_{i}, σM_{j} | β_{k} : R_{k}} Δ; Γ ⊢ A_{i} : T_{i} [β_{k} := R_{k}] S′ = {N_{i} : T_{i}, σM_{j} | β_{k} : β′_{k}} Δ; Γ ⊢ [N_{i}=A_{i}, σM_{j}=B_{j} | β_{k}=R_{k}] : S

val type

Δ; Γ ⊢ T type Δ; Γ ⊢ A : {F | β : T′, H} Δ; Γ ⊢ A.β◁−T : {F | β : T, H}

Abbildung 4.3: Der polymorphe Kalkül: Termtypen (vorläufig) sehen Zugriffe von außen immer den gerade aktuellen Typ. Obwohl dies bei den einfach gestrichenen Regeln formal sehr ähnlich aussieht, ist die Situation hier doch etwas anders: Die Kontexte wurden in der Regel val obj so vorbereitet, daß die aktuellen Feldinhalte freie Typvariablen sind. Es kann also innerhalb eines Methodenrumpfes keine konkrete Annahme über den Inhalt der bindenden Typfelder gemacht werden.

Allerdings gibt es mit diesen Typregeln noch eine Schwierigkeit: Man wird es nicht schaffen, für die Regel val type in dieser Form die Typerhaltung nachzuweisen. Denn durch diese Regel kann sich der Typ der Felder eines Objektes verändern, ohne daß der Inhalt der Felder dem neuen Typ entsprechen muß. Um diesen Mangel zu beheben, verwenden wir den Typkalkül mit Initialisierung und ändern die Regel so ab, daß die betroffenen Felder nach dem Überschreiben des Typfeldes als uninitialisiert gewertet werden.

Damit können wir den Typkalkül endgültig angeben:

Definition 4.11 Der polymorphe Typkalkül entsteht, indem man den Kalkül mit Initialisierung aus dem dritten Kapitel mit den oben angebenen Regeln verschmilzt. Insbesondere wird die Regel val type modifiziert zu

    val type

Δ; Γ ⊢ T type

Δ; Γ ⊢ A : ΛN_{i}.{F | β : T′, H}

Δ; Γ ⊢ A.β◁−T : ΛN_{i}.{F | β : T, H}

wobei die N_{i} alle diejenigen Feldnamen sind, in deren Typ die Variable β frei vorkommt.

Der Kalkül in seiner endgültigen Form ist recht komplex. Zur Referenz ist er im Anhang vollständig angegeben.

Für die Typerhaltung müssen wir wieder zuerst die Substitutionslemmas formulieren.

Lemma 4.12 (Substitutionslemma für Typen)

(i) Ist S ein Typ in einem bestimmten Kontext, gilt also Δ; Γ, Γ′ ⊢ S type, dann läßt sich aus der Herleitung Δ; Γ, α : S, Γ′ ⊢ T type folgern, daß Δ; Γ, Γ′ ⊢ T [α := S] type.

(ii) Ist wieder Δ; Γ ⊢ S type, dann läßt sich aus Δ, α; Γ ⊢ T type folgern, daß Δ; Γ ⊢ T [α := S] type.

Beweis: Teil (i) wird genau wie in Lemma 2.27 bewiesen. Die Erweiterung des Kontextes Δ in type obj kann direkt durch Verwenden der Induktionsannahme behandelt werden. Teil (ii) zeigt man dann ganz analog. □

Lemma 4.13 (Substitutionslemma für Untertypen) Es sei S ein Typ in einem bestimmten Kontext, also Δ; Γ ⊢ S type. Dann gilt

(i) Aus Δ; Γ, α : S ⊢ R ≤ T folgt Δ; Γ ⊢ R [α := S] ≤ T [α := S].

(ii) Läßt sich das Urteil Δ, α; Γ, Γ′ ⊢ R ≤ T herleiten, dann folgt auch Δ; Γ, Γ′ [α := S] ⊢ R [α := S] ≤ T [α := S].

Beweis: Auch hier läuft der Beweis für Teil (i) genau wie bei Lemma 2.28. Teil (ii) wird wieder ganz analog gezeigt. Bei sub var muß zusätzlich berücksichtigt werden, daß T in Γ′ liegen muß, falls T die zu substituierende Typvariable α enthält und deshalb die Substitution auf beiden Seiten durchgeführt wird. □

Lemma 4.14 (Erstes Substitutionslemma für Termtypen) Es gelte die Voraussetzung Δ; Γ ⊢⊢ A :: S. Dann gilt auch

(i) Δ; Γ, α : S ⊢⊢ B : T ⟹ Δ; Γ ⊢⊢ B [$ := A] : T [α := S]
(ii) Δ; Γ, α : S ⊢⊢ B :: T ⟹ Δ; Γ ⊢⊢ B [$ := A] :: T [α := S]

Beweis: Man induziert wie in Lemma 2.29 über die Herleitung von B : T beziehungsweise über die Herleitung von B :: T. Wir diskutieren der Übersichtlichkeit halber die Fälle im Kalkül ohne Initialisierung; für den kompletten Kalkül muß man die Argumentation aus Lemma 3.4 noch hinzunehmen. Zur Abkürzung sei Γ′ = Γ, α : S′ und Δ′ = Δ, β_{k}. Wir beschreiben zunächst den Fall val read ausführlich:

Es sei B ≡ C.N^{+} und es gelte Γ′ ⊢⊢ C : R sowie R.N^{+} [H] = T für S = {F | H}. Durch Induktion erhält man dann Γ′ ⊢⊢ C [$ := A] : R [α := S]. Aufgrund von Lemma 4.7 und der Nebenbedingung der Substitution ist R [α := S] .N^{+} [H] = R.N^{+} [H] [α := S], da die bindenden Typvariablen aus H in S nicht frei sind. Also bekommt man durch Anwenden der Regel val read eine Herleitung für Γ′ ⊢⊢ B [$ := A] : T [α := S].

   Für die Fälle val read', val read'', val write', val write' und val

write'' kombiniert man die obige Argumentation zur Substitution mit der Behandlung des Falles in Lemma 2.29. Die Fälle val subs, val self und alle val exec-Fälle kann man direkt aus Lemma 2.29 übernehmen. Auch den Fall val obj kann man direkt übernehmen, da die Zusatzannahmen über die Form des Typs S den Induktionsschritt nicht verändern. Den Fall val type betrachten wir wieder ausführlich (der Fall val type'' funktioniert ganz analog):

Es sei B ≡ C.γ◁−R und T ≡ {F | β : R, H}. Nach Prämisse der Regel gibt es eine Herleitung für Δ; Γ′ ⊢⊢ C : T′ mit T′ ≡ {F | β : R′, H}. Durch Induktion erhält man Δ; Γ ⊢⊢ C [$ := A] : T′ [α := S]. Aus Δ; Γ′ ⊢ R type folgt nach Lemma 4.12 Δ; Γ ⊢ R [α := S] type. Anwenden der Regel val obj liefert dann Δ; Γ ⊢⊢ B [$ := A] : T [α := S]. □

Lemma 4.15 (Zweites Substitutionslemma für Termtypen) Es gelte allgemein Δ; Γ ⊢⊢ A :: S. Dann gilt:

(i) Aus der Voraussetzung Δ, α; Γ, Γ′ ⊢⊢ B : T läßt sich die Aussage Δ; Γ, Γ′ [α := S] ⊢⊢ B [α := S] : T [α := S] herleiten.

(ii) Aus der Voraussetzung Δ, α; Γ, Γ′ ⊢⊢ B :: T läßt sich die Aussage Δ; Γ, Γ′ [α := S] ⊢⊢ B [α := S] :: T [α := S] herleiten.

Beweis: Wir induzieren über die Herleitung von B : T beziehungsweise B :: T. Die Induktion verläuft für alle Fälle nach dem gleichen Schema: Enthalten die Prämissen sub- oder typ-Urteile, dann können wir Lemma 4.12 beziehungsweise Lemma 4.13 andwenden. Auf die anderen Prämissen läßt sich direkt die Induktionsannahme anwenden; und durch Anwenden der Regel des untersuchten Falles erhält man die gewünschte Konklusion. Bei der Regel val obj muß man etwas genauer hinsehen:

Sei B ≡ [N_{i} : C_{i}, σM_{j} : D_{j} | β_{k}=R_{k}]. Bis auf die Prämisse, die den Methodenrumpf überprüft, also konkret Δ, α, β_{k}; Γ, Γ′, γ : T′ ⊢⊢ D_{j} : γ kann man wieder das obige Schema verwenden. Aus dieser Prämisse folgt durch Induktion jedoch Δ, β_{k}; Γ, Γ′ [α := S], γ : T′ [α := S] ⊢⊢ D_{j} [α := S] : γ. Da aber in der gewünschten Konklusion auch T′ substituiert wird, paßt wieder alles zusammen, und durch Anwenden der Regel val obj ist dieser Fall auch gezeigt. □

Das Lemma 2.30 für die Objekttypen überträgt sich wörtlich, und wir können nun endlich die Typerhaltung zeigen:

Satz 4.16 (Typerhaltung) Es gelte A → A′. Dann folgt:

\begin{aligned}(i) & Γ ⊢⊢ A : S & ⟹ & Γ ⊢⊢ A′ : S \\ (ii) & Γ ⊢⊢ A :: S & ⟹ & Γ ⊢⊢ A′ :: S \end{aligned}

Beweis: Der Beweis geht fast genauso wie in Satz 2.31. Zusätzlich muß noch folgendes beachtet werden:

• Bei den Leseregeln paßt die Kontraktion des Redex mit der in der Regel vorgenommenen Substitution zusammen. Lemma 4.13 erlaubt es, auch bei den nötigen Abschwächungen die Substitution mit zu berücksichtigen.

• Bei den Schreibregeln wiederum stimmt die Substitution mit der Prämisse in val obj beziehungweise val init überein. Also gibt es auch hier keine Schwierigkeiten.

• Für die Ausführungsregel muß die Prämisse aus val obj für den Methodenrumpf benutzt werden. Dazu wendet man erst das zweite Substitutionslemma 4.15 an, um die β′_{k} durch die jetzt konkret gegebenen Inhalte der Typfelder zu ersetzen. Damit bringt man den Typ S und den Typ S′ aus der Regel val obj in Übereinstimmung, so daß man jetzt weiter wie in Satz 2.31 vorgehen und das erste Substitutionslemma anwenden kann.

• Für die Regeln val type und val type'' schließlich benutzt man, daß für alle Felder, deren Typen die Variable β frei enthalten, ein ΛN in der Konklusion der Regel hinzukommt. Daher muß für diese Felder die val init-Regel nicht angewandt werden. Alle anderen Vorkommen der val init-Regel, die man aus dem Lemma für Objekttypen erhält, können bedenkenlos weiter verwendet werden. Also kann man auch hier die gewünschte Herleitung konstruieren. □

Vollständigkeit

In diesem Kapitel wollen wir untersuchen, inwieweit jetzt Funktionen in dem Kalkül als typbare Objekte darstellbar sind. Dazu wollen wir zunächst einige Beispiele für solche Darstellungen untersuchen. Schließlich werden wir eine Übersetzung des getypten Lambda-Kalküls angeben. Damit haben wir dann gleichzeitig nachgewiesen, daß unser Kalkül vollständig im Sinne der Berechenbarkeit von Funktionen ist.

5.1 Funktionen als Objekte

Zuerst wollen wir die einfachste Funktion, nämlich die Identitätsfunktion, nochmal betrachten.

Beispiel 5.1 Der Term

ID ≡ [arg^{−}:α=♢, res^{+}:α=♢, σid=$.↓res^{+}◁−($.↓arg^{−}) | α={}]

stellt die polymorphe Identitätsfunktion dar. Sie hat den Typ

Λarg^{−}.Λres^{+}.{arg^{−}:α, res^{+}:α, σid(arg^{−}→res^{+}) | α={}}

Wir wollen ID wie im letzten Kapitel auf das Objekt X=[x : []] anwenden und dabei genau verfolgen, wie die Typen während der Reduktion aussehen.

X hat den Typ T = {x : {}}. Der Term, der ID auf X anwndet, lautet

A_{1} ≡ ID.α◁−T.σid(arg^{−}◁−X).res^{+}

Er hat wieder den Typ T. Betrachten wir jetzt die Reduktion. Zunächst reduziert A_{1} zu A_{2} ≡ B_{2}.σid(arg^{−}◁−X).res^{+} mit

B_{2} ≡ [arg^{−}:α=♢, res^{+}:α=♢, σid=$.↓res^{+}◁−($.↓arg^{−}) | α=T].

Dabei erhält B_{2} den Typ

⊢ B_{2} : Λarg^{−}.Λres^{+}.{arg^{−}:α, res^{+}:α, σid(arg^{−}→res^{+}) | α=T} Wir lösen die Abkürzung B.σid(arg^{−}◁−X) zu B.arg^{−}◁−X.σid auf. Dann reduziert A_{2} zu A_{3} ≡ B_{3}.σid.res^{+} mit

B_{3} ≡ [arg^{−}:α=X, res^{+}:α=♢, σid=$.↓res^{+}◁−($.↓arg^{−}) | α=T] Für B_{3} bestimmen wir den Typ

⊢ B_{3} : Λres^{+}.{arg^{−}:α, res^{+}:α, σid(arg^{−}→res^{+}) | α=T} Wird nun die Methode in A_{3} ausgeführt, dann reduziert A_{3} weiter zu

A_{4} ≡ B_{3}.res^{+}.◁−(B_{3}.arg^{−}).res^{+} Spätestens hier müssen wir jetzt zum Reduktionskalkül übergehen, um diesen Term noch typisieren zu können. Er erhält dann natürlich den Typ ⊢⊢ A_{4} : T. Wir reduzieren weiter zu

A_{5} ≡ B_{3}.res^{+}.◁−(X).res^{+} und schließlich zu A_{6} ≡ B_{6}.res^{+} mit

B_{6} ≡ [arg^{−}:α=X, res^{+}:α=X, σid=$.↓res^{+}◁−($.↓arg^{−}) | α=T] Dabei hat B_{6} den Typ

⊢⊢ B_{6} :: {arg^{−}:α, res^{+}:α, σid(arg^{−}→res^{+}) | α=T} Und zum Schluß reduziert A_{6} weiter zu X mit dem Typ T. Analog zur Identität kann man Projektionsfunktionen für Tupel definieren: Man muß nur mehrere Argumente arg_{1}^{−}, …, arg_{n}^{−} vorsehen. Dieses Beispiel ist natürlich eher trivial, da Objekte von sich aus schon Tupel darstellen. Interessanter ist da schon der Rekursionsoperator: Beispiel 5.2 Die polymorphe Rekursionsfunktion Y verarbeitet eine Funktion mit einem Argumentfeld arg^{−} und einem Resultatsfeld res^{+} sowie einer Methode σf. Dabei können Argument- und Resultatsfeld von einem beliebigen Typ α sein.

Y=[func^{−}:{arg^{−}:α, res^{+}:α |}=♢, limit^{+}:α=♢,
σrec=$.↓limit◁−($.↓func^{−}.σf(arg^{−}◁−($.σrec.limit^{+})).res^{+}) | α={|}]

Der Term Y hat den Typ Λfunc^{−}.Λlimit^{+}.{func^{−}:{arg^{−}:α, res^{+}:α |}, limit^{+}:α, σ(func^{−}→limit^{+}) | α={|}}

\frac{var}{Γ, x : T, Γ′ ⊢ x : T}

→-elim ; Γ ⊢ A : S→T  Γ ⊢ B : S ; Γ ⊢ A B : T  →-intro ; Γ, x : S ⊢ A : T ; Γ ⊢ λx : S.A : S→T

∀-elim ; Γ ⊢ A : ∀α.T ; Γ ⊢ A S : T [α := S] ∀-intro

Γ ⊢ A : T α ∉ FV(Γ)
Γ ⊢ Λalpha.A : ∀α.T

Abbildung 5.1: Der polymorphe Lambda-Kalkül

5.2 Übersetzen des Lambda-Kalküls

In diesem Abschnitt wollen wir den polymorphen Lambda-Kalkül in der Church-Version, wie er zum Beispiel in [Bar92] steht, in unseren Objektkalkül übersetzen. Dabei wollen wir sowohl Terme wie Typen übersetzen. Wir passen die Darstellung der Regeln für den Lambda-Kalkül an unsere Buchstabenkonvention an. Die Regeln für den polymorph getypten Lambda-Kalkül sind zur Referenz noch einmal in Abbildung 5.1 angegeben.

Wir beschränken uns zunächst auf den nicht-polymorphen Teil der Kalküle und geben eine Übersetzung der Terme ohne zusätzliche Typinformation an, damit das Prinzip klar wird.

Die Idee bei der Übersetzung ist, einen Lambda-Term durch einen closure zu interpretieren, das heißt, für die freien Variablen des Terms Platz zu reservieren und diesen dann zu füllen, sobald eine Applikation vorliegt. Diese Methode wird auch in der Praxis für die Implementierung des Lambda-Kalküls verwendet.

Definition 5.3 Wir bezeichnen mit Φ(A)_{Δ} die Übersetzung des Lambda-Terms A, der die freien Variablen in Δ hat, in den Objektkalkül. Konkret ist Φ durch

Φ(x)_{y_{1},...,y_{n},x} ≡ $.arg^{−}
Φ(y_{i})_{y_{1},...,y_{n},x} ≡ $.y_{i}
Φ(A B)_{y_{1},...,y_{n}} ≡ Φ(A)_{y_{1},...,y_{n}}.σexec(arg^{−}◁−Φ(B)_{y_{1},...,y_{n}}).res^{+}
Φ(λx.A)  ≡ [arg^{−}=♢, res^{+}=♢, σexec=$.res^{+}◁−Φ(A)_{x}]
Φ(λx.A)_{y_{1},...,y_{n},z} ≡ [arg^{−}=♢, res^{+}=♢, y_{1}=$.y_{1}, …, y_{n}=$.y_{n}, z=$.arg,
σexec=$.res^{+}◁−Φ(A)_{y_{1},...,y_{n},z,x}]

gegeben.

Will man beweisen, daß die Übersetzung und der Ursprungsterm adäquat zueinander reduzieren, dann muß man zusätzlich eine Rückübersetzung der closures angeben, in der die freien Variablen mit ihrer aktuellen Belegung im closure subtitutiert werden. Das ist etwas technisch; und da hier unser Hauptaugenmerk auf dem Typsystem liegt, werden wir diesen Beweis hier nicht durchführen.

Jetzt wollen wir zu den Typen höherer Ordnung übergehen. Zunächst geben wir dazu an, wie Typen übersetzt werden, da wir dies für die Übersetzung der Terme benötigen.

Definition 5.4 Die Übersetzung eines Typs T des Lambda-Kalküls wird durch Φ(T) notiert. Dabei ist

Φ(α)  = α
Φ(S→T) = Λarg^{−}.Λres^{+}.{arg^{−}:Φ(S), res^{+}:Φ(T) |}
Φ(∀α.T) = {body:Φ(T) | α : {|}}

Nun können wir auch die Terme des polymorphen Lambda-Kalküls übersetzen. Allerdings benötigen wir dazu mehr Typinformation, als uns in den Termen selbst zur Verfügung steht, da auch die Ergebnisfelder im Objektkalkül einen Typ bekommen müssen. Also übersetzen wir gleich das ganze Typurteil Γ ⊢ A : T, das uns die gewünschten Typinformationen liefern kann.

Definition 5.5 Wir bezeichnen mit Φ(Γ ⊢ A : T) die Übersetzung des Lambda-Terms A, der durch Γ ⊢ A : T getypt werden kann. Man beachte, daß wir für den Lambda-Kalkül geordnete Kontexte verwenden. Die Übersetzung sieht folgendermaßen aus:

Φ(Γ, x : T ⊢ x : T)  ≡ $.arg^{−}
Φ(Γ, y_{i} : T, Γ′ ⊢ y_{i} : T)  ≡ $.y_{i}
Φ(Γ ⊢ A B : T)  ≡
Φ(Γ ⊢ A : S→T).σexec(arg^{−}◁−Φ(Γ ⊢ B : S)).res^{+}
Φ(⊢ λx : S.A : S→T)  ≡ [arg^{−}:Φ(S)=♢, res^{+} : Φ(T)=♢,
σexec=$.res^{+}◁−Φ(x : S ⊢ A : T) | ]
Φ(Γ, z : R ⊢ λx : S.A : S→T) ≡ [arg^{−}:Φ(S)=♢, res^{+} : Φ(T)=♢,
y_{1}:Φ(R_{1})=$.y_{1}, …, y_{n}:Φ(R_{n})=$.y_{n}, z:Φ(R)=$.arg^{−},
σexec=$.res^{+}◁−Φ(Γ, z : R, x : S ⊢ A : T) | ]
wobei Γ = y_{1} : R_{1}, …, y_{n} : R_{n}
Φ(Γ ⊢ Λα.A : ∀α.T)  ≡ [body:T =Φ(Γ ⊢ A : T) | α={|}]
Φ(Γ ⊢ A S : T)  ≡ Φ(Γ ⊢ A : ∀α.T′).α◁−Φ(S).body

Satz 5.6 Sei A ein Lambda-Term mit Typ T. Dann ist Φ(A) im Objektkalkül typbar mit dem Typ Φ(T).

Beweis: Es ist offensichtlich, daß die Übersetzung der Typherleitung folgt. Man muß also nur noch für jeden Fall prüfen, ob sich eine passende Typherleitung im Objektkalkül finden läßt. Dabei muß noch berücksichtigt werden, daß man durch Abschwächung die Felder für die freien Variablen des Lambda-Terms verschwinden lassen kann. Damit läßt sich dann wirklich jeder Fall überprüfen. □

Der getypte Objektkalkül hat also die gleiche Ausdrucksstärke wie der polymorphe Lambda-Kalkül.

Diskussion

Nachdem der Kalkül jetzt vollständig ist, wollen wir kurz einige Beobachtungen zusammenfassen, die man durch ihn gewinnen kann.

Zunächst fällt auf, daß der Kalkül selbst zwar relativ einfach, aber das letztendliche nötige Typsystem schon sehr komplex ist. Das ist einerseits gut, da es zeigt, daß der Ansatz nun wirklich vom funktionalen Denken weiter entfernt ist. Andererseits ist es schlecht, da man komplexe Systeme mathematisch natürlich schlechter in den Griff bekommt. Allerdings ist es auch möglich, daß die Grundlagen des imperativen oder auch des objektorientierten Programmierens eben komplex sind, und es keine einfache elegante Modellierung dafür gibt.

Auch die Art der Übersetzung des Lambda-Kalküls weist darauf hin, daß mit dem Kalkül ungefähr der richtige Weg eingeschlagen wurde. Die natürlichste Übersetzung, die sich anbietet, ist auch in der Praxis weit verbreitet. Das zeigt, daß unser Kalkül offenbar wirklich zumindest einige der wichtigsten Grundlagen gut repräsentiert.

Eine völlig offene Frage ist es, wie ein geeignete Semantik für den Objektkalkül aussehen könnte. Die üblichen mathematischen Strukturen, auf die man normalerweise zurückgreifen würde, sind vermutlich ein Schritt in die falsche Richtung, da mit ihnen eher das funktionale Paradigma gut modelliert wird. Auch für die Typen wäre es schön, wenn man von den syntaktischen Strukturen wegkommen könnte und die gemischt-varianten Tupel statt dessen in einem Modell besser verstehen könnte. Dies würde vielleicht auch einen Hinweis darauf liefern, wie man einige der nun zu erwähnenden Defekte ausbessern könnte.

6.1 Mögliche Ergänzungen

In dem Kalkül gibt es Terme, für die man keinen Typ finden kann: Hat ein Objekte zum Beispiel zwei Felder x und y und die beiden Methoden σf=$.x◁−($.y.a) und σg=$.y◁−($.x.a), dann müßten sich die beiden Felder gegenseitig referieren, was in dem Typsystem nicht möglich ist.

Als Lösung kann man rekursive Typen einführen. Dabei muß man sich allerdings überlgen, wie sie mit den Untertypen sowie der Ko- und Kontravarianz richtig zusammenspielen sollen.

Um Funktionen darzustellen, haben wir für eine Methode besondere Ein- und Ausgabefelder reserviert. Genauso könnte man sich vorstellen, auch Felder nur für den Gebrauch innerhalb der Methode zu reservieren. Auf diese Art hätte man lokale Variablen für Methoden.

Die vielleicht interessanteste Erweiterung schließlich wäre es, den Kalkül mit einer imperativen Semantik auszustatten. Dazu müßte man sich die Objekte als persistent vorstellen. Felder verweisen dann auf andere Objekte, und man müßte eine clone-Operation oder ähnliches hinzunehmen, die neue Objekte erzeugt.

Bei dieser Art von Semantik geht die Church-Rosser Eigenschaft sofort verloren, da jetzt Seiteneffekte auftreten können. Man müßte dann also die Reduktionsreihenfolge festlegen. Auch bei der Polymorphie gibt es Probleme: Ein Objekt, daß von mehreren Feldern aus referiert wird, darf nicht einfach mit neuen Typfeldinhalten überschrieben werden, da ansonsten nicht gewährleistet ist, daß die referierenden Felder noch auf ein Objekt mit dem korrekten Typ zeigen. Die nicht-polymorphe Version des Typkalküls aber kann man auch mit der imperativen Semantik unverändert verwenden, wie man sich leicht überlegen kann.

Es gibt auch noch einige offene theoretische Fragen bezüglich des Typkalküls. So ist nicht geklärt, ob das Typisierbarkeitsproblem hier entscheidbar ist. Auch das Typherleitbarkeitsproblem ist noch offen. Man kann sich leicht einen Algorithmus überlegen, der in vielen Fällen auch den gewünschten Typ liefert. Schaut man sich diesen Algorithmus genauer an, so erkennt man, daß es Fälle gibt, wo der Algorithmus keinen minimalen Typ finden kann. Dies deutet darauf hin, daß das polymorphe Typsystem noch nicht allgemein genug ist.

6.2 Zusammenfassung

Was hat man jetzt durch diesen Kalkül gelernt? Der Kalkül zeigt, daß es ist möglich ist, die Grundlagen der objekt-orientierten und teilweise auch der imperativen Programmierung direkt zu modellieren, ohne den Umweg über funktionale Modelle zu gehen. Dies ist sogar mit der vollen Ko- und Kontravarianz und einer eingeschränkten Selbst-Referenz möglich.

Gleichzeitig hat man den Zusammenhang zwischen funktionalem und imperativen Programmieren sichtbar gemacht. Es wird nicht nur klar, auf welche Weise einen gegenseitige Simulation möglich ist, man kann auch genau sehen, wie sich die Wirkung einer Funktion in der imperativem getypten Sichtweise niederschlägt: Der ursprüngliche atomare Vorgang der Applikation wird dreigeteilt, mit der Konsequenz, daß das Typsystem dem Rechnung tragen muß.

Auch der Begriff der Polymorphie ist genauer beleuchtet worden: Zum einen schlägt sich die Polymorphie in den Untertypen nieder, zum anderen wird sie als parametrische Polymorphie ein Teil des Zustandes. Dies bietet vielleicht einen Ansatzpunkt, um auch Typsysteme höherer Ordnung für imperative Sprachen besser in den Griff zu bekommen.

Zusammenfassend kann man also sagen, daß — auch wenn unser Kalkül noch nicht eine endgültig zufriedenstellende Lösung ist — er doch zumindest einige Einblicke in die Zusammenhänge und Grundlagen der verschiedenen Programmierparadigma vermittelt.

Literaturverzeichnis

[AC94] Martin Abadi and Luca Cardelli. A theory of primitive objects: untyped and first order systems. In Proc. Theor. Aspects of Computer Software, pages 296–320, Japan, 1994. Expanded version to appear in Information and Computation.

[AC96] Martin Abadi and Luca Cardelli. A theory of objects. Springer Verlag, 1996.

[Bar84] Hendrik Pieter Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, 2nd 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.

[Bru94] Kim B. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4:127–206, April 1994.

[GM94] C. Gunter and J. Mitchel, editors. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1994.

[Mey88] Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, 1988.

[MMS95] Tom Mens, Kim Mens, and Patrick Steyaert. OPUS: a calculus for modelling object-oriented concepts. In D. Patel, Y. Sun, and S. Patel, editors, Proceedings of the 1994 International Conference on Object Oriented Information Systems, pages 152–165. Springer-Verlag, 1995.

[PT94] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4:207–247, April 1994.

[QKB96] Zhenyu Qian and Bernd Krieg-Brckner. Typed object-oriented programming with late binding. In Proc. 10th European Conf. on Object-Oriented Programming, LNCS, pages 48–72. Springer-Verlag, 1996.

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

Anhang A

Übersicht über alle Typregeln

In diesem Anhang sind noch einmal die vollständigen Typregeln für den polymorphen Typkalkül mit Initialisierung zusammengestellt. Regeln für Typwohlgeformtheit:

\frac{type var}{Δ; Γ, α : T, Γ′ ⊢ α type}

\frac{type free}{Δ, β; Γ ⊢ β type}

                                                type init

Δ; Γ ⊢ T type Δ; Γ ⊢ ΛN.T type

type obj

Γ ⊢ S_{k} type Γ, β_{k} : {|} ⊢ T_{i} type Γ ⊢ {N_{i} : T_{i}, σM_{j} | β_{k} : S_{k}} type

Regeln für Untertypen:

sub refl ; Δ; Γ ⊢ S type ; Δ; Γ ⊢ S ≤ S

sub trans ; Δ; Γ ⊢ S ≤ R ; Δ; Γ ⊢ R ≤ T ; Δ; Γ ⊢ S ≤ T

                                                sub init right

Δ; Γ ⊢ S type Δ; Γ ⊢ S ≤ ΛN.S

\frac{sub var}{Δ; Γ, α : T, Γ′ ⊢ α ≤ T}

                                            sub init both

Δ; Γ ⊢ S ≤ T

Δ; Γ ⊢ ΛN.S ≤ ΛN.T

sub obj

Δ, β_{l}; Γ ⊢ S′_{i} ≤ S_{i} Δ, β_{l}; Γ ⊢ T_{j} ≤ T′_{j} Δ; Γ ⊢ {N_{i}^{−} : S_{i}, N_{j}^{+} : T_{j}, σM_{k} | β_{l} : R_{l}}

≤ {N_{i}^{−} : S′_{i}, N_{j}^{+} : T′_{j}, σM_{k} | β_{l} : R_{l}}

                                        sub ext

Δ; Γ ⊢ {F′ | H} type

Δ; Γ ⊢ {F, F′ | H} ≤ {F | H} Regeln für das Typisieren konsistenter Terme:

val subs

Δ; Γ ⊢ A : S Δ; Γ ⊢ S ≤ T

Δ; Γ ⊢ A : T

\frac{val self}{Δ; Γ, α : ΛN_{i}.S ⊢ $ : ΛN_{i}.α}

val read

Δ; Γ ⊢ A : ΛN_{i}.S N ≠ N_{i} S = {F | H} S.N [H] = T

Δ; Γ ⊢ A.N : T

                                     val write

Δ; Γ ⊢ B : T

Δ; Γ ⊢ A : ΛN.ΛN′_{i}.S

S = {F | H} S.N [H] = T

Δ; Γ ⊢ A.N◁−B : ΛN′_{i}.S

val read'

Δ; Γ, α : ΛN_{i}.S ⊢ A : ΛN_{i}.α N ≠ N_{i} S = {F | H} S.N [H] = T

Δ; Γ, α : S ⊢ A.↓N : T

                               val write'

Δ; Γ, α : ΛN_{i}.S ⊢ B : T

Δ; Γ, α : ΛN_{i}.S ⊢ A : ΛN.ΛN′_{j}.α S = {F | H} S.N [H] = T

Δ; Γ, α : ΛN_{i}.S ⊢ A.↓N◁−B : ΛN′_{j}.α

val exec

Δ; Γ ⊢ A : ΛN_{i}.S σM(N_{i}) ∈ S

Δ; Γ ⊢ A.σM : S

                                       val exec'

Δ; Γ, α : ΛN_{i}.S ⊢ A : ΛN′_{j}.α σM(N′_{j}) ∈ S

Δ; Γ, α : ΛN_{i}.S ⊢ A.σM : α

val obj

Δ, β′_{k}; Γ, α : Λ_{jl}.S′ ⊢ B_{j} : α α, β′_{k} ∉ FV(Δ; Γ) Δ; Γ ⊢ R_{k} type S = {N_{i} : T_{i}, σM_{j}(N_{jl}) | β_{k} : R_{k}} Δ; Γ ⊢ T_{i} [β_{k} := R_{k}] type S′ = {N_{i} : T_{i}, σM_{j}(N_{jl}) | β_{k} : β′_{k}}

Δ; Γ ⊢ [N_{i}=A_{i}, σM_{j}=B_{j} | β_{k}=R_{k}] : S

val type

Δ; Γ ⊢ T type Δ; Γ ⊢ A : ΛN_{i}.{F | β : T′, H}

Δ; Γ ⊢ A.β◁−T : ΛN_{i}.{F | β : T, H}

val init

Δ; Γ ⊢⊢ A : T [H] Δ; Γ ⊢⊢ [N : T =A, L | H] : ΛN.ΛN_{i}.S

Δ; Γ ⊢⊢ [N : T =A, L | H] : ΛN_{i}.S Regeln für das Typisieren von Termen auch während der Reduktion:

val subs

Δ; Γ ⊢⊢ A : S Δ; Γ ⊢ S ≤ T

Δ; Γ ⊢⊢ A : T

\frac{val self}{Δ; Γ, α : ΛN_{i}.S ⊢⊢ $ : ΛN_{i}.α}

val read

Δ; Γ ⊢⊢ A : ΛN_{i}.S N^{+} ≠ N_{i} S = {F | H} S.N^{+} [H] = T

Δ; Γ ⊢⊢ A.N^{+} : T

                                    val write

Δ; Γ ⊢⊢ B : T

Δ; Γ ⊢⊢ A : ΛN^{−}.ΛN′_{i}.S

S = {F | H} S.N^{−} [H] = T

Δ; Γ ⊢⊢ A.N◁−B : ΛN′_{i}.S

val read'

Δ; Γ, α : ΛN_{i}.S ⊢⊢ A :: ΛN_{i}.α N ≠ N_{i} S = {F | H} S.N [H] = T

Δ; Γ, α : S ⊢⊢ A.↓N : T

                               val write'

Δ; Γ, α : ΛN_{i}.S ⊢⊢ B : T

Δ; Γ, α : ΛN_{i}.S ⊢⊢ A :: ΛN.ΛN′_{j}.α S = {F | H} S.N [H] = T

Δ; Γ, α : ΛN_{i}.S ⊢⊢ A.↓N◁−B :: ΛN′_{j}.α

val read''

Δ; Γ ⊢⊢ A :: ΛN_{i}.S N ≠ N_{i} S = {F | H} S.N [H] = T

Δ; Γ ⊢⊢ A.N^{+} : T

                                     val write''

Δ; Γ ⊢⊢ B : T

Δ; Γ ⊢⊢ A :: ΛN.ΛN′_{i}.S

S = {F | H} S.N [H] = T

Δ; Γ ⊢⊢ A.N◁−B :: ΛN′_{i}.S

val exec

Δ; Γ ⊢⊢ A : ΛN_{i}.S σM(N_{i}) ∈ S

Δ; Γ ⊢⊢ A.σM : S

                               val type

Δ; Γ ⊢ T type

Δ; Γ ⊢⊢ A : ΛN_{i}.{F | β : T′, H}

Δ; Γ ⊢⊢ A.β◁−T : ΛN_{i}.{F | β : T, H}

val exec'

Δ; Γ, α :: ΛN_{i}.S ⊢⊢ A : ΛN′_{j}.α σM(N′_{j}) ∈ S

Δ; Γ, α :: ΛN_{i}.S ⊢⊢ A.σM : α

val exec''

Δ; Γ ⊢⊢ A :: ΛN_{i}.S σM(N_{i}) ∈ S

Δ; Γ ⊢⊢ A.σM :: S

                               val type''

Δ; Γ ⊢ T type

Δ; Γ ⊢⊢ A :: ΛN_{i}.{F | β : T′, H}

Δ; Γ ⊢⊢ A.β◁−T :: ΛN_{i}.{F | β : T, H}

val obj

Δ, β′_{k}; Γ, α : Λ_{jl}.S′ ⊢⊢ B_{j} :: α α, β′_{k} ∉ FV(Δ; Γ) Δ; Γ ⊢ R_{k} type S = {N_{i} : T_{i}, σM_{j}(N_{jl}) | β_{k} : R_{k}} Δ; Γ ⊢ T_{i} [β_{k} := R_{k}] type S′ = {N_{i} : T_{i}, σM_{j}(N_{jl}) | β_{k} : β′_{k}}

Δ; Γ ⊢⊢ [N_{i}=A_{i}, σM_{j}=B_{j} | β_{k}=R_{k}] :: S

val init

Δ; Γ ⊢⊢ A : T [H] Δ; Γ ⊢⊢ [N : T =A, L | H] :: ΛN.ΛN_{i}.S

Δ; Γ ⊢⊢ [N : T =A, L | H] :: ΛN_{i}.S

val conv ; Δ; Γ ⊢⊢ A :: S ; Δ; Γ ⊢⊢ A : S

wobei bei den val typ-Regeln die N_{i} genau diejenigen Felder sind, die in ihrem Typ β als freie Typvariable enthalten.

\underline{Erklärung:}

Hiermit erkläre ich, daß ich diese Arbeit selbständig und nur mit den angegebenen Hilfsmitteln angefertigt habe. Ich bin damit einverstanden, daß der Betreuer meiner Diplomarbeit diese nach Abschluß der Prüfung zu wissenschaftlichen Zwecken weitergeben kann.

Darmstadt, im Juli 1997