Prof. Dr. Reinhold Letz Institut für Informatik Dr. Ralph Matthes der Universität München

Übungsblatt 1

zur Vorlesung Lambda-Kalkül und Typen im Sommer 2000 9. Mai 2000

1. Definiere K := λxλyx und S := λxλyλz.xz(yz) (x, y, z verschieden). Beachte: Anwendungen sind immer implizit von links her geklammert, und der Punkt steht für ein Klammerpaar, das am Punkt öffnet und soweit rechts schließt, wie irgend (syntaktisch korrekt) möglich ist.

Berechne eine β-Normalform von SKK, d.h. einen Term r, den man durch endlich viele Umformungen mittels (λxt)s → t[x := s] (das sind β-Reduktionen) aus SKK erhält und der keine (weiteren) β-Reduktionen erlaubt.

2. Zeige

(a) \underline{m} ∘ \underline{n} =_{β} \underline{m · n} und

(b) \underline{m} \underline{n} =_{β} \underline{n^{m}} für m ≠ 0.

Dabei seien \underline{n} := λfλx. \underbrace{f(… (f}_{n-mal} x) …) die n-te Church-Ziffer, die Kompo-

sition wie erwartet r ∘ s := λx.r(sx) (für ein ”neues“ x) und m · n und n^{m} die üblichen Operationen auf natürlichen Zahlen. Wir erkennen, daß auf diese Weise einfache Arithmetik im ungetypten Lambda-Kalkül modelliert werden kann (tatsächlich lassen sich alle partiell rekursiven Funktionen modellieren).

3. (schwere Aufgabe) Definiere einen Lambda-Term P, der den Vorgänger modelliert: Für jede natürliche Zahl n ist P \underline{n} =_{β} \underline{n − 1}, und P \underline{0} =_{β} \underline{0}. Verifiziere, daß P diese Spezifikation erfüllt.

Ein Weg: Die Ziffer \underline{n} wendet ihr erstes Argument n-mal auf ihr zweites an. Also ist Iteration schon von selbst im System. Volle primitive Rekursion läßt sich mittels einer Paarbildung auf Iteration zurückführen. Paare selbst kann man ganz leicht definieren (also zu Termen r und s einen Term ⟨r, s⟩ und zu r Terme π_{1}r und π_{2}r mit π_{1}⟨r, s⟩ =_{β} r und π_{2}⟨r, s⟩ =_{β} s).

Besprechung in der Übung am 15. Mai 2000.