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

Als Graham Hendrick seiner Frau das erste Mal beim Ehebruch zusah, da machte es ihm überhaupt nichts aus. Er mußte sogar kichern.

aus Julian Barnes: Als sie mich noch nicht kannte

Aufgabe 1

Einen Listenausdruck zu einer Liste beliebiger Tiefe ausgewertet werden kann, und der kein undefiniertes Listenelement enthält, nennen wir lazy-terminierend.

Hat die Funktion concat angewendet auf einen lazy-terminierenden Listenausdruck eine Kopfnormalform?

Aufgabe 2

Zeigen Sie mit abstrakter Reduktion:

a) Die rekursive Funktion length wertet ihr Listeargument vollständig in der Länge aus.

b) Die Funktion sum wertet ihr Listenargument vollständig aus.

c) Wenn die Länge des Ergebnis einer Anwendung von append ausgewertet werden soll, dann müssen beide Argumente von append endliche Listen darstellen.

d) Ein rekursiv absteigender Parser einer linksrekursiven Grammatik terminiert nicht.