Andreas Podelski Fachbereich 14 – Informatik Universität des Saarlandes, Max-Planck-Institut für Informatik

[figure: I N F O R M A T I K]

Programmiersprachen (WS 1996/97)

5. Dezember 1996  Übungsblatt 7  Abdelwaheb Ayari Hubert Baumeister

Aufgabe 1: (4 Punkte) Um den Typ von rekursiven Funktionen zu bestimmen verwendet man den Fixpunktoperator Y, der zu einer Funktion f deren Fixpunkt a berechnet, d.h. für a gilt: f(a) = a.

1. Bestimme den allgemeinsten Typ von Y mit Hilfe des Typinferenzalgorithmus und der Eigenschaft von Y den Fixpunkt zu berechnen, d.h. f(Y f) = Y f.

2. Reduziere den Term (Y (λf.λx. if x = 0 then 1 else x ∗ (f (x − 1)))) 2, wobei für Y die Reduktionsregel Y (λf.e) → e[(Y (λf.e))/f] verwendet wird.

3. Leite den Typ von Y (λf.λx. if x = 0 then 1 else x ∗ (f (x − 1))) mit Hilfe des Typinferenzalgorithmus ab.

Aufgabe 2: (6 Punkte) Gegeben ist eine Liste von Termgleichungen E = [s_{1} = t_{1}, …, s_{n} = t_{n}]. Gesucht ist eine Substitution σ, so daß s_{i}σ = t_{i}σ ist für alle i von 1 bis n.

1. Implementiere eine Datenstruktur, die Terme repräsentiert. Die Signatur ist:

     signature TERM =
     sig
         type T;
         exception TermFunctionError of string;
         val cTerm : string * T list -> T;   val cVar : string -> T;
         val funct : T -> string;            val args : T -> T list;
         val arity : T -> int;               val isVar : T -> bool;
         val equals : T * T -> bool;         val occurs : T*T -> bool;
         val replace : T*T -> T -> T;        val show : T -> unit;
     end

Ein Term wird mit Hilfe der Funktionen cVar und cTerm erzeugt. Zum Beispiel der Term

     f(g(x, a)) wird durch den Ausdruck cTerm("f",[cTerm("g",[cVar("x"),cTerm("a",[])])])

erzeugt. Für funct und args gelten die Gleichungen funct(cTerm("f",args)) = "f" und args(cTerm("f",args)) = args. Die Funktion arity liefert die Anzahl der Argumente eines Terms und isVar liefert true, falls das Argument eine Variable ist, ansonsten false.

Die Funktion occurs(x,t) liefert true, falls die Variable x in t als Subterm vorkommt. Die Funktion replace(x,s) t ersetzt jedes Vorkommen der Variablen x in dem Term t durch den Term s. Die Funktion show gibt einen Term auf dem Bildschirm aus. Die Ausnahme TermFunctionError hat als Argument den Namen der Funktionen, bei der der Fehler aufgetreten ist.

2. Schreibe eine Struktur, die die Signatur SUBSTITUTION mit den folgenden Komponenten implementiert.

    structure Term:TERM;
    type T;
    exception SubFunctionError of string;
    val empty : T;                val cSub : Term.T * Term.T -> T;
    val show : T -> unit;         val apply : T * Term.T -> Term.T;
    val compose : T * T -> T

empty liefert die “leere” Substitution, d.h. apply(empty,t) = t und cSub(x,t) die Substitution [t/x], die x durch t ersetzt. Die Funktion compose(s1,s2) stellt die Komposition von zwei Substitutionen dar, wobei darauf geachtet werden muß, daß s1 auf die Terme von s2 angewandt werden muß, d.h. compose([f(a, b)/x], [g(a, x)/y, c/x]) = [f(a, b)/x, g(a, f(a, b))/y]. Beachte, daß [c/x] von [f(a, b)/x] überdeckt wird. Die Funktion apply wendet eine Substitution auf einen Term an und show gibt eine Darstellung der Substitution auf dem Bildschirm aus.

3. Gegeben sei die Signatur UNIFY mit den Komponenten:

    exception NotSolvable;
    structure T:TERM;                      structure S:SUBSTITUTION;
    val solve : (T.T * T.T) list -> S.T;   val unify : T.T * T.T -> S.T

Die Funktion unify(s,t) ist hierbei nur eine Abkürzung für solve([s,t]). Schreibe eine Struktur, die ein Lösungsverfahren für Termgleichungssysteme nach dem folgenden Inferenzsystem implementiert. Split: Wähle eine Gleichung f(s_{1}, …, s_{n}) = g(t_{1}, …, t_{m}) aus E, wobei n, m ≥ 0. Ist f ≠ g oder n ≠ m, dann ist das Gleichungssystem nicht lösbar. Ansonsten ersetzte die obige Gleichung in E durch die Gleichungen s_{1} = t_{1}, …, s_{n} = t_{n}. Merge: Wähle ein x = t aus E, wobei t ≠ x ist. Kommt x als Subterm in t vor, dann ist das Gleichungssystem nicht lösbar. Ansonsten entferne x = t aus E, ersetze jedes Vorkommen von x in E durch t und füge die Substitution [t/x] zur Lösungssubstitution σ hinzu. Delete: Lösche ein Vorkommen s = s aus E. Die Regeln erzeugen eine Folge (E_{0}, σ_{0}) … (E_{n}, σ_{n}) von Gleichungssystemen und Substitutionen, wobei E_{0} das zu lösende Gleichungssystem und σ_{0} die leere Substitution ist. Gelangt man zu E_{n} = ∅, dann ist das Gleichungssystem lösbar und die Substitution σ_{n} ist die Lösungssubstitution, ansonsten ist das Gleichungssystem nicht lösbar. Teste das Lösungsverfahren an folgenden Gleichungssystemen (x, y, z sind dabei Variablen und a und b nullstellige Funktionen (= Konstanten)):

[(f(x, a), f(a, x))] [(f(x, a), f(b, y))] [(f(x, a), f(b, x))] [(x, y)] [(x, x)]
[(f(a, b), h(a, b))] [(g(x), x)] [(f(g(y), y), f(x, g(z)))] [(f(x, y), f(z, g(g(y))))]