Theorie und Implementation objektorientierter Programmiersprachen

Andreas Abel Ludwig-Maximilians-Universität

Rohfassung vom 20. August 2002

Skript zur Vorlesung Theorie und Implementation objektorientierter Programmiersprachen. Weiteres Material ist bereitgestellt unter

   http://www.tcs.informatik.uni-muenchen.de/~abel/OO/index.html.

Kommentare und Verbesserungsvorschläge bitte an abel@informatik.uni-muenchen.de.

Dieses Skript ist in Bearbeitung. Die Präsentation des Stoffes ist unvollständig und höchstwahrscheinlich fehlerbehaftet. Zitate verwandter Arbeiten fehlen. Bitte dieses Dokument nicht zitieren.

Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Andreas Abel \underline{ii}

Rohfassung vom 20. August 2002

Inhaltsverzeichnis

1 Einführung 1 1.1 Geschichte objektorientierter Programmierung . . . . . . . . . . 2 1.2 Wesentliche Konzepte der Objektorientierung . . . . . . . . . . . 2 1.3 Sicherheit durch formale Methoden . . . . . . . . . . . . . . . . . 2 1.4 Typ-Systeme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.5 Statische und dynamische Typprüfung . . . . . . . . . . . . . . . 3 1.6 Typprüfung für objekt-orientierte Sprachen . . . . . . . . . . . . 3 1.7 Ziel und Inhalt der Vorlesung . . . . . . . . . . . . . . . . . . . . 6

2 Ungetypte arithmetische Ausdrücke 9 2.1 Externe Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Interne Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.2.1 Induktiv definierte Mengen . . . . . . . . . . . . . . . . . 11 2.2.2 Rekursion über induktive Mengen . . . . . . . . . . . . . 13 2.2.3 Beweise durch Induktion . . . . . . . . . . . . . . . . . . . 14

2.3 Semantik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.1 Abstrakte Maschine . . . . . . . . . . . . . . . . . . . . . 15 2.3.2 Natürliche Semantik . . . . . . . . . . . . . . . . . . . . . 18

3 Getypte arithmetische Ausdrücke 19

4 Der ungetypte Lambda-Kalkül 21 4.1 Die λ-Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4.2 Syntax des reinen Lambda-Kalküls . . . . . . . . . . . . . . . . . 23 4.3 Operationale Semantik . . . . . . . . . . . . . . . . . . . . . . . . 23 4.4 Programmieren im Lambda-Kalkül . . . . . . . . . . . . . . . . . 25

4.4.1 Church-Booleans . . . . . . . . . . . . . . . . . . . . . . . 25 4.4.2 Paare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.4.3 Church-Ziffern . . . . . . . . . . . . . . . . . . . . . . . . 27 4.4.4 Divergenz . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.4.5 Funktionen mit mehreren Argumenten und Currying … 28

4.5 Formale Behandlung des Lambda-Kalküls . . . . . . . . . . . . . 29 5 Der getypte Lambda-Kalkül 33

5.1 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.2 Einfach-getypter λ-Kalkül . . . . . . . . . . . . . . . . . . . . . . 34

6 Erweiterungen des getypten Lambda-Kalküls 37 6.1 Der ein-elementige Typ . . . . . . . . . . . . . . . . . . . . . . . 37 6.2 Befehlssequenzen und let . . . . . . . . . . . . . . . . . . . . . . 37 6.3 Produkttypen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 6.4 Datensatztypen . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 6.5 Rekursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 6.6 Zusammenfassung . . . . . . . . . . . . . . . . . . . . . . . . . . 37

6.6.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 6.6.2 Auswertung mit Call-by-Value . . . . . . . . . . . . . . . 38 6.6.3 Typisierung . . . . . . . . . . . . . . . . . . . . . . . . . . 40

7 Referenzen 43

8 Untertypen 47 8.1 Subsumption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 8.2 Regeln der Untertyp-Beziehung . . . . . . . . . . . . . . . . . . . 48 8.3 Entscheidung der Untertyp-Beziehung . . . . . . . . . . . . . . . 48

9 Objekt-orientierte Programmierung 51 9.1 Objekte, Methoden . . . . . . . . . . . . . . . . . . . . . . . . . . 51 9.2 Konstruktor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 9.3 Subtyping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 9.4 Bündelung der Instanzen-Variablen . . . . . . . . . . . . . . . . . 52 9.5 Klassen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 9.6 Zusätzliche Instanzenvariablen . . . . . . . . . . . . . . . . . . . 53 9.7 self (ohne dynamische Bindung) . . . . . . . . . . . . . . . . . . 53 9.8 self (mit dynamischer Bindung) . . . . . . . . . . . . . . . . . 54

10 Featherweight Java 57

Literatur 59

Kapitel 1

Einführung

Objektorientierte Programmiersprachen haben sich einen festen Platz in professioneller Softwareentwicklung erobert. Herausragend sind die Sprachen C++, die eine Erweiterung des “Marktführers” C um objektorientierte Konstrukte darstellt, und JAVA, die besonders zur Entwicklung portabler und platformübergreifender Software verwendet wird. Beide Sprachen sind vergleichsweise jung. Die erste Definition von C++ war 1986 abgeschlossen, JAVA kam 1995 auf den Markt. Das Prinzip der Objektorientierung ist jedoch beinahe vierzig Jahre alt und findet sich bereits bei SIMULA 1 (1964) und Smalltalk (1972) [Zus99].

Ein Objekt, die Grundeinheit objekt-orientierter Programmiersprachen, ist eine Entität mit einem gewissen Verhalten, das durch seine Methoden bestimmt wird. Eine Liste von Methoden, über die ein Objekt gesteuert werden kann, wird als Schnittstelle (Interface) bezeichnet. Idealerweise spezifiziert diese Schnittstelle das Verhalten des Objekts unter Aufruf seiner Methoden. In realen Programmiersprachen ist jedoch meist nur für jede Methode der Typ gegeben, der angibt, wie die Methode syntaktisch korrekt benutzt werden kann. Es gibt jedoch Spezifikationssprachen wie z.B. die Unified Modelling Language (UML), oder Spracherweiterungen wie ESC JAVA [DLNS98], die eine teilweise Definition des Verhaltens ermöglichen.

Ein weiteres Kernkonzept in objektorientierten Programmiersprachen sind Klassen. Eine Klasse implementiert ein Schnittstelle; sie definiert die internen Datenelemente (Felder) von Objekten eben dieser Klasse und implementiert die Methoden der Schnittstelle. Jedes Objekt wird genau einer Klasse zugeordnet, kann aber mehreren Schnittstellen genügen. Zur Laufzeit eines objektorientierten Programmes muss klar sein, welcher Klasse ein bestimmtes Objekt angehört, um Aufrufe von Methoden dieses Objekts ausführen zu können. Die Klasse eines Objekts kann auch einfach als ihr Typ angesehen werden.

[ Bla bla... Hier folgen nun die Folien des ersten Vortrags. ]

2  Einführung

1.1 Geschichte objektorientierter Programmie-

rung

1. Vorläufer: SIMULA 1 (1964): Sprache für Simulationen.

2. Smalltalk (1972): Erste rein objektorientierte Sprache.

3. C++ (1986): Hybridsprache: Prozedural und objektorientiert.

4. JAVA (1995): Typsichere (?) OO-Sprache für platformunabhängige Anwendungen.

5. weitere: ObjectPascal, MODULA-3, Oberon …

1.2 Wesentliche Konzepte der Objektorientierung

Operationelle Konzepte:

1. Methoden und dynamische Bindung

2. Vererbung

3. Späte Bindung Sicherheitskonzepte:

4. Datenkapselung

5. Subtyping (Interfaces, Subclasses)

1.3 Sicherheit durch formale Methoden

• Anforderung an moderne Programmiersprachen: zur Verlässlichkeit und Robustheit von Software beitragen.

• Vollständige Korrektheitsbeweise durch formale Methoden sind sehr aufwendig und meist zu teuer.

• Schlanke formale Methoden: beschränken sich auf automatisch testbare

Eigenschaften von Programmen. 1. Typ-Systeme

2. Model-Checker

3. Laufzeitüberwachungssysteme

Rohfassung vom 20. August 2002

1.4 Typ-Systeme

• Definition (Benjamin Pierce [Pie02]):

A type system is a syntactic method for automatically proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute.

• Typsicherheit:

1. Jeder korrekte Programmausdruck hat einen Typ.

2. Der Typ eines Ausdrucks ändert sich durch Auswertung nicht.

3. Ein wohlgetypter Ausdruck erzeugt keine unerwarteten Laufzeitfeh-

ler.

• Slogan: Well-typed programs cannot go wrong.

1.5 Statische und dynamische Typprüfung

Statisch  Dynamisch
Typprüfung beim Übersetzen  zur Laufzeit
Vorteil Fehler früher erkannt Nur wirkliche Fehler
Nachteil  Korrekte Programme abgelehnt Fehler “schlummern”
Sprachen ML, Haskell LISP, Scheme
C, C++, JAVA  JAVA

Bemerkung: Nicht alle Sprachen mit Typprüfung sind auch typsicher. Unsicher sind z.B. C und C++.

1.6 Typprüfung für objekt-orientierte Sprachen

• Typsysteme für objekt-orientierte Sprachen sind kompliziert:

• Das Typ-System von JAVA ist stellenweise unnötig restriktiv.

• Beispiel: Cloning.

  interface Move {}
  /* A game board with undo */
  abstract class Board {
      Board prev;
      void copyFrom (Board board) {

Rohfassung vom 20. August 2002

    this.prev = board.prev;
}
abstract Board copy();
abstract void doMove (Move move);
void back () {
    this.copyFrom (this.prev);
}
void forward (Move move) {
    Board board = this.copy();
    this.prev = board;
    this.doMove (move);
}
}
class ChessBoard extends Board {
boolean turn; /* ... further instance variables */
ChessBoard () { /* initialize */ }
void copyFrom (ChessBoard chessBoard) {
    super.copyFrom (chessBoard);
    this.turn = chessBoard.turn; /* ... further code */
}
ChessBoard copy() {
    ChessBoard chessBoard = new ChessBoard();
    chessBoard.copyFrom (this);
    return chessBoard;
}
void doMove (Move move) { /* perform chess move */ }
}

Die abgeleitete Klasse ChessBoard kopiert auch sich selbst, deswegen sollte die Methode copy ein Objekt vom Typ ChessBoard zurückgeben. Dies scheitert jedoch am Compiler:

cloning.java:36: The method ChessBoard copy() declared in class
ChessBoard cannot override the method of the same signature
declared in class Board.  They must have the same return type.
ChessBoard copy() {
           ^
1 error

Eine akzeptierte Implementation von ChessBoard lautet:

class ChessBoard extends Board {
boolean turn; /* ... further instance variables */
ChessBoard () { /* initialize */ }
void copyFrom (Board chessBoard) {
    super.copyFrom (chessBoard);
    this.turn = ((ChessBoard)chessBoard).turn; /* ... further code */
}
Board copy() {
    ChessBoard chessBoard = new ChessBoard();
    chessBoard.copyFrom (this);
    return (Board)chessBoard;
}
void doMove (Move move) { /* perform chess move */ }
}

• Manchmal ist das operationelle Verhalten überraschend.

• Beispiel: Equality.

/* classes with equality */
class A {
int x;
A (int x) { this.x = x; }
boolean eq(A a) {
    return this.x == a.x;
}
}
class B extends A {
int y;
B (int x, int y) { super(x); this.y = y; }
boolean eq(B b) {
    return super.eq(b) && this.y == b.y;
}
}
class Eq {
public static void main (String[] args) {
    A a1 = new A(1);
    B b1 = new B(1,2);

if (a1.eq(b1)) System.out.println ("a1 = b1");
else System.out.println ("NOT a1 = b1");
if (b1.eq(a1))  System.out.println ("b1 = a1");
else System.out.println ("NOT b1 = a1");
}
}

Das Ergebnis verblüfft und ist bedingt durch overloading.

a1 = b1
b1 = a1

• Das Typ-System von JAVA enthält fehlerhafte Regeln.

• Beispiel: Arrays.

class A { }
class B extends A { void bla() { System.out.println("Class B blabla."); } }
class C {
A a = new A();
void assign (A[] v) {
v[0] = a;
}
public static void main (String[] args) {
C c = new C();
B[] v = new B[1];
c.assign (v);
v[0].bla();
}
}

Das Programm produziert einen Typfehler zur Laufzeit, obwohl es keine kritischen Casts enthält. Ursache ist eine fehlerhafte Typregel für Arrays.

Exception in thread "main" java.lang.ArrayStoreException
at C.assign(Compiled Code)
at C.main(Compiled Code)

1.7 Ziel und Inhalt der Vorlesung

Ziel: Beherrschung von Typsystemen für OO-Sprachen.

1. Theorie • Schrittweise Einführung in Typen und korrekte Typregeln.

• Beweis von Typsicherheit für zunehmend mächtigere Systeme.

2. Implementation • Umsetzen der theoretischen Erkenntnisse in funktionierende Typprüfer.

• Entwicklung eines typsicheren Interpreters für eine objektorientierte Sprache.

8  Einführung

Ungetypte arithmetische Ausdrücke

In diesem Kapitel führen wir eine simple “Programmiersprache” für Ganzzahlen und Zeichenketten ein. Die Sprache ist so rudimentär und hat den Namen Programmiersprache eigentlich nicht verdient. Sie hilft uns aber, wichtige Konzepte der formalen Behandlung von Programmiersprachen zu verdeutlichen.

In unserer Metasprache seinen die ganzen Zahlen 0, 1, -1, 2, -2, … und Zeichenketten "hallo", "bla", … vorhanden. Mit Metasprache meinen wir die Sprache, in der wir unsere Objektsprachen, d.h. die uns interessierenden Fragmente von objektorientierten Programmiersprachen, definieren und analysieren. Diese Metasprache ist die Sprache der Mathematik, und in einigen Fällen die Programmiersprache, die wir für die Implementation eines Interpreters oder Typprüfers verwenden. In diesem Kapitel benutzen wir Haskell [?].

In der Mathematik wird die Menge der ganzen Zahlen mit ℤ bezeichnet, die Menge der Zeichenkette bezeichnen wir mit 𝕊. In Haskell heißt der Typ der ganzen Zahlen Int und der Typ der Zeichenketten String. Für ganze Zahlen verwenden wir die Buchstaben i, j, k und für Zeichenketten s.

2.1 Externe Syntax

Die Sprache, die wir in diesem Kapitel vorstellen, behandelt einen kleinen Teil der gültigen Ausdrücke von JAVA. Dieser Teil kann durch folgende (BNF-ähn-liche) Grammatik beschrieben werden.

e ::= n  konstante ganze Zahl 0, 1, -1, …
| s  konstante Zeichenkette, z.B. "hallo"
| e_{1} + e_{2}  Addition
| e_{1} − e_{2}  Subtraktion
| e.length()  Länge der Zeichenkette e
| Integer.toString(e) Verwandlung der Zahl e in eine Zeichenkette

Beispiel 2.1 Folgende JAVA-Ausdrücke werden von der Grammatik erfasst.

5 + 4
"hallo".length() + 1
Integer.toString(753).length()
"hallo" + 1.length()

Dabei ist der letzte Ausdruck “unsinnig” und wird vom JAVA-Compiler zurückgewiesen. Wie man die sinnvollen von den unsinnigen Ausdrücken unterscheidet, werden wir in Kapitel ?? besprechen.

2.2 Interne Syntax

Um knapp und präzise über Programmausdrücke reden zu können, führt man eine interne oder abstrakte Syntax ein. Manchmal dient sie auch dazu, eine gedachte Programmiersprache zu definieren und zu analysieren, ohne sich über eine genaue Definition der Syntax den Kopf zerbrechen zu müssen.

t ::= n  konstante ganze Zahl
| s  konstante Zeichenkette
| t_{1} plus t_{2}  Addition
| t_{1} minus t_{2} Subtraktion
| len t  String-Länge
| str t  Verwandlung in Zeichenkette

Diese rekursive Definition der gültigen Terme t lässt sich in Haskell durch den folgenden rekursiven Datentyp beschreiben.

data Term = CInt Int
          | CStr String
          | Plus Term Term
          | Minus Term Term
          | Len Term
          | Str Term

Das Symbol Term bezeichnet den neuen Typ der Terme, den wir durch die sechs Klauseln definieren. Die Symbole CInt, CStr, Plus, Minus, Len und Str sind sogenannte Konstruktoren, durch die Ausdrücke vom Typ Term erzeugt werden können. In unserem Fall haben sie je ein bis zwei Argumente vom Typ Int, String oder Term. Die dritte Klausel z.B. ist so zuverstehen: sind t_{1} und t_{2} Ausdrücke vom Typ Term, so ist Plus t_{1} t_{2} wieder ein Ausdruck vom Typ Term.

Beispiel 2.2 Die JAVA-Ausdrücke aus dem letzten Bespiel lassen sich wie folgt in interne Syntax übersetzen und in Ausdrücke vom Typ Term übersetzen:

5 plus 4                    Plus (CInt 5) (CInt 4)
(len "hallo") plus 1        Plus (Len (CStr "hallo")) (CInt 1)
len (str 753)               Len (Str (CInt 753))
"hallo" plus (len 1)        Plus (CStr ("hallo")) (Len 1)

Wie aus den Beispielen deutlich geworden ist, betrachten wir Klammern zwar nicht als primären Bestandteil unserer internen Syntax, benutzen sie aber, um Ausdrücke zu disambiguieren. So ist z.B. die Struktur des Ausdrucks

                         1 minus 2 minus 3

nach unserer Grammatik nicht eindeutig; durch Klammersetzung entscheiden wir uns für eine der Möglichkeiten

                         1 minus (2 minus 3)

oder

                        (1 minus 2) minus 3.

2.2.1 Induktiv definierte Mengen

Die oben gegebene Grammatik der internen Syntax ist eine Kurzschreibweise für die folgende induktive Definition der Menge von Termen Tm.

Definition 2.1 (Terme, induktiv)

1. ℤ ⊆ Tm

2. 𝕊 ⊆ Tm

3. Sind t_{1}, t_{2} ∈ Tm, so auch t_{1} plus t_{2}, t_{1} minus t_{2} ∈ Tm.

4. Ist t ∈ Tm, so sind len t, str t ∈ Tm.

Diese Definition kann auch durch folgende Inferenzregeln ausgedrückt werden:

Definition 2.2 (Terme, durch Inferenzregeln)

{i ∈ ℤ \atop i ∈ Tm}  {s ∈ 𝕊 \atop s ∈ Tm}

t_{1} ∈ Tm t_{2} ∈ Tm
t_{1} plus t_{2} ∈ Tm

t_{1} ∈ Tm t_{2} ∈ Tm
t_{1} minus t_{2} ∈ Tm
{t ∈ Tm \atop len t ∈ Tm}  {t ∈ Tm \atop str t ∈ Tm}

Mit Hilfe dieser Inferenzregeln lassen sich Beweisbäume oder Herleitungen, generieren, die belegen, warum ein bestimmter Ausdruck t in Tm ist (bzw. wie er da “hereingekommen” ist). Dabei ist jede Regel so zu lesen: Wenn die Prämissen über dem Balken erfüllt sind, so gilt die Konklusion unter dem Balken.

Beispiel 2.3 Wir beweisen, das (len "hallo") plus 1 ein Term unserer Sprache ist.

                      "hallo" ∈ 𝕊
                     "hallo" ∈ Tm
                   len"hallo" ∈ Tm

1 ∈ ℤ 1 ∈ Tm

                     (len"hallo") plus 1 ∈ Tm

Genauso kann man beweisen, dass der unsinnige Ausdruck "hallo" plus (len 1) ∈ Tm.

Übung 2.1 Geben Sie eine Herleitung von (len (str "bla")) minus (5 plus 3) ∈ Tm an.

Die Menge Tm ist definiert als die kleineste Menge, die unter den Inferenzregeln abgeschlossen ist.

Wir können die Menge der Terme schrittweise von unten konstruieren, mit Hilfe der folgenden Definition.

Definition 2.3 (Terme, schrittweise) Für jede natürliche Zahl n, definiere eine Menge T_{n} wie folgt:

T_{0}  = ∅
T_{n+1} = ℤ ∪ 𝕊
∪ {t_{1} plus t_{2}, t_{1} minus t_{2} | t_{1}, t_{2} ∈ T_{n}}
∪ {len t, str t | t ∈ T_{n}}

Schliesslich sei T = ⋃_{n∈ℕ} T_{n} der Limes der Folge (T_{n})_{n∈ℕ}.

Übung 2.2 Geben Sie einen Ausdruck t an mit t ∈ T_{3} aber t ∉ T_{2}.

Satz 2.1 Die Mengen T_{n} sind kumulativ, d.h. T_{n} ⊆ T_{n+1} für beliebiges n ∈ ℕ.

Übung 2.3 Beweisen Sie Satz 2.1.

Die Konstruktion der Menge der Terme ist korrekt, d.h. T ist die kleinste Menge, die unter den Inferenzregeln in Definition 2.2 abgeschlossen ist.

Satz 2.2 T = Tm. Das entspricht:

1. T ist unter den Regeln in Def. 2.2 abgeschlossen.

2. Sei T′ unter den Inferenzregeln abgeschlossen. Dann T ⊆ T′.

Beweis.

1. Beispielhaft zeigen wir das t_{1} plus t_{2} ∈ T, falls t_{1}, t_{2} ∈ T. Nach Voraussetzung gibt es Indices n_{1}, n_{2} ∈ ℕ mit t_{1} ∈ T_{n_{1}} und t_{2} ∈ T_{n_{2}}. Sei n = max(n_{1}, n_{2}). Da die Folge (T_{m})_{m∈ℕ} kumulativ ist (Satz 2.1), sind t_{1}, t_{2} ∈ T_{n} und damit ist t_{1} plus t_{2} ∈ T_{n+1} ⊆ T.

2. Es genügt zu zeigen, dass für alle Indices n ∈ ℕ und alle Terme t ∈ T_{i} auch t ∈ T′ gilt. Wir beweisen diese Aussage durch vollständige Induktion über n.

Sei z.B. len t ∈ T^{n}. Dann ist n > 1 und t ∈ T_{n−1}. Nach Induktionsvoraussetzung ist t ∈ T′. Da T′ unter den Inferenzregeln abgeschlossen ist, gilt auch len t ∈ T′.

□

Übung 2.4 Vervollständigen Sie diesen Beweis für die noch nicht behandelten Fälle.

2.2.2 Rekursion über induktive Mengen

In unserer Metasprache können wir nun Funktionen definieren, die Terme manipulieren. Beispielweise eine Funktion | · | : Tm → ℕ, die die Größe eines Terms bestimmt. Wir definieren diese Funktion rekursiv, und durch Fallunterscheidung über die verschiedenen Termformen. Wir geben eine Definition in mathematischer Notation und eine in Haskell.

 | · |  : Tm → ℕ  size :: Term -> Int
 |i|  = 1  size (CInt i) = 1
 |s|  = 1  size (CStr s) = 1
 |t_{1} plus t_{2}| = 1 + |t_{1}| + |t_{2}| size (Plus  t1 t2) = 1 + size t1 + size t2
 |t_{1} minus t_{2}| = 1 + |t_{1}| + |t_{2}| size (Minus t1 t2) = 1 + size t1 + size t2
 | len t|  = 1 + |t|  size (Len t) = 1 + size t
 | str t|  = 1 + |t|  size (Str t) = 1 + size t

Diese Definition ist dadurch gerechtfertigt, dass eine rekursive Verwendung immer nur mit “kleinerem” Argument auftritt. In der Definition der Größe von t_{1} plus t_{2} z.B. wird sich nur auf die Größe der Subterme t_{1} und t_{2} bezogen. Diese Intuition können wir auch mathematisch präzise fassen. Wir definieren eine Folge von Funktionen (size_{n})_{n∈ℕ}:

size_{0}  : T_{0} → ℕ
…
size_{n+1} : T_{n+1} → ℕ verwendet size_{n} : T_{n} → ℕ
…

Jede dieser Funktion ist nicht rekursiv und approximiert die zu konstruierende Funktion | · | : T → ℕ, welche wir als Grenzwert der Folge erhalten.

Funktionen über Terme wie | · |, die sich selbst nur mit Subtermen als Argument aufrufen, nennt man auch strukturell rekursiv. Eine weitere strukturell rekursive Funktion berechnet die Höhe eines Terms.

height  : Tm → ℕ
height(i)  = 1
height(s)  = 1
height(t_{1} plus t_{2}) = 1 + max(height(t_{1}), height(t_{2}))
height(t_{1} minus t_{2}) = 1 + max(height(t_{1}), height(t_{2}))
height(len t)  = 1 + height(t)
height(str t)  = 1 + height(t)

Übung 2.5 Schreiben sie eine strukturell rekursive Funktion, die einen Ausdruck der internen Syntax in externe Syntax übersetzt.

2.2.3 Beweise durch Induktion

Es gibt drei Arten, beweise für Aussagen über Terme t zu führen:

1. Induktion über die Termhöhe height(t) ∈ ℕ.

2. Induktion über die Termgrösse |t| ∈ ℕ.

3. Strukturelle Induktion über die Konstruktion von t ∈ Tm. Alternative 3 vermeidet den Umweg über die natürlichen Zahlen und führt meistens zu einer klaren Beweisstruktur. Wann immer möglich, werden wir strukturelle Induktion verwenden. Satz 2.3 Für alle Terme t ∈ Tm gilt height(t) ≤ |t|. Beweis. Durch strukturelle Induktion über t ∈ Tm. Wir müssen nun alle sechs Fälle abhandeln: Fall t = i. Es gilt height(i) = 1 ≤ 1 = |i|. Fall t = s. Analog. Fall t = t_{1} plus t_{2}. Nach Induktionsvoraussetzung ist height(t_{n}) ≤ |t_{n}| für

n ∈ {1, 2}. Somit gilt

height(t) = 1 + max(height(t_{1}), height(t_{2})) ≤ 1 + |t_{1}| + |t_{2}| = |t|.

Fall t = t_{1} minus t_{2}. Analog. Fall t = len t′. Nach Induktionsvoraussetzung ist height(t′) ≤ |t′|. Damit auch

height(t) = 1 + height(t′) ≤ 1 + |t′| = |t|.

Fall t = str(t′). Analog. □ Übung 2.6 Beweisen Sie |t| ≤ 2^{height(t)} − 1 für alle Terme t ∈ Tm.

Rohfassung vom 20. August 2002

2.3 Semantik

Bis jetzt haben wir die Terme als reine syntaktische Objekte behandelt. Obwohl die Namen der Termkonstruktoren eine gewisse Bedeutung suggerieren, haben wir doch die Semantik nicht definiert.

Es gibt verschiedene Methoden, die Bedeutung von Programmkonstrukten mathematisch präzise zu erklären. Man unterscheidet zwischen

1. operationeller Semantik, welche für jeden Term beschreibt, wie er von einer abstrakten Maschine ausgewertet wird,

2. denotationeller Semantik, die Terme in mathematische Objekte übersetzt, und

3. axiomatischer Semantik, die das Programmverhalten durch logische Axiome beschreibt.

Wir werden uns ausschließlich mit der ersten Alternative befassen, da sie gleichzeitig einen Grundbaustein zur Implementation eines Interpreters darstellt.

In der Praxis findet man häufig eine von zwei weiteren Alternativen.

• Natürlich-sprachliche Semantik. Programmkonstrukte werden informell erklärt.

• Gar keine Semantik. Es gibt keine genaue Sprachbeschreibung. Die Bedeutung eines Programms ergibt sich, in dem man es kompiliert und ausführt.

Diese Ansätze haben entscheidende Schwächen: Falls keine genaue Spezifikation existiert, werden verschiedene Übersetzer ein- und dasselbe Programm mit großer Wahrscheinlichkeit leicht unterschiedlich interpretieren. Anwendungen, die unter einem Compiler entwickelt wurden, funktionieren mit einem anderen Compiler plötzlich nicht mehr. Die Programmiersprache ist nicht portabel.

2.3.1 Abstrakte Maschine

Wir definieren die Auswertung eines Programmausdrucks durch eine abstrakte Maschine. Die Maschine ist abstrakt in dem Sinne, dass wir konkrete Details ignorieren, z.B. wie Speicher repräsentiert ist etc. Das Ergebnis der Berechnung durch die Maschine ist ein Wert. In unserem Fall gibt es nur zwei verschiedene Kategorien von Werten.

v ::= i Ganzzahl-Konstante
| s String-Konstante

Der Zustand der Maschine wird vollständig bestimmt durch den Ausdruck, der gerade ausgewertet werden soll. Durch einen Auswertungsschritt wird die Maschine in den nächsten Zustand überführt, den wir wiederum durch einen Ausdruck charakterisieren. Die Zustandsübergangsrelation können wir daher als binäre Relation zwischen Termen schreiben.

t ⟶ t′ t wertet in einem Schritt zu t′ aus Welche Terme sollen wir nun in Relation zueinander setzen? Zuerst einmal definieren wir, wie sich unsere Operationen plus, minus, len, str auf Werten verhalten.

Definition 2.4 (Auswertungssemantik I: Berechnungsregeln)

\overline{E-PlusVV} i_{1} plus i_{2} ⟶ i_{3} wobei i_{3} die Zahl i_{1} + i_{2} bezeichnet

\overline{E-MinusVV} i_{1} minus i_{2} ⟶ i_{3} wobei i_{3} die Zahl i_{1} − i_{2} bezeichnet

\overline{E-LenV} ; len s ⟶ i_{s} wobei i_{s} die Länge von s bezeichnet

\overline{E-StrV} ; str i ⟶ s_{i} wobei s_{i} die Dezimalnotation von i bezeichnet

Einen Ausdruck t, der mit einer der Berechnungsregeln in einen Ausdruck t′ überführt werden kann (t ⟶ t′), nennt man Redex. Den Term t′ nennt man Redukt. In unserer Sprache sind Redices von der folgenden Form.

r ::= i_{1} plus i_{2}

                              | i_{1} minus i_{2}
                              | len s
                              | str i

Beispiel 2.4 Redices und ihre Redukte.

5 + 4  ⟶ 9

                      len"hallo" ⟶ 5
                      str 753  ⟶ "753"

Noch ungeklärt ist, wie z.B. der Ausdruck (5 plus 4) minus (4 plus 3) ausgewertet wird. Es fehlen noch Regeln, die angeben, was z.B. mit Termen t_{1} minus t_{2} passieren soll, wenn t_{1} oder t_{2} keine Werte sind. Im Prinzip haben wir im obigen Beispiel zwei Möglichkeiten:

   (5 plus 4) minus (4 plus 3) ⟶ 9 minus (4 plus 3) ⟶ 9 minus 7 ⟶ 2,

oder

   (5 plus 4) minus (4 plus 3) ⟶ (5 plus 4) minus 7 ⟶ 9 minus 7 ⟶ 2.

Wir könnten nun beide zulassen, dann wäre unsere Auswertung nicht-determi-nistisch. Wir bevorzugen jedoch eine deterministische Auswertungsstrategie, in der Fachliteratur under dem Namen left-most outer-most reduction oder head reduktion bekannt. Diese bearbeitet immer den Redex, der “am weitesten links” im Term bzw. im sogenannten Kopf (engl. head) des Termes steht. Die folgenden Regeln ermöglichen die Auflösung eines Redexes tief innerhalb eines Terms, jedoch nur des am weitesten links stehenden Redexes.

Definition 2.5 (Auswertungssemantik II: Kongruenzregeln)

t_{1} ⟶ t′_{1}
\overline{E-PlusTT}

t_{1} plus t_{2} ⟶ t′_{1} plus t_{2}

t ⟶ t′
\overline{E-PlusVT}

                                    i plus t ⟶ i plus t′

t_{1} ⟶ t′_{1}
\overline{E-MinusTT}

t_{1} minus t_{2} ⟶ t′_{1} minus t_{2}

t ⟶ t′
\overline{E-MinusVT}

                                      i minus t ⟶ i minus t′

t ⟶ t′
\overline{E-LenT}

           len t ⟶ len t′

t ⟶ t′
\overline{E-StrT}

                                   str t ⟶ str t′

Die Kongruenzregeln haben je eine Hypothese: Z.B. liest sich die Regel E-LenT folgendermaßen: Wenn die Maschine t in einem Schritt zu t′ auswerten könnte, dann ist der Übergang von len t nach len t′ auch möglich. Die Möglichkeit eines Auswertungsschrittes können wir durch eine Herleitung belegen, an deren Anfang eine Berechnungsregel steht, gefolgt von Kongruenzregeln.

Beispiel 2.5

\overline{E-StrV}

                    str 753 ⟶ "753"

\overline{E-LenT}

                len(str 753) ⟶ len"753"

\overline{E-PlusTT}

  len(str 753) plus (5 plus 4) ⟶ (len"753") plus (5 plus 4)

Übung 2.7 Für die folgenden Terme t, entscheiden Sie ob ein Auswertungsschritt zu einem Term t′ möglich ist. Wenn ja, geben Sie eine Herleitungen für t ⟶ t′ an.

  1. t = 5 minus ((len"hallo") plus (2 minus 3)).
  2. t = (len 753) plus (str"hallo").
  3. t = str((4 plus 1) minus (len"hallo")).

Definition 2.6 (Reduktion) Die durch die Berechnungs- und Kongruenzregeln definierte Relation ⟶ heißt Ein-Schritt-Reduktion oder Ein-Schritt-Auswertung und ist eine small-step semantics. Die Regeln nennen wir auch Reduktionsregeln.

Alle Terme t, die nicht mit irgeneinem anderen Term t′ in der Relation t ⟶ t′ stehen, können auch nicht weiter ausgewertet werden. Diese nennen wir Normalformen. Darunter fallen z.B. alle Werte v, aber auch unsinnige Terme wie

; minus 5.

Definition 2.7 (Normalform) Gibt es kein t′ mit t ⟶ t′ so ist t in Normalform.

Satz 2.4 Jeder Wert v ist in Normalform.

Beweis. Durch Überprüfen aller Auswertungsregeln. □ Unsere Auswertungsrelation ist in der Tat deterministisch.

Satz 2.5 (Auswertung ist deterministisch) Wenn t ⟶ t′ und t ⟶ t′′, dann ist t′ = t′′.

Beweis. Durch Induktion nach t ⟶ t′. □

[ Beweis ausführen. ]

Definition 2.8 (Mehr-Schritt-Reduktion) Wir definieren die Relationen:

⟶^{+} transitive Hülle von ⟶
⟶^{∗} reflexiv-transitive Hülle von ⟶

Übung 2.8 Definieren Sie ⟶^{+} und ⟶^{∗} durch Inferenzregeln. Dabei dürfen Sie ⟶ als gegeben voraussetzen.

Satz 2.6 (Mehr-Schritt-Auswertung ist deterministisch) Sei t ein Term und u, u′ Normalformen. Wenn t ⟶^{∗} u und t ⟶^{∗} u′, dann u = u′.

2.3.2 Natürliche Semantik

Im letzten Teil haben wir eine operationelle Semantik in Form einer smallstep Auswertungsrelation kennengelernt. Dabei wurden die einzelnen Schritte spezifiziert, die eine abstrakte Maschine durchführen kann, um einen Ausdruck in Normalform überzuführen. Alternativ kann man die Semantik auch natürlich bzw. in Form einer big-step Auswertungsrelation definieren. Diese Relation gibt direkt an, zu welchem Wert ein Term auswertet.

Definition 2.9 (Big-step Semantik) Die Auswertungsrelation t ⇓ v ist durch folgende Regeln gegeben.

\overline{B-Value} ; v ⇓ v

t_{1} ⇓ i_{1} t_{2} ⇓ i_{2}
\overline{B-Plus}
t_{1} plus t_{2} ⇓ (i_{1} + i_{2})

t_{1} ⇓ i_{1} t_{2} ⇓ i_{2}
\overline{B-Minus}
t_{1} minus t_{2} ⇓ (i_{1} − i_{2})
t ⇓ s ; \overline{B-Len} ; len t ⇓ i_{s}  t ⇓ i ; \overline{B-Str} ; str t ⇓ s_{i}

Dabei sind i_{s} und s_{i} wie oben definiert.

Für unsere Sprache sind small- und big-step Semantik äquivalent.

Satz 2.7 Sei t ein Term und v ein Wert.

1. Wenn t ⇓ v, dann t ⟶^{∗} v.

2. Wenn t ⟶^{∗} v, dann t ⇓ v.

Übung 2.9 Beweisen Sie Satz 2.7. Teil 1 geht direkt mittels struktureller Induktion; für Teil 2 müssen Sie erst die folgende Hilfsaussage beweisen:

Wenn t ⟶ t′ und t′ ⇓ v, dann t ⇓ v.

Getypte arithmetische Ausdrücke

[ Mitschrift von Cyril Bitterich: ]

Slogan ”well-typed programs do not go wrong”.

T ::= Int | String

Definition 3.1 Die Typisierungsrelation t : T ist gegeben durch folgende Schlussregeln (Inferenzregeln):

\overline{i:Int}T − Int _{\overline{s:String}} T − String \frac{t_{1}:Int t_{2}:Int}{t_{1} plus t_{t}2:Int}T − P lus \frac{t_{1}:Int t_{2}:Int}{t_{1} minus t_{2}:Int}T − Minus \frac{t:String}{t:Int} T − Len \frac{t:Int}{t:String} T − Str

Definition 3.2 Ein \underline{Typsystem} ist eine Term-/Programmiersprache zusammen mit einer Typisierungsrelation.

Definition 3.3 Ein Typsystem ist \underline{deterministisch}, wenn zu jedem Term t höchstens ein Typ T existiert mit t : T.

Definition 3.4 Ein Typsystem ist \underline{entscheidbar}, wenn ein Algorithmus existiert, der für jeden Term t und jeden Typ T entscheidet, ob t : T. Ein solcher Algorithmus heißt Typprüfungs- bzw. Type-Checking-Algorihmus.

Definition 3.5 Ein Algorithmus, der zu einem gegebenen Term t einen Typ T berechnet, heißt Typinferenz.

Beispiel 3.1 ^{\frac{^{\frac{\frac{\overline{′′hallo′′:String} T −String}{len′′hallo′′:Int} T −Len \overline{1:Int} T −Int}{(len′′hallo′′+1):Int}} T −P lus}{str(len′′hallo′′)+1):String}}T − Str

Definition 3.6 Ein Typsystem ist \underline{sicher}, falls es folgende zwei Eigenschaften besitzt.

1. Fortschritt (Progress). Ist ein Term wohlgetypt und kein Wert, so kann man ihn auswerten.

2. Typerhaltung (Preservation, Subject Reduction). Ist ein Term wohlgetypt, besitzt er nach Auswertung noch den selben Typ.

Satz 3.1 (Typerhaltung) Falls t : T und t → t′, dann t′ : T.

Beweis. Induktion über t : T.

Fall _{\overline{c:Int}}T − Int denn i ↛

Fall _{\overline{s:String}} T − String. s ↛

Fall \frac{t_{1}:Int t_{2}:Int}{t_{1} plus t_{2}:Int}T − P lus.

Unterfall \frac{t_{1}→t′_{1}}{t_{1}plust_{2}→t′_{1}plust_{2}} E − P lusT T \frac{t′_{1}:Int t_{2}:Int}{t′_{1}plust_{2}:Int}T − P lus

Unterfall \frac{t_{2} → t′_{2}}{i_{1} plus t_{2}→i_{2} plus t′_{2}} E − P lusV T Nach I.V. t′_{2} : Int Somit

\frac{_{\overline{i_{1}:Int}} T −Int t′_{2}:Int}{i_{1} plus t′_{2}:Int}T − P lus

Unterfall _{\overline{i_{1} plus i_{2}→(i_{1}+i_{2})}}E − P lusV V _{\overline{(i_{1}+i_{2}):Int}}T − Int

□

Satz 3.2 (Fortschritt) Falls t : T, dann entweder t = v oder t → t′

Der ungetypte Lambda-Kalkül

Fast alle Programmiersprachen stellen Konstrukte für Unterprogramme, Sub-Routinen, Prozeduren, Methoden oder Funktionen, um den Programmcode zu modularisieren und zu abstrahieren, um wiederkehrende Berechnungen nicht jedes Mal neu implementieren zu müssen. Die Abstraktion ermöglicht erst die Entwicklung grösserer Softwarepakete. Auch in der Mathematik sind die Konzepte Abstraktion und Funktionsbildung von essentieller Bedeutung.

Der Lambda-Kalkül ist eine syntaktische Theorie der Funktionenbildung und -anwendung. Er wurde in den 1920er Jahren von Alonzo Church und Mitarbeitern entwickelt ihm Rahmen der Formalisierung von mathematischen Grundlagen, und fand in der frühen höheren Programmiersprache LISP (ab 1950er, John McCarthy) Verwendung. Peter Landin benutze ihn in den 1960er Jahren als Kern-Programmiersprache, auf die sich alle anderen Programmkonstrukte zurückführen lassen. Einige Beispiele dazu werden wir in Teil 4.4 behandeln.

Heute ist der Lambda-Kalkül Grundlage von Programmiersprachentheorie und Implementation. Er ist Kern von funktionalen Sprachen wie Scheme, ML und Haskell und Teil von PIZZA, einer Erweiterung von JAVA. Er dient dem Studium von Variablenbehandlung, Bindung, Auswertungsstrategien und Typsystemen.

4.1 Die λ-Notation

In der Mathematik sehen wir Funktionen oft dadurch definiert, was bei ihrer Anwendung auf ein Argument zurückgegeben wird.

\begin{aligned}f(x) & = & a · x + b \\ f(0) & = & a · 0 + b \end{aligned}

Die Anwendung auf Argument 0 ist entsprechend direkt zu berechnen. Seltener wird die Funktion als eigenständiges Objekt definiert. Hier ist die Anwendung auf ein Argument eine Operation, die erklärt werden muss.

\begin{aligned}f & = & x ↦ a · x + b \\ f(0) & = & (x ↦ a · x + b)(0) = a · 0 + b \end{aligned}

Der Pfeil x ↦ t wird gelesen als “x wird abgebildet auf t”. Er erzeugt eine Funktion, indem er x im Ausdruck t abstrahiert. Der Vorteil dieser Notation ist, dass sie namenlose Funktionen erlaubt, die auch innerhalb eines größeren Ausdruckes vorkommen können, wie z.B. x ↦ a·x+b in der zweiten Zeile. Somit macht die ↦-Notation Funktionen zu “Bürgern erster Klasse”: Sie können so frei verwendet werden wie z.B. relle Zahlen und beliebig in Ausdrücken vorkommen.

Im Lambda-Kalkül schreibt man für die Abstraktion x ↦ t den Term λxt, daher der Name. Die Anwendung (oder Applikation) schreibt man durch Hintereinanderstellung ohne Klammerung des Arguments, also f 0 statt f(0).

\begin{aligned}f & = & λx(a · x + b) \\ f 0 & = & (λx(a · x + b)) 0 = a · 0 + b \end{aligned}

Funktionale Programmiersprachen kennen Notationen für anonyme Funktionen, die der mathematischen bzw. der des Lambda-Kalküls ähnlich sind.

    SML:      fn x => a * x + b
    Haskell:  \x -> a * x + b

Dabei ist der Schrägstrich \ die beste Approximation an ein λ im ASCII-Zeichensatz.

Um Klammern zu sparen, verwenden wir die Punkt-Notation. Ein Punkt “.” öffnet eine Klammer, die sich so weit rechts schließt wie syntaktisch möglich. Normalerweise wird der Punkt direkt hinter der abstrahierten Variable eingesetzt.

f = λx. a · x + b

Folgende drei Ausdrücke sind syntaktisch äquivalent.

(λx(x)) (λx(λf(f (x f))))
(λx x) (λxλf. f (x f))
λx x λxλf. f. x f

Der erste Ausdrück verwendet weder keine Punktnotation und auch nicht die Regel, dass λx … genau einen Ausdruck erwartet, in dem x abstrahiert wird. Zur Sicherheit wurden überall Klammern gesetzt, was die Lesbarkeit beeinträchtigt. Der zweite Ausdruck macht sich die Parsing-Regel für λ teilweise zunutze und verwendet die Punkt-Notation maßvoll. Der letzte Ausdruck hingegen macht vollen Gebrauch von Parsing-Regel und Punkt-Notation und spart alle Klammern ein, allerdings auf Kosten der Lesbarkeit. Wir werden den Punkt nur hinter einer Abstraktion verwenden wie im zweiten Ausdruck.

4.2 Syntax des reinen Lambda-Kalküls

Der reine Lambda-Kalkül kennt als alleinige Operationen Abstraktion und Applikation. Everything is a function.

Definition 4.1 ((Interne) Syntax) Die Terme t des ungetypten Lambda-Kalküls sind durch folgende Grammatik gegeben.

t ::= x  Variable
| λxt Abstraktion, Funktionskonstruktion, -einführung
| t_{1} t_{2} Applikation, Funktionsanwendung, -elimination

Die Abstraktion λxt bindet die Variable x. Variablen, die durch kein vorangestelltes λ gebunden werden, bezeichnen wir als frei. Eine präzise Definition folgt in Teil 4.5.

Beispiel  Freie Variablen Gebundene Variablen
λx. a · x + b  a, b  x
λx. y (λz. x z) y  x, z
λx. y (λy. x y) y  x, y

Tabelle 4.1: Beispiele für freie und gebundene Variablen.

Tabelle 4.1 zeigt einige λ-Terme mit freien und gebunden Variablen. Das letzte Beispiel λx. y (λy. x y) enthält y einmal frei, einmal gebunden. In diesem Fall sprechen wir von freien und gebundenen Vorkommen einer Variable.

Gebundene Variablen dürfen mit einem neuen Namen versehen werden, der in dem Term noch nicht vorkommt. Die Bedeutung des Terms ändert sich dabei nicht, und wir betrachten die entstehenden Terme sogar als syntaktisch gleich. Es gibt also keinen Unterschied zwischen λx x und λy y. Die Umbenennung von gebundenen Variablen bezeichnet man als α-Konversion und zwei Terme, die sich nur in den Namen der gebundenen Variablen unterscheiden, als αäquivalent. Solche Variablenumbenennungen sind auch aus der Integralrechnung bekannt, z.B.

(∫_{−∞}^{+∞} e^{−x^{2}}dx)^{2} = ∫_{−∞}^{+∞} e^{−x^{2}}dx ∫_{−∞}^{+∞} e^{−y^{2}}dy = ∫_{−∞}^{+∞} ∫_{−∞}^{+∞} e^{−x^{2}−y^{2}}dxdy

Die Integralnotation ∫ tdx bindet die Variable x. Sie kann also in y umbenannt werden.

4.3 Operationale Semantik

Die Ausführung der Anwendung einer Funktion auf ein Argument bezeichnet man als β-Reduktion. Z.B.

(λx. a · x + b) 0 ⟶ a · 0 + b Dabei mussten alle freien Vorkommen von x durch 0 ersetzt werden. Diese Operation bezeichen als Substitution und schreiben allgemein [s/x]t (lies “s für x in t). Hier ersetzen wir die freien Vorkommen von x in t durch s. Eine genaue Definition von Substitution folgt in Teil 4.5.

Definition 4.2 (β-Reduktion) Seien s, t λ-Terme und x eine Variable. Der Term (λxt) s) wertet in einem Schritt zu [s/x]t aus und wir schreiben

(λxt) s ⟶ [s/x]t.

Dabei bezeichnen wir (λxt) s als Redex (reducible expression) und [s/x]t als Redukt.

Definition 4.3 (β-Gleichheit) Zwei Terme t_{1} und t_{2} sind β-gleich (β-äqui-valent), in Zeichen t_{1} =_{β} t_{2}, falls man in t_{1} und t_{2} β-Reduktionen durchführen kann, so dass man Terme t′_{1} und t′_{2} erhält, die syntaktisch gleich sind t′_{1} = t′_{2}.

Ein Term kann nun viele Redexe enthalten, die entfernt werden müssen um die Normalform zu erreichen. Die Reihenfolge, in der Redexe entfernt werden, wird durch ein Auswertung-Strategie bestimmt.

Wir unterscheiden 4 Auswertungsstrategien:

Beispiel 4.1 \underline{(λxx) (\underline{(λxx)λz.\underline{(λxx)z}})} id = λxx

\underline{id(\underline{id λz.\underline{id z}})}  [figure: x λx; x λx; λx; z; app; λz; app; app]

A Strategien, die alle Redexe entfernen

1. Volle β-Reduktion (Redexe könne in beliebiger Reihenfolge bearbeitet werden.) Nicht deterministisch. z.B. id(id λz.\underline{id z}) ⟶ id(\underline{id λz.z}) ⟶ \underline{id(λz.z)} ⟶ λz.z

2. Normale Auswertung / Kopf- (head-)Reduktion/ Leftmost-outermost Entfernt den Redex, der am weitesten links-außen steht, zuerst. z.B. \underline{id(id λz. id z)} ⟶ \underline{id(λz. id z)} ⟶ λz.\underline{id z} ⟶ λz.z B Strategien, die nicht unter λ reduzieren

Rohfassung vom 20. August 2002

3. Call-by-name / lazy / verzögerte Auswertung Wie normale Auswertung; stoppt, wenn Wurzel des Termbaums eine Abstraktion. z.B. \underline{id(id λz. id z)} ⟶ \underline{id λz. id z} ⟶ λz. id z

4. Call-by-value / strict / eager / Applikative Reihenfolge Zuerst wird Argument ausgewertet, dann in Funktion eingesetzt. id(\underline{id λz. id z}) ⟶ \underline{id λz. id z} ⟶ λz. id z

Beispiel 4.2 power3(x) = x · x · x

power3(100!) ⟶^{cbn} 100! · 100! · 100!

power3(100!) ⟶^{cbv} v · v · v(v = 100!)

ignore(x) = false

ignore(100!) =⟶^{cbn} false

ignore(100!) =⟶^{cbv} false(v = 100!)

4.4 Programmieren im Lambda-Kalkül

Der Lambda-Kalkül ist eine Turing-vollständige Programmiersprache, d.h. jede berechenbare Funktion lässt sich im Lambda-Kalkül repräsentieren. Weitere Beispiele für Turing-mächtige Sprachen sind Turing-Maschinen, WHILEund GOTO-Sprachen, die Peano-Arithmetik, kombinatorische Algebren, jede vernünftige Programmiersprache, aber auch z.B. das Textsatzsystem TEX und die Seitenbeschreibungssprache POSTSCRIPT.

Im Folgenden werden wir einige elementare Datentypen und die wichtigsten Anwendungen dieser Datentypen im Lambda-Kalkül definieren.

4.4.1 Church-Booleans

Die ersten Datenobjekte, den wir betrachten, sind die Wahrheitswerte true und false und ihre Verwendung mit if. Da im Lambda-Kalkül “alles Funktion” ist, müssen wir die drei Konstrukte durch Funktionen realisieren. Wollen wir Datentypen im Lambda-Kalkül repräsentieren, müssen wir folgende Schlüssel-Frage beantworten:

Wie kann ein Objekt des betrachteten Typs verwendet werden?

Es geht also nicht um die Konstruktion (Einführung), sondern um die Verwendung (Elimination) eines Datenobjekts. Ein Datenobjekt im Lambda-Kalkül wird bestimmt durch seine Verwendungsmöglichkeiten.

Ein Wahrheitswert steht für eine Entscheidung, welche von zwei alternativen Berechnungen fortgesetzt werden soll. Das aus Programmiersprachen bekannte if-then-else ist also die allgemeinste Verwertung eines boolschen Wertes. Alle anderen Funktionen, wie z.B. logische Verknüpfungen, können mit Hilfe von if ausgedrückt werden.

Der Wert true ist eine Funktion, die angewandt auf zwei Berechnungen, den then-Zweig und den else-Zweig, stets den then-Zweig wählt. Der Wert false verfolgt immer den else-Zweig.

true = λtλe. t
false = λtλe. e
if  = λbλtλe. b t e

Der Destruktor if tut nichts Besonderes, er wendet den übergebenen Wahrheitswert b auf t, denn then-Zweig, und e, den else-Zweig an. Die Negationsfunktion können wir nun wie folgt definieren:

                    not = λb. if b false true

Die Definition is korrekt, wie aus den folgenden Auswertungssequenzen ersichtlich:

        not true = (λb. if b false true) true
        ⟶ if true false true = (λbλtλe. b t e) true false true
        ⟶ (λtλe. true t e) false true
        ⟶ (λe. true false e) true
        ⟶ true false true = (λtλe. t) false true
        ⟶ (λe. false) true ⟶ false
        not false = (λb. if b false true) false
        ⟶^{4} (false false true) = (λtλe. e) false true
        ⟶^{2} true

Die Funktion not kann noch knapper definiert werden durch den Term λb. b falsetrue, welcher sich auch ergibt, wenn man die ursprüngliche Definition normalisiert. Auch folgende Definition ist denkbar:

not = λbλtλe. b e t

Boolsche Funktionen lassen sich durch (geschachtelte) if-Ausdrücke implementieren. Deswegen sind sie auch im Lambda-Kalkül problemlos kodierbar. Z.B. Konjunktion:

                      and = λbλc. b c false

Der Ausdruck and b c liesst sich: Wenn b, dann c, sonst falsch.

4.4.2 Paare

Ein Paar ist der Zusammenschluss zweier Komponenten. Bei der Elimination eines Paares erhälten wir eine der Komponenten zurück. (Wollen wir beide Komponenten, müssen wir das Paar zweimal verwenden.) Welche der beiden Komponenten wir erhalten wollen, geben wir durch einen Wahrheitwert an. Ein Paar ist also eine Funktion, die ein Bit erwartet und eine Komponente zurückliefert.

                pair = λc_{true}λc_{false}λb. b c_{true} c_{false}
                fst = λp. p true
                snd = λp. p false

Die Selektoren fst und snd tun nichts weiter, als entweder die Nachricht true oder false an das Paar p zu übergeben. Wieder sind also alle Verwendungsmöglichkeiten im Konstruktor pair enthalten. Korrektheit wird ersichtlich durch die Reduktionsfolgen:

fst (pair t_{1} t_{2}) = (λp. p true) (pair t_{1} t_{2})

     ⟶ (pair t_{1} t_{2}) true = (λc_{true}λc_{false}λb. b c_{true} c_{false}) t_{1} t_{2} true

⟶^{3} true t_{1} t_{2} ⟶^{2} t_{1}
snd (pair t_{1} t_{2}) = (λp. p false) (pair t_{1} t_{2})
⟶^{4} false t_{1} t_{2} ⟶^{2} t_{2}

4.4.3 Church-Ziffern

Auch unendliche Datentypen wie die natürlichen Zahlen lassen sich im Lambda-Kalkül repräsentieren. (Dabei ist jede Zahl ein endliches Gebilde.) Eine natürliche Zahl n gibt allgemein an, wie oft eine Prozedur ausgeführt wird bzw. eine Funktion angewendet wird. Die Repräsentation der Zahl n im Lambda-Kalkül, die Church-Ziffer \underline{n} ist also eine Funktion, die eine beliebige Funktion f als Argument nimmt und n-mal iteriert. Dabei ist 0-fache Iteration die Identität. Die n-te Iterierte einer Funktion f können wir allgemein so definieren.

\begin{aligned}f^{0} & = & λx. x \\ f^{n+1} & = & f ∘ f^{n} = λx. f (f^{n} x) \end{aligned}

Damit erhalten wir die Church-Ziffern nach folgendem Schema:

\underline{0} = λfλx. x
\underline{1} = λfλx. f x
\underline{2} = λfλx. f (f x)
⋮
\underline{n} = λfλx. f^{n} x

Die Applikation \underline{n} f einer Church-Ziffer ist also f^{n}. Tabelle 4.2 listet einige einfache Funktionen über natürlichen Zahlen auf.

Die Vorgänger-Funktion pred mit pred\underline{n} = \underline{n − 1} ist nicht direkt implementierbar. Man benötigt Paare.

               x  = pair \underline{0} \underline{0}
               f  = λp. pair (snd p) (succ (snd p))
               pred = λn. fst (n f x)

Übung 4.1 Definieren Sie Multiplikation mult auf Church-Ziffern.

Funktion Beschreibung Spezifikation  Implementation
succ  Nachfolger  succ \underline{n} = \underline{n + 1}  λnλfλx. f (n f x)
add  Addition  add \underline{n} \underline{m} = \underline{n + m}  λnλmλfλx. n f (m f x)

 iszero Test auf 0  iszero \underline{0} = true  λn. n (λ . false) true
                        iszero \underline{n + 1} = false

Tabelle 4.2: Funktionen über natürliche Zahlen.

Übung 4.2 Definieren Sie Exponentiation exp auf Church-Ziffern.

Übung 4.3 Definieren Sie Subtraktion sub und euklidische Division^{1} div auf Church-Ziffern.

4.4.4 Divergenz

Nicht alle Terme des ungetypten Lambda-Kalküls lassen sich auf Normalform reduzieren. Einfachstes Beispiel für einen divergenten Term ist Ω = (λx. x x) (λx. x x), der durch Selbstanwendung entsteht. Ω ist invariant unter Reduktion:

Ω = (λx. x x) (λx. x x) ⟶ [λx. x x/x](x x) = (λx. x x) (λx. x x) = Ω

4.4.5 Funktionen mit mehreren Argumenten und Currying

Funktionen mit mehreren Argumenten (z.B. pair, add) haben wir mit Hilfe von mehrfacher Lambda-Abstraktion definiert. Streng genommen ist z.B. pair eine Funktion, die die erste Komponente als Argument nimmt und eine Funktion zurückgibt, die wieder ein Argument, die zweite Komponente, erwartet, und dann ein Paar erzeugt. Diese Darstellung hat den Vorteil, dass man pair auch teilweise anwenden kann. So kann man eine Funktion pair0 definieren, die nur ein Argument t erwartet und dann ein Paar mit konstanter erster Komponente \underline{0} und zweiter Komponente t erzeugt.

 pair0 = pair \underline{0} = (λc_{true}λc_{false}λb. b c_{true} c_{false}) \underline{0} ⟶ λc_{false}λb. b \underline{0} c_{false}

pair0 t = (λc_{false}λb. b \underline{0} c_{false}) t ⟶ λb. b \underline{0} t =_{β} pair \underline{0} t

Im Fall von Paaren mag das nicht besonders sinnvoll sein, aber nehmen wir an, wir hätten eine Exponentiationsfunktion power definiert mit

                      power \underline{n} \underline{m} = \underline{m^{n}}

power  = λnλm …

1Das ist herkömmliches Teilen mit Rest, wie aus der Grundschule bekannt.

Rohfassung vom 20. August 2002

Dann können wir Quadratur sqr \underline{n} = \underline{n^{2}} sehr knapp definieren durch teilweise Applikation von power:

                           sqr = power \underline{2}

Eine Funktion, die teilweise Applikation erlaubt, nennt man gecurryt (nach Haskell Curry).

Alternativ können wir im Lambda-Kalkül Funktionen mit mehreren Argumenten über Paare definieren, z.B. die Additionsfunktion

add = λp. λfλx. (fst p) f ((snd p) f x)

add (pair n m) ⟶ λfλx. fst (pair n m) f (snd (pair n m) f x)
⟶^{2} λfλx. n f (m f x)

Im Lambda-Kalkül sieht diese Variante etwas umständlich aus, jedoch ist dies in den meisten Programmiersprachen die gängige Form. Etwas eleganter wird sie mit der gebräuchlichen Notation (a_{1}, …, a_{n}) für n-Tupel. Im SML können wir add dann folgendermaßen implementieren.

    add = fn (n, m) => fn f => fn x => n f (m f x)

Das Transformieren einer über Tupel definierte Funktion mit mehreren Argumenten in eine mit iterierter λ-Abstraktion nennt man currying, die Gegentransformation uncurrying.

Übung 4.4 Definieren Sie eine λ-Funktion curry, die eine Funktion f als Argument nimmt, welche wiederum ein Paar von Argumenten erwartet, und eine Funktion zurückliefert, die zwei einzelne Argumente erwartet, aber sonst das Gleiche leistet wie f.

Übung 4.5 Definieren Sie auch eine Funktion uncurry.

4.5 Formale Behandlung des Lambda-Kalküls

Nach dem wir gesehen haben, was wir im Lambda-Kalkül programmieren können, wollen wir den Lambda-Kalkül von außen betrachten und schon benutzte Begriffe wie freie Variable und Substitution präzisieren. Die folgende Definition erfasst wohlgeformte Terme des ungetypten Lambda-Kalküls.

Definition 4.4 (Terme des ungetypten Lambda-Kalküls) Sei V eine abzählbare^{2} Menge für Namen von Variablen. Die Menge Tm der wohlgeformten Terme ist die kleinste Menge, die unter folgenden Regeln abgeschlossen ist:

1. Wenn x ∈ V, dann x ∈ Tm.

2. Wenn x ∈ V und t ∈ Tm, dann λxt ∈ Tm.

3. Wenn t_{1} ∈ Tm und t_{2} ∈ Tm, dann t_{1} t_{2} ∈ Tm.

2Abzählbar impliziert immer unendlich.

Rohfassung vom 20. August 2002

Die Menge der freien Variablen eines Terms lässt sich durch die folgende strukturell rekursive Funktion implementieren.

Definition 4.5 (Freie Variablen) Für t ∈ Tm bezeichnet FV(t) ⊆ V die Menge der freien Variablen von t.

FV(x)  = {x}
FV(λxt) = FV(t) \ {x}
FV(t_{1} t_{2}) = FV(t_{1}) ∪ FV(t_{2})

Nachdem wir Substitution schon intuitiv verwendet haben, wollen wir sie jetzt formal definieren. Um in einem Termbaum t eine Variable x durch einen Term s zu ersetzen, müssen wir in t alle mit x bezeichneten Blätter finden und anstatt ihrer s einhängen. Die Substitutionsfunktion verfährt natürlicherweise also durch Rekursion über t. Hier eine erste Definition:

[s/x]x  = s
[s/x]y = y x ≠ y
[s/x]λyt  = λy. [s/x]t
[s/x](t_{1} t_{2}) = ([s/x]t_{1}) ([s/x]t_{2})

Der Fall λyt hat noch zwei Schwachstellen. Erstens, auch gebundene Variablen werden ersetzt (falls y = x), z.B.

[z/x]λx x = λx. [z/x]x = λx z

Die Bedeutung dieses Terms hat sich geändert, eine gebundene Variable ist plötzlich frei geworden. Der umgekehrte Fall kann auch eintreten, es können freie Variablen in s “eingefangen” werden (engl. variable capture), z.B.

[x/z]λx. z x = λx([x/z]zx) = λx. x x

Beide Probleme können behoben werden, wenn wir bei der Substitution die gebundene Variable y durch eine frische Variable y′ ersetzen, die weder in s noch in t vorkommt. Solche neuen Variablen sind immer verfügbar, da wir eine unendliche Variablenmenge V zugrunde gelegt haben. Außerdem ändert sich gemäß α-Regel die Bedeutung des Termes nicht. Nun also die verbesserte Definition der Substitution.

Definition 4.6 (Substitution) Für Terme s, t ∈ Tm und eine Variable x ∈ V bezeichnet [s/x]t ∈ Tm den Term, der durch Ersetzung aller freien Vorkommen von x in t entsteht.

[s/x]x  = s
[s/x]y = y x ≠ y
[s/x]λyt  = λy′. [s/x][y′/y]t y′ neue Variable
[s/x](t_{1} t_{2}) = ([s/x]t_{1}) ([s/x]t_{2})

Falls in der dritten Zeile x = y, kann t keine freien Vorkommen von x enthalten, die substituiert werden müssten. An dieser Stelle kann man die Substitution beenden. Außerdem, falls y ≠ x und y ∉ FV(s), kann man sich das Umbennenen sparen. Damit ergeben sich folgende Optimierungen:

[s/x]λxt = λxt
[s/x]λyt = λy. [s/x]t falls y ≠ x und y ∉ FV(s)

Der getypte Lambda-Kalkül

[ Hier behandeln wir Teile 9.1-9.3 aus Pierce [Pie02]. Ich bin Cyril Bitterich sehr verbunden, der die folgende Mitschrift (und weitere) zur Verfügung gestellt hat. ]

5.1 Booleans

t ::= true | false | if t_{1} then t_{2} else t_{3} v ::= true | false

Berechnungs-Regeln:

\overline{E-IfTrue}

               if true then t_{2} else t_{3} ⟶ t_{2}

\overline{E-IfFalse}

               if false then t_{2} else t_{3} ⟶ t_{3}

Kongruenz-Regel:

t_{1} ⟶ t′_{1}
\overline{E-If}

           if t_{1} then t_{2} else t_{3} ⟶ if t′_{1} then t_{2} else t_{3}

Typisierung:

             \overline{T-True} true : Bool \overline{T-False} false : Bool

t_{1} : Bool  t_{2} : T  t_{3} : T
\overline{T-If}

                    if t_{1} then t_{2} else t_{3} : T

5.2 Einfach-getypter λ-Kalkül

Beispiel 5.1 λxt : Fun (λxx)true : Bool (λxλyy)true : Fun (Hier sind (λxx) und (λxλyy) vom Typ Fun)

λxx : Bool → Bool λxx : Int → Int λxλyy : Bool → (Bool → Bool) λxλyy : Bool → Int → Int)

T_{1} → (T_{2} → T_{3}) : Typ von Funktionen, die ein Argument vom Typ T_{1} erwarten und eine Funktion vom Typ T_{2} → T_{3} zurückliefern. (T_{1} → T_{2}) → T_{3} : Typ der Funktionen, die eine Funktion vom Typ T_{1} → T_{2} als Argument erwarten und etwas vom Typ T_{3} zurückliefern.

f : R → R λxx : A → A SML: (fnx ⇒ x) :′ a →′ a x ↦ sin(2x) f = λx.sin(2x) : R → R λx : Bool.x : Bool → Bool

\underbrace{λx : Int.x}_{t} : \underbrace{Int → Int}_{T}

Definition 5.1 Syntax des reinen einfach getypten Lambda-Kalküls (λ^{→})

Terme: t :: = x | λ x : T t

| t_{1} t_{2}

Typen: T ::= T → T

Kontexte: T :: = . leerer Kontext | Γ , x: T erweiterter Kontext

λx : Bool λy : Int x : Bool → Int → Bool

λy : Int x : Int → Bool

x : Bool

\frac{\frac{_{\overline{x:Bool,y:Int⊢x:Bool}} T −V AR}{x:Bool⊢λy:Int x:Int→Bool}T − LAM}{⊢ λx : Bool λy : Int x : Bool → Int → Bool} T − LAM

\frac{Γ ⊢ t_{1} : T′ → T Γ ⊢ t_{2} : T′}{Γ ⊢ t_{1} t_{2} : T}

Definition 5.2 Typisierungs-Relation Γ ⊢ t : T “Im Kontext Γ hat t den Typ T ”.

\frac{x : T ∈ Γ}{Γ ⊢ x : T}T − V ar

5.2 Einfach-getypter λ-Kalkül  35

\frac{Γ, x : S ⊢ t : T}{Γ ⊢ λx : S.t : S → T} T − LAM

\frac{Γ ⊢ t : S → T Γ ⊢ s : S}{Γ ⊢ ts : T} T − AP P

Definition 5.3 (λ^{→,Bool}) Der Kalkül λ^{→,Bool} entsteht durch Hinzunehmen von Booleans zu λ^{→}

Beispiel 5.2

In λ^{→,Bool} gibt es folgende Typen: Rang Bool 0 Bool → Bool, Bool → Bool → Bool 1 “first-order” (Bool → Bool) → Bool, ... 2 ↓ ((Bool → Bool) → Bool) → Bool 3 “higher-order”

Definition 5.4 (Rang, Ordnung) rk(Bool) = 0 rk(T_{1} → T_{2}) = max(rk(T_{1}) + 1, rk(T_{2}))

Nun interessiert uns auch wieder die Frage der Typsicherheit: Dafüer benötigen wir auch wieder:

Definition 5.5 Auswertung cbv für geschlossene Terme \underline{Werte} v ::= λx : S.t

\overline{(λx : S.t)v → [v/x]t}E − BetaV

\frac{t_{1} → t′_{1}}{t_{1}t_{2} → t′_{1}t_{2}} E − AppT

\frac{t → t′}{vt → vt′} E − AppV

Satz 5.1 Fortschritt Wenn ⊢ t : T , dann t → t′ oder t = v.

Lemma 5.1 Inversion, Erzeugung, Generation

1. Wenn Γ ⊢ x : T, dann x : T ∈ T

2. Wenn Γ ⊢ λx : S.t : R, dann R = S → T und Γ, x : S ⊢ t : T

3. Wenn Γ ⊢ t_{1}t_{2} : T, dann Γ ⊢ t_{1} : S → T für ein S und T ⊢ t_{2} : S 4. Wenn Γ ⊢ true : T , dann T = Bool

5. Wenn Γ ⊢ false : T , dann T = Bool

6. Wenn Γ ⊢ if t_{1} then t_{2} else t_{3} : T , dann Γ ⊢ t_{1} : Bool und Γ ⊢ t_{2} : T, Γ ⊢ t_{3} : T

Beweis. Durch Fallunterscheidung über die Typherleitung. □

Erweiterungen des getypten Lambda-Kalküls

6.1 Der ein-elementige Typ 6.2 Befehlssequenzen und let 6.3 Produkttypen 6.4 Datensatztypen 6.5 Rekursion 6.6 Zusammenfassung

6.6.1 Syntax

Typen.

T ::= T_{1} → T_{2} Funktionstyp
| Int  Typ der Ganzzahlen
| Bool  Typ der Wahrheitswerte
| Unit  Ein-elementiger Typ
| T_{1} × T_{2}  Produkttyp
| \begin{cases}−⇀ \\ l:T \end{cases}\}  Datensatz-Typ

Rohfassung vom 20. August 2002

Terme.

t ::= x | λx:T t | t_{1} t_{2}  Variablen, Funktionen, Anwendung
| i | t_{1} + t_{2} | t_{1} − t_{2} | iszero t  Ganzzahl-Konstanten, Addition, Subtraktion, Test auf 0
| true | false | if t_{1} then t_{2} else t_{3} Wahrheitswerte, Fallunterscheidung
| ()  Leeres Tupel
| (t_{1}, t_{2}) | t.1 | t.2  Paarbildung und Projektionen
| {l_{1} =t_{1}, …, l_{n} =t_{n}} | t.l  Datensatz und Projektion
| let x=t_{1} in t_{2}  Lokale Variablen
| fix f:T t  Rekursion

Werte.

v ::= λx:T t  Funktionen
| i  Ganzzahl-Konstanten
| true | false  Wahrheitswerte
| ()  Leeres Tupel
| (v_{1}, v_{2})  Paar von Werten
| {l_{1} =v_{1}, …, l_{n} =v_{n}} Datensatz von Werten

6.6.2 Auswertung mit Call-by-Value

Einzelschritt-Auswertung.

t ⟶ t′

Lambda-Kalkül Berechnung.

\overline{E-Beta} ; (λx:T t) v ⟶ [v/x]t

Kongruenz.

t_{1} ⟶ t′_{1} ; \overline{E-AppTT} ; t_{1} t_{2} ⟶ t′_{1} t_{2}  t ⟶ t′ ; \overline{E-AppVT} ; v t ⟶ v t′

Ganzzahlen Berechnung.

i_{3} = i_{1} + i_{2} ; \overline{E-PlusVV} ; i_{1} + i_{2} ⟶ i_{3}  i_{3} = i_{1} − i_{2} ; \overline{E-MinusVV} ; i_{1} − i_{2} ⟶ i_{3}

E-IsZeroTrue

 iszero 0 ⟶ true

i ≠ 0

E-IsZeroFalse

                                  iszero i ⟶ false

Kongruenz.

t_{1} ⟶ t′_{1} ; \overline{E-PlusTT} ; t_{1} + t_{2} ⟶ t′_{1} + t_{2} t_{1} ⟶ t′_{1}

\overline{E-MinusTT}
t_{1} − t_{2} ⟶ t′_{1} − t_{2}

t ⟶ t′ ; \overline{E-PlusVT} ; i + t ⟶ i + t′ t ⟶ t′

\overline{E-MinusVT}
i − t ⟶ i − t′
t ⟶ t′
\overline{E-IsZero}

                   iszero t ⟶ iszero t′

Rohfassung vom 20. August 2002

Wahrheitswerte Berechnung.

\overline{E-IfTrue}

               if true then t_{2} else t_{3} ⟶ t_{2}

\overline{E-IfFalse}

               if false then t_{2} else t_{3} ⟶ t_{3}

Kongruenz.

t_{1} ⟶ t′_{1}
\overline{E-If}

           if t_{1} then t_{2} else t_{3} ⟶ if t′_{1} then t_{2} else t_{3}

Leeres Tupel Keine Auswertungsregeln.

Paare Berechnung.

E-PairBeta_{1}

(v_{1}, v_{2}).1 ⟶ v_{1}

E-PairBeta_{2}

(v_{1}, v_{2}).2 ⟶ v_{2}

Kongruenz.

t_{1} ⟶ t′_{1} ; \overline{E-PairTT} ; (t_{1}, t_{2}) ⟶ (t′_{1}, t_{2})  t ⟶ t′ ; \overline{E-PairVT} ; (v, t) ⟶ (v, t′)
t ⟶ t′ ; \overline{E-Proj_{1}} ; t.1 ⟶ t′.1  t ⟶ t′ ; \overline{E-Proj_{2}} ; t.2 ⟶ t′.2

Datensätze Berechnung.

E-RecordBeta

\begin{cases}−⇀ \\ l =v \end{cases}\}.l_{i} ⟶ v_{i}

Kongruenz.

t ⟶ t′
\overline{E-Record}

\begin{cases}−⇀ \\ l =v \end{cases}, l′ =t, \begin{matrix}−⇀ \\ l′′ =t′′ \end{matrix}\} ⟶ \begin{cases}−⇀ \\ l =v \end{cases}, l′ =t′, \begin{matrix}−⇀ \\ l′′ =t′′ \end{matrix}\}

t ⟶ t′ ; \overline{E-Proj} ; t.l ⟶ t′.l

Lokale Variablen Berechnung.

\overline{E-LetBeta}
let x=v in t ⟶ [v/x]t

Kongruenz.

t_{1} ⟶ t′_{1}
\overline{E-Let}
let x=t_{1} in t_{2} ⟶ let x=t′_{1} in t_{2}

Rohfassung vom 20. August 2002

Rekursion Berechnung.

\overline{E-Fix}

fix f:T t ⟶ [fix f:T t/f]t

6.6.3 Typisierung

Kontexte.

Γ ::= ·  leerer Kontext
| Γ, x:T erweiterter Kontext

Typisierungsrelation.

Γ ⊢ t : T

Lambda-Kalkül

(x:T) ∈ Γ ; \overline{T-Var} ; Γ ⊢ x : T

Einführung.

Γ, x:S ⊢ t : T
\overline{T-Lam}
Γ ⊢ λx:S t : S → T

Beseitigung.

Γ ⊢ t : S → T Γ ⊢ s : S
\overline{T-App}
Γ ⊢ t s : T

Ganzzahlen Einführung.

\overline{T-Int} ; Γ ⊢ i : Int

Beseitigung. Γ ⊢ t_{1} : Int Γ ⊢ t_{2} : Int

\overline{T-Plus}
Γ ⊢ t_{1} + t_{2} : Int

Γ ⊢ t_{1} : Int Γ ⊢ t_{2} : Int
\overline{T-Minus}
Γ ⊢ t_{1} − t_{2} : Int
Γ ⊢ t : Int
\overline{T-IsZero}

                    Γ ⊢ iszero t : Bool

Wahrheitswerte Einführung.

\overline{T-True}

          Γ ⊢ true : Bool

\overline{T-False}

                                  Γ ⊢ false : Bool

Beseitigung.

Γ ⊢ t_{1} : Bool Γ ⊢ t_{2} : T Γ ⊢ t_{3} : T
\overline{T-If}

                  Γ ⊢ if t_{1} then t_{2} else t_{3} : T

Rohfassung vom 20. August 2002

6.6 Zusammenfassung  41

Leeres Tupel Einführung.

\overline{T-Unit} ; Γ ⊢ () : Unit

Keine Beseitigung. Paare Einführung.

Γ ⊢ t_{1} : T_{1} Γ ⊢ t_{2} : T_{2}
\overline{T-Pair}
Γ ⊢ (t_{1}, t_{2}) : T_{1} × T_{2}

Beseitigung.

Γ ⊢ t : T_{1} × T_{2} ; \overline{T-Proj_{1}} ; Γ ⊢ t.1 : T_{1} Γ ⊢ t : T_{1} × T_{2} ; \overline{T-Proj_{2}} ; Γ ⊢ t.2 : T_{2}

Datensätze Einführung.

Γ ⊢ t_{i} : T_{i} für i = 1 … n

\overline{T-Record}

Γ ⊢ \begin{cases}−⇀ \\ l =t \end{cases}\} : \begin{cases}−⇀ \\ l:T \end{cases}\}

Beseitigung.

Γ ⊢ t : \begin{cases}−⇀ \\ l:T \end{cases}\} ; \overline{T-Proj} ; Γ ⊢ t.l_{i} : T_{i}

Lokale Variablen

Γ ⊢ s : S Γ, x:S ⊢ t : T
\overline{T-Let}
Γ ⊢ let x=s in t : T

Rekursion

Γ, f:T ⊢ t : T
\overline{T-Fix}

Γ ⊢ fix f:T t : T

Referenzen

Bislang wurden nur rein funktionale Programmkonstrukte behandelt. Der Wert v eines Ausdrucks t war allein durch die Gestalt von t bestimmt, d.h. es gab immer höchstens ein v mit t ⟶^{∗} v. Dies ändert sich, wenn man Seiteneffekte zur Programmiersprache hinzunimmt. Der Wert eines Ausdrucks t is dann abhängig von einem Zustand μ der Maschine, der nicht durch t allein determiniert ist. Zudem kann die Auswertung eines Ausdrucks eine Änderung des Zustandes verursachen. Beispiele für Zustand in einem realen Rechnersystem sind Register- , Hauptspeicher- und Festplatteninhalt, der Zustand von Peripheriegeräten wie z.B. der Tastatur. Wir behandeln im folgenden nur den Hauptspeicher.

[ Hier wird der Stoff aus Pierce [Pie02], Kapitel 13, behandelt. Die folgende Mitschrift ist von Cyril Bitterich. ]

Operationen

• Allozierung + Initialisierung einer neuen Zelle ref v

• Auslesen einer Zelle !v

• Neubeschreiben einer Zelle v_{1} := v_{2}

Beispiel 7.1 C/JAVA

int bla() {
  int x = 5;
  x = x+1;
  return x;
}

In λ^{Ref}: bla = λu : Unit let x = ref 5

in (x := !x+1;

!x)

Auswertung bla() ref 5 ⟶ l (l ist neue Adresse “location”) !x ⟶ !l ⟶ 5 5 +1 ⟶ 6 x:=6 ⟶ () !x ⟶ 6

Beschreibung der Speicherbelegung

μ Zustand des Speichers, bildet Adressen auf Werte ab d.h. !l ⟶ μ(l)

Operationen auf den Speicher

• Allokieren: (μ, l ↦ v): neue Adresse l, Initialisierung mit v

• Schreiben: [l ↦ v]μ: v neuer Inhalt von l

• Lesen: μ(l) = v: v Inhalt von l

• Leerer Speicher: ∅

Neue Auswertungsrelation

t | μ ⟶ t′ | μ′

Übung 7.1 ref5 | μ_{0} ⟶ l | \underbrace{(μ_{0}, l ↦ 5)}_{μ_{1}} μ_{1} ≥ μ_{0}

!l | μ_{1} ⟶ \underbrace{μ_{1}(l)}_{5} | μ_{1}

l := 6 | μ_{1} ⟶ () | \underbrace{[l ↦ 6]μ_{1}}_{μ_{2}} μ_{2} ≱ μ_{1}

!l | μ_{2} ⟶ \underbrace{μ_{2}(l)}_{6} | μ_{2}

Terme

t:: = … | ref t | !t | t_{1} := t_{2} | l (nur intern)

Werte

v :: = … | l

\underline{45}

Auswertungsregeln

• Erweitere bisherige Regeln im Speicher μ

z.B.

\overline{(λx : T.t)v | μ ⟶ [v/x]t | μ}E − Beta

z.B.

\frac{t_{1} | μ ⟶ t′_{1} | μ′}{t_{1}t_{2} | μ ⟶ t′_{1}t_{2} | μ′}

• Neue Regeln:

– Allokation \overline{ref v | μ ⟶ l | (μ, m ↦ v)}E − RefV

\frac{t | μ ⟶ t′ | μ′}{ref t | μ ⟶ ref t′ | μ′} E − Ref

– Auslesen \overline{!l | μ ⟶ μ(l) | μ}E − DerefV

\frac{t | μ ⟶ t′ | μ′}{!t | μ ⟶ t′ | μ′} E − Deref

– Zuweisung \overline{l := v | μ ⟶ () | [l ↦]μ}E − AssignV V

\frac{t_{1} | μ ⟶ t′_{1} | μ′}{t_{1} := t_{2}μ ⟶ t′_{1} := t_{2} | μ}E − AssignT T

\frac{t | μ ⟶ t′ | μ′}{l := t | μ ⟶ l := t′ | μ′} E − AssignV T

Typisierung

T :: = … | Ref T

Regeln

\frac{Γ | Σ ⊢ t : T}{Γ | Σ ⊢ ref t : Ref T} T − Ref

\frac{Γ | Σ ⊢ t : Ref T}{Γ | Σ ⊢!t : T} T − Deref

\frac{Γ | Σ ⊢ t_{1} : Ref T Γ | Σ ⊢ t_{2} : T}{Γ | Σ ⊢ t_{1} := t_{2} : Unit} T − Assign

\frac{Σ(l) = T}{Γ | Σ ⊢ l :}T − Loc

Rohfassung vom 20. August 2002

Übung 7.2 let x = ref 5 in x:= !x+1

\frac{\frac{\overline{5:Int}}{ref 5:Ref Int} \frac{_{\overline{x...⊢x:Ref Int}} T −V ar ^{\frac{\frac{\overline{x:...⊢x:Ref Int} T −V ar}{x:...⊢!x:Int ...⊢1:Int} T −Deref}{x:...⊢!x+1:Int}} T −Assign}{X:Ref Int⊢x:=!x+1:Unit}}{⊢ let x = ref5 inx :=!x + 1 : Unit}

Durch Auswertung treten auch Terme l aud, Was ist ihr Typ? z.B.: ref5 ⟶ l

Lösung Typisiere den Speicher μ. Merke für jede Adresse l den Typ der zugehörigen Zelle.

Speichertyp

Σ :: = ∅ | Σ, l : T

Übung 7.3 \frac{5:Int}{·|∅⊢ref 5:Ref Int}T − Ref ref 5 | ∅ ⟶ l | (∅, l ↦ 5) \overline{·|l:Int ⊢l:Ref Int}T − Loc

Satz 7.1 Wenn

Γ | Σ ⊢ t : T
t | μ ⟶ t′ | μ′
Γ ⊢ μ : Σ

dann gibt es ein Σ′ mit Σ′ ∋ Σ und

Γ | Σ′ ⊢ t′ : T
Γ ⊢ μ′ : Σ′

Definition 7.1 Γ ⊢ μ : Σ

\overline{Γ ⊢ ∅ : ∅}T − Empty

\frac{Γ ⊢ μ : Σ Γ | Σ ⊢ v : T}{Γ ⊢ (μ, l ↦ v) : (Σ, l : T)} T − Alloc

\frac{Γ ⊢ μ : Σ Γ | Σ ⊢ v : Σ(l)}{Γ ⊢ [l ↦ v]μ : Σ}T − W rite

Rohfassung vom 20. August 2002

Untertypen

Der Begriff des Untertyps^{1} ist essentiell für objekt-orientierte Programmierung, findet sich aber schon in einfachen imperativen Programmiersprachen wie z.B. PASCAL. Dort gibt es zwei Divisionsoperatoren: div für Ganzzahlen und “/” für Fließkommazahlen. In unserer Schreibweise:

               i : Int  j : Int
                 i div j : Int

                                  a : Float  b : Int

                                     a/b : Float

PASCAL erlaubt die Anwendung von “/” auch auf Ganzzahlen; der Compiler führt intern eine Konvertierung nach Fließkomma durch. Eine Typherleitung für den Term i/j sieht dann so aus:

i : Int ; \overline{T-Sub} ; i : Float j : Int ; \overline{T-Sub} ; j : Float
\overline{T-DivFloat}

                      i/j : Float

An den Stellen T-Sub wird eine Typkonversion durchgeführt. Die Konversion ist zulässig, weil Int als ein Untertyp von Float angesehen werden kann, d.h. jede Ganzzahl kann als Fließkommazahl interpretiert werden. Die zentrale Frage im Zusammenhang mit Untertypen ist: Welche Konversionen sind zulässig und sollen vom Typ-Prüfer bzw. Übersetzer automatisch durchgeführt werden?

8.1 Subsumption

Aus der Mathematik ist bekannt, dass ℤ ⊆ ℝ. Diese semantische Relation können wir auf der Typebene reflektieren durch die Untertyp-Relation

                           Int <: Float

1auch Teiltyp.

Rohfassung vom 20. August 2002

Konversion ist möglich von einem Term eines Typs S in dessen Obertyp T, was wir durch die Subsumptions-Regel erfassen:

Γ ⊢ t : S S <: T
\overline{T-Sub}
Γ ⊢ t : T

Prinzip I (Teilmenge) Ein Typ S kann als Untertyp von T aufgefasst werden, wenn die Menge der Bewohner von S als eine Teilmenge der Bewohner von Typ T angesehen werden kann.

Prinzip II (Ersetzung) Ein Typ S kann als Untertyp von T aufgefasst werden, wenn an jeder Stelle, wo ein Term vom Typ T erwartet wird, ein Term vom Typ S eingesetzt werden kann ohne die Typsicherheit zu gefährden.

8.2 Regeln der Untertyp-Beziehung

[ Hier fehlt die Motivation der einzelnen Typregeln ]

Definition 8.1 (Deklarative Untertyp-Beziehung) Die Relation S <: T ist gegeben durch die folgenden Inferenzregeln:

\overline{S-Refl} ; T <: T  R <: S  S <: T ; \overline{S-Trans} ; R <: T

T_{1} <: S_{1}  S_{2} <: T_{2} ; \overline{S-Arrow} ; S_{1} → S_{2} <: T_{1} → T_{2}  S_{1} <: T_{1}  S_{2} <: T_{2} ; \overline{S-Prod} ; S_{1} × S_{2} <: T_{1} × T_{2}

\overline{S-RWidth} ; \begin{cases}−⇀ \\ l : T \end{cases}, \begin{matrix}−⇀ \\ k : R \end{matrix}\} <: \begin{cases}−⇀ \\ l : T \end{cases}\} S_{i} <: T_{i} für i=1..|\begin{matrix}− ⇀ \\ l \end{matrix}| \overline{S-RDepth}

\begin{cases}−⇀ \\ l : S \end{cases}\} <: \begin{cases}−⇀ \\ l : T \end{cases}\}

8.3 Entscheidung der Untertyp-Beziehung

Satz 8.1 Die Untertyp-Relation ist entscheidbar.

Zum Beweis dieses Satzes müssen wir einen Algorithmus angeben, der für beliebige Typen S und T entscheidet ob S <: T.

Aus den bisherigen Untertyp-Regeln lässt sich nicht direkt ein Algorithmus ableiten. Insbesondere die Transitivitäts-Regel bereitet Kopfzerbrechen, denn sie ist nicht Syntax-gerichtet. Um zu entscheiden ob R <: T, empfiehlt uns die Transitivitäts-Regel, einen Typ S zu finden und dann R <: S und S <: T zu testen. Da es unendlich viele Typen S gibt, kann unsere Suche endlos dauern.

Wir entwickeln im folgenden neue Regeln für Untertypen, die ohne eine Transitivitäts-Regel auskommen, deterministisch und Syntax-gerichtet sind.

Definition 8.2 (Algorithmische Untertyp-Beziehung) Die Relation S ◁: T ist gegeben durch die folgenden Inferenzregeln:

\overline{SA-Refl} ; A ◁: A für Grundtypen A

T_{1} ◁: S_{1}  S_{2} ◁: T_{2} ; \overline{SA-Arrow} ; S_{1} → S_{2} ◁: T_{1} → T_{2}  S_{1} ◁: T_{1}  S_{2} ◁: T_{2} ; \overline{SA-Prod} ; S_{1} × S_{2} ◁: T_{1} × T_{2}

S_{i} ◁: T_{i} für i=1..|\begin{matrix}− ⇀ \\ l \end{matrix}|

\overline{SA-Record}

\begin{cases}−⇀ \\ l : S \end{cases}, \begin{matrix}−⇀ \\ k : R \end{matrix}\} ◁: \begin{cases}−⇀ \\ l : T \end{cases}\}

Aus diesen Regeln lässt sich nun direkt ein Algorithmus ablesen. Bleibt zu zeigen, dass die beiden Untertyp-Beziehungen äquivalent sind. Die eine Richtung ist einfach: Jede Untertyp-Beziehung S ◁: T, die mit den algorithmischen Regeln hergeleitet wurde, kann auch mit den deklarativen gezeigt werden. Hierfür muss man nur einsehen, dass sich jede Anwendung der Regel SA-Record durch eine Kombination von S-RWidth, S-RDepth, S-Trans und S-Refl ausdrücken lässt.

Lemma 8.1 (Algorithmische Untertyp-Relation ist korrekt) Wenn S ◁: T, dann S <: T.

Beweis. Induktion nach S ◁: T. □

Die andere Richtung ist etwas schwieriger. Hier machen Anwendungen der Regeln S-Refl und S-Trans Umstände. Wir zeigen also zuerst, dass die algorithmische Relation reflexiv und transitiv ist. Die Beweise dieser Aussagen geben uns Algorithmen, wie wir Vorkommen von S-Refl und S-Trans eliminieren können.

Lemma 8.2 (Reflexivität) Für alle Typen T gilt T ◁: T.

Beweis. Durch Induktion nach T. Wir demonstrieren einen Fall:

Fall T = T_{1} → T_{2}. Nach Induktionsvoraussetzung gilt T_{1} ◁: T_{1} und T_{2} ◁: T_{2}. Mit Regel SA-Arrow folgt damit T_{1} → T_{2} ◁: T_{1} → T_{2}. □

Lemma 8.3 (Transitivität) Wenn R ◁: S und S ◁: T, dann R ◁: T.

Beweis. Durch Induktion nach R ◁: S mit Fallunterscheidung über S ◁: T. Zum Beispiel:

Fall R = R_{1} → R_{2}, S = S_{1} → S_{2} und

{S_{1} ◁: R_{1}  R_{2} ◁: S_{2} \atop R_{1} → R_{2} ◁: S_{1} → S_{2}}SA-Arrow  S_{1} → S_{2} ◁: T

Die einzige Möglichkeit ist T = T_{1} → T_{2} mit T_{1} ◁: S_{1} und S_{2} ◁: T_{2}. Induktionsvoraussetzung liefert T_{1} ◁: R_{1} und R_{2} ◁: T_{2}. Mit Regel SA-Arrow folgt also R_{1} → R_{2} ◁: T_{1} → T_{2}. □

Lemma 8.4 (Algorithmische Untertyp-Relation ist vollständig) Wenn S <: T, dann S <: T.

Beweis. Durch Induktion nach S <: T, unter Verwendung der Lemmata über Reflexivität und Transitivität. □

Satz 8.1 folgt nun leicht. Die algorithmische Untertyp-Relation lässt sich direkt in ein Programm umwandeln, dass für gegebene S, T entscheidet, ob S ◁: T. Nach Lemmata 8.1 und 8.4 ist dies äquivalent zu S <: T.

Objekt-orientierte Programmierung

Objekt-orientierung ist ein Paradigma bzw. ein Programmierstil. Manche Programmiersprachen stellen Sprachkonstrukte zur Verfügung, die objekt-orientiertes Programmieren begüngstigen; allerdings kann man auch in funktionalen Sprachen objekt-orientiert Programmieren (siehe Abelson und Sussman [ASS91]). In realen objekt-orientierten Sprachen vereinigt das Konzept der Klasse eine Vielzahl von Aspekten objekt-orientierter Programmierung auf sich. Wie Pierce [Pie02] beschränken wir uns auf fünf wesentliche Kennzeichen.

Polymorphie Ein Interface kann mehrere Implementationen besitzen. Dynamic dispatch: Objekt entscheidet, welcher Code ausgeführt wird.

Kapselung Nur Methoden des Objektes können auf Instanzenvariablen direkt zugreifen.

Subtyping Ein Objekt mit mehr Funktionalität (Methoden) kann an jeder Stelle verwendet werden, an der ein Objekt mit weniger Funktionalität erwartet wird.

Vererbung Verhalten und Implementation kann an \underline{Subklasse} weitergegeben werden.

Späte Bindung (self, this) Vituelle Methoden.

Im folgenden zeigen wir am Beispiel eines Zählers (counter), wie wir die obigen Konzepte in unserer funktionalen Sprache simulieren können. Der Programmcode ist direkt von Pierce [Pie02] übernommen.

9.1 Objekte, Methoden

Interface.

Counter = { get: Uni -> Int , inc: Unit -> Unit }

Objekt.

c = let x = ref 0 in
        { get = \lambda _:Unit. !x,
          inc = \lambda _:Unit. x := !x + 1 }
c : Counter

Methodenaufruf.

c.get(), c.inc()
inc3 = \lambda c: Counter. (c.inc(); c.inc(); c.inc())

9.2 Konstruktor

Objektkonstruktoren bezeichnen wir mit new...

newCounter : Unit -> Counter
newCounter = \lambda _:Unit. let x = ref 0 in
        { get = \lambda _:Unit. !x,
          inc = \lambda _:Unit. x := !x + 1 }

9.3 Subtyping

ResetCounter={get...; inc..., reset:Unit -> Unit}
newResetCounter = \lambda _:Unit. let x = ref 0 in
        { get   = \lambda _:Unit. !x,
          inc   = \lambda _:Unit. x := !x + 1,
          reset = \lambda _:Unit. x := 0 }

9.4 Bündelung der Instanzen-Variablen

CounterRep = { x: Ref Int }
newCounter = \lambda _:Unit.
    let r = {x=ref 0 } in
        { get = \lambda _:Unit. !(r.x),
          inc = \lambda _:Unit. r.x := !(r.x) + 1 }

9.5 Klassen

Definition 9.1 Interface Ein Datensatz-Typ, in dem jeder Eintrag ein Funktionstyp ist.

Definition 9.2 Objekt Ein Term vom Typ “Interface”.

Definition 9.3 Methode Ein Bestandteil eines Objektes.

Definition 9.4 Klasse Die Sammlung der Objekte mit identischer Implementation der Methoden.

CounterRep = { x: Ref Int}
counterClass: CounterRep -> Counter
counterClass
     = \lambda r: CounterRep.
        {get = \lambda _: Unit. !(r.x),
         inc = \lambda _: Unit. r.x := !(r.x) + 1 }

Vererbung

ResetCounter = { get..., inc..., reset: Unit ->Unit }
resetCounterClass : CounterRep -> ResetCounter
resetCounterClass = \lambda r: CounterRep.
     let super = counterClass r in
         { get = super.get,
           inc = super.inc,
           reset = \lambda _: Unit. r.x := 0 }
newResetCounter = \lambda _: Unit. let r = {x = ref 0} in resetCounterClass r

9.6 Zusätzliche Instanzenvariablen

BackupCounterRep = { x: Ref Int, b: Ref Int}
BackupCounter = { get..., inc..., reset..., backup: Unit -> Unit }
backupCounterClass : BackupCounterRep -> BackupCounter
backupCounterClass = \lambda r : BackupCounterRep.
     let super = counterClass r in
         { get = super.get,
           inc = super.inc,
           reset = \lambda _: Unit. r.x := !(r,b),
           backup = \lambda _: Unit. r.b := !(r.x) }

9.7 self (ohne dynamische Bindung)

Ziel: Eine Methode kann andere Methoden des gleichen Objektes aufrufen. (Rekursion)

SetCounter = { get : Unit -> Unit,
               set : Int -> Unit,

               inc : Unit -> Unit }
setCounterClass : CounterRep -> SetCounter
setCounterClass = \lambda r : CounterRep.
      fix self : SetCounter.
      { get = \lambda _: Unit. !(r.x),
        set = \lambda i : Int. r.x := i,
        inc = \lambda _: Unit.
              self.set (self.get()+1) }
newSetCounter : Unit -> SetCounter
newSetCounter = \lambda _:Unit
      let r = {x = ref 0 } in setCounterClass r

9.8 self (mit dynamischer Bindung)

SetCounter = { get : Unit -> Unit,
               set : Int -> Unit,
               inc : Unit -> Unit }
setCounterClass : CounterRep -> SetCounter -> SetCounter
setCounterClass = \lambda r : CounterRep.
      \lambda self : SetCounter.
      { get = \lambda _: Unit. !(r.x),
        set = \lambda i : Int. r.x := i,
        inc = \lambda _: Unit.
              self.set (self.get()+1) }
newSetCounter : Unit -> SetCounter
newSetCounter = \lambda _:Unit
      let r = {x = ref 0 } in
        fix self : SetCounter. setCounterClass r self

Problem: Mit cbv-Auswertung hängt sich der Rechner beim Instantiieren der

Klasse mit newSetCounter auf:
fix self : SetCounter. setCounterClass r self
--> setCounterClass r (fix self... setCounterClass r self)
--> setCounterClass r (setCounterClass r (fix self... setCounterClass r self ))
--> ...

Abhilfe:

1. Man verwendet eine “lazy” Sprache, die Funktionsargumente nur bei Bedarf auswertet.

2. Man kodiert verzögerte Auswertung per Hand durch “dummy”-Abstraktionen \lambda _:Unit und -Applikationen ().

     self : Unit -> SetCounter
     self () : SetCounter
     setCounterClass : CounterRep -> (Unit -> SetCounter) -> SetCounter
     setCounterClass = \lambda r : CounterRep.
           \lambda self : Unit -> SetCounter.
           { get = \lambda _: Unit. !(r.x),
             set = \lambda i : Int. r.x := i,
             inc = \lambda _: Unit. self().set (self().get() + 1) }
     newSetCounter = \lambda _:Unit
           let r = {x = ref 0 } in
             fix self : Unit -> SetCounter.
               \lambda _: Unit. setCounterClass r self

Beispiel: “instrumented Counter”; zählt die Anzahl der Schreibzugriffe mit set. Das in der Oberklasse setCounterClass mit später Bindung implementierte inc kann unverändert übernommen werden, obwohl set überschrieben wird.

Achtung! Diese Implementation ist in einer strikten cbv-Sprache inkorrekt und muss nach dem Vorbild von setCounterClass umgearbeitet werden.

InstrCounterRep = { x : RefInt, a: RefInt }
InstrCounter = { get..., set..., inc..., accesses: Unit -> Int }
instrCounterClass = InstrCounterRep -> InstrCounter -> InstrCounter
instrCounterClass =
    \lambda r : InstrCounterRep \lambda self : InstrCounter.
      let super = setCounterClass r self
      in { get = super.get ,
           set = \lambda i : Int. ( super.set(i) ; r.a := !(r.a)+1),
           inc = super.inc ,
           accesses = \lambda _: Unit. !(r.a) }

Kapitel 10

Featherweight Java

[ Hier wird der Stoff aus Pierce [Pie02], Kapitel 19, behandelt. ]

58  Featherweight Java

Literaturverzeichnis

[ASS91] Harold Abelson, Gerald Jay Sussman, and Julie Sussman. Struktur und Interpretation von Computerprogrammen. Springer-Verlag, 1991.

[DLNS98] David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq SRC, 1998.

[Pie02] Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002.

[Zus99] Horst Zuse. Geschichte der Programmiersprachen. Technical Report 1999-1, Technische Universität Berlin, 1999.