Prof. Dr. Manfred Schmidt-Schauß Fachbereich Informatik (20) Künstliche Intelligenz/Softwaretechnologie Johann Wolfgang Goethe-Universität Frankfurt am Main

Funktionales Programmieren II:

Semantik, statische Analyse, Verifikation und abstrakte Interpretation

Wintersemester 1996/97

Übungsblatt Nr. 7

Die photographische Telegraphie, die im vergangenen Jahrhundert von Professor Giovanni Caselli aus Florenz erfunden worden war, erlaubte es überdies, das Faksimile jedes beliebigen Schriftstücks, Handschrift oder Zeichnung in weiteste Fernen zu schicken und Wechsel oder Verträge über fünftausend Meilen hinweg zu unterzeichnen.

aus Jules Verne: Paris im 20. Jahrhundert

Aufgabe 1

Übersetzen Sie folgenden PCF-Ausdruck in ein ETK-Programm.

a) f = λx.λy.((λx.x)y)

b) f = λx.λy.λz.

((μg.λa.λb.

plus ((λd.λe.if (zero? d) then plus 10 (plus a x) else g (plus b e)(plus y 1)) a a)

((λq.plus q z) (plus a x)))

(plus (plus y z)((λq.(plus z q))(plus y z))) (plus (plus y z)((λq.(plus z q))(plus y z))))

Aufgabe 2

Übersetzen Sie folgende ETK-Programme in PCF-Ausdrücke:

a) fib x = if (zero? x) then 1
    else (if (zero? (pred x)) then 1
          else plus (fib (pred x)) (fib pred (pred x)))
b) f1 x = if (zero? x) then 1 else (succ (f2 (pred x)))
f2 x = if (zero? x) then 1 else (succ (f1 (pred x)))
main = f1 5