Inhaltsverzeichnis

1  Einleitung  3

1.1  Motivation  3

1.2  Formen der Typisierung  3

1.2.1  Explizite Typisierung  4

1.2.2  Implizite Typisierung  4

2  Explizit getypter Lambda-Kalk ul  5

2.1  Formale Definition des Kalk uls  5

2.1.1  Terme  5

2.1.2  Typen  5

2.2  Herleitung der Typrelation  5

2.2.1  Wohlgetyptheit  6

2.3  Typpr ufung  7

2.3.1  Kontext  8

2.3.2  Alogrithmus  8

2.4  Formale Definition der Typrelation  9

2.5  Eigenschaften der Typpr ufung  9

2.6  Eigenschaften des explizit getypten Lambda-Kalk uls  9

3  Implizit getypter Lambda-Kalk ul  11

3.1  Idee der Typrekonstruktion  11

3.1.1  Herleitung des Algorithmus  12

3.2  Constraint Typing Relation  13

3.3  Unifikation  14

3.4  Selbstanwendung und Rekursion  14

3.5  Eigenschaften der Typrekonnstruktion  14

Quellenverzeichnis   15

2

1 Einleitung

1.1 Motivation

Der einfach getypte Lambda-Kalk¨ ul (simply typed lambda-calculus) wurde von Alonso Church (1940) und Haskell Curry (1958) entwickelt. Er erweitert den ungetypten Lambda Kalk¨ ul um Typen, die ¨ uber die Typrelation mit den Termen in Beziehung stehen. Da

bereits der ungetypte Lambda-Kalk¨ ul turing-m¨ achtig ist, ist nicht zu erwarten, dass die Einf¨ uhrung von Typen die Berechnung zus¨ atzlicher Funktionen erm¨ oglicht. Stattdessen ist die Einf¨ uhrung von Typen haupts¨ achlich durch folgende Aspekte motiviert: F¨ ur die Praxis am bedeutsamsten ist die automatisierte, statische Fehlererkennung, die durch Typisierung erm¨ oglicht wird. So k¨ onnen Laufzeitfehler auf ein Minimum reduziert werden und bedeutungslose Terme, wie etwa die Summe aus einer Zahl und einem booleschen Wert, fr¨ uhzeitig abgefangen werden. Deswegen kommen heutzutage bei gr¨ oßeren Softwareprojekten fast ausschließlich Programmiersprachen mit einer entsprechenden Typisierung zum Einsatz. Zwar ist der Lambda-Kalk¨ ul keine in der Praxis eingesetzte Programmiersprache, jedoch basieren praxisrelevante funktionale Programmiersprachen wie ML oder Haskell und deren Typsysteme auf dem getypten Lambda-Kalk¨ ul. Historisch gesehen war die Einf¨ uhrung von Typen dem Anliegen Churchs geschuldet, den Lambda-Kalk¨ ul zur Kodierung und Berechnung logischer Aussagen zu verwenden. Dazu werden Lambda-Terme als logische Aussagen interpretiert und Beta- ¨

als logische ¨ Aquivalenz aufgefasst. Nimmt man den Negationsoperator not als gegeben an, so l¨ asst sich im ungetypten Lambda-Kalk¨ ul nach dieser Interpretation folgender Widerspruch konstruieren: R := λx. not(x x) ⇒ R R ≡ β not(R R)

Derartige Inkonsistenzen lassen sich durch die Einf¨ uhrung von Typen eliminieren. Tats¨ achlich ist der getypte Lambda-Kalk¨ ul Basis moderner automatischer und interaktiver Beweissysteme.

Außerdem erm¨ oglichen Typen eine pr¨ agnante Spezifikation von Prozeduren, wobei angegeben wird, was f¨ ur Argumente eine Prozedur erwartet und von welcher Art das gelieferte Ergebnis ist. Dabei wird von der Funktionsweise der Prozedur abstrahiert. Als Beispiel betrachten wir die Typen einer Prozedur prim, die entscheidet, ob eine nat¨ urliche Zahl prim ist, und einer Prozedur +, die die Addition auf den nat¨ urlichen Zahlen realisiert:

1.2 Formen der Typisierung

Im Folgenden werden wir zwischen zwei Formen der Typisierung unterscheiden.

3

1.2.1 Explizite Typisierung

Hierbei erfolgt die Typisierung durch Typanotationen innerhalb des Terms. W¨ ahrend der Typpr¨ ufung (type checking) pr¨ uft der Interpreter/Compiler die Typangaben auf Konsistenz und liefert gegebenenfalls den Typ des Terms.

1.2.2 Implizite Typisierung

Hierbei erfolgen keinerlei Typangaben innerhalb des Terms. Der Interpreter/Compiler rekonstruiert aus der Struktur des Terms den passenden Typ. Diesen Vorgang bezeichnet man als Typinferenz (type inference).

4

2 Explizit getypter Lambda-Kalk¨ ul

2.1 Formale Definition des Kalk¨ uls

2.1.1 Terme

Genau wie im ungetypten Lambda-Kalk¨ ul k¨ onnen im einfach getypten Lambda-Kalk¨ ul Terme entweder Variablen, Abstraktionen oder Applikationen sein. Dabei werden Abstraktionen bei expliziter Typisierung um eine Typangabe f¨ ur die eingef¨ uhrte Variable erweitert. So werden wir im folgenden anstatt λx. x zum Beispiel λx : nat. x oder λx : bool. x schreiben.

Zus¨ atzlich erweitern wir den Kalk¨ ul um Primitive f¨ ur die nat¨ urlichen Zahlen und die booleschen Werte true und f alse, so dass diese k¨ unftig nicht mehr als Abstraktionen codiert werden m¨ ussen.

2.1.2 Typen

Die Typen von Konstanten bezeichnen wir als Basistypen. Wir f¨ uhren die zwei Basistypen nat und bool f¨ ur die nat¨ urlichen Zahlen beziehungsweise die booleschen Werte true und f alse ein. Prinzipiell l¨ asst sich der Kalk¨ ul auch noch um weitere Basistypen f¨ ur weitere Konstanten erweitern.

Außerdem brauchen wir einen Typ f¨ ur Abstraktionen. Hierf¨ ur f¨ uhren wir den Funktionstyp T 1 → T 2 ein, der als ” T 1 nach T 2 “ gelesen wird. Dabei bezeichnet T 1 den Argumenttyp der Abstraktion und T 2 den Ergebnistyp.

2.2 Herleitung der Typrelation

Nun k¨ onnen wir Aussagen der Form t : T formulieren, die wir als ” t hat den Typ

T“ lesen. Diese Relation zwischen Termen und Typen wird als Typrelation bezeichnet. Sofort einsichtig sind folgende Aussagen: