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. 6

Heute ist nicht Donnerstag Gestern war nicht Donnerstag und über morgen bin ich mir nicht sicher.

aus Lars Sundström: Kassenzettel

Aufgabe 1

a) Übersetzen Sie die folgende Haskellfunktion in PCF:

rotate :: Bool -> Bool -> Bool -> Bool
rotate x y z |x = x |otherwise = rotate y z x

b) Berechnen Sie die denotationale Semantik der in a) erstellten Funktion.

c) Geben Sie einen PCF-Ausdruck an, der in der denotationalen Semantik äquivalent zur in a) definierten Funktion ist, aber μ nur in der Form μx.x enthält. Zeigen Sie, daß diese Funktion tatsächlich äquvalent interpretiert wird.