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

Übungsblatt 5

zur Vorlesung Termersetzungssysteme im Sommersemester 2001 7. Juni 2001

1. [2, Exercise 4.18] Schreibe s ≲^{?} t für das Problem, eine Substitution σ zu finden mit σ̂(s) = t, in ”Deutsch“: Matcht s auf t? So ein σ heißt dann Match. (s ist das Muster und t eine Instanz des Musters.)

Entscheide die Lösbarkeit der folgenden Unifikations- und Matchingprobleme und gib nach Möglichkeit allgemeinste Lösungen an.

(a) f(x, y) =^{?} f(h(a), x) und f(x, y) ≲^{?} f(h(a), x)

(b) f(x, y) =^{?} f(h(x), x) und f(x, y) ≲^{?} f(h(x), x)

(c) f(x, b) =^{?} f(h(y), z) und f(x, b) ≲^{?} f(h(y), z)

(d) f(x, x) =^{?} f(h(y), y) und f(x, x) ≲^{?} f(h(y), y)

(Es ist immer dieselbe Gleichung einerseits als Unifikations- und andererseits als Matchingproblem.)

2. [1, Aufgabe 3.4.4] Entscheide die Lösbarkeit der folgenden Unifikationsprobleme und gib gegebenenfalls idempotente allgemeinste Unifikatoren an.

(a) f(f(x, b), y) =^{?} f(f(a, y), x)

(b) f(x, y) =^{?} f(f(x, b), y)

(c) g(x, f(x, y), f(y, f(x, y))) =^{?} g(x, y′, f(z, y′))

(d) g(x, f(x, y), f(y, f(x, y))) =^{?} g(x, y′, f(y′, z))

3. [3, Aufgabe 8.1] Gib, wenn möglich, allgemeinste Unifikatoren zu folgenden Problemen an:

(a) h(x_{2}, x_{3}, x_{4}, x_{5}) =^{?} h(f(x_{1}, x_{1}), f(x_{2}, x_{2}), f(x_{3}, x_{3}), f(x_{4}, x_{4}))

(b) h(x_{1}, g(x_{2}), x_{1}, x_{1}) =^{?} h(x_{2}, x_{1}, g(x_{2}), g(x_{3}))

(c) f(x_{1}, g(x_{2})) =^{?} f(f(x_{3}, x_{4}), g(x_{3}))

4. [2, Exercise 4.16] Seien S und T Unifikationsprobleme, seien σ ein mgu von S und θ ein mgu von σ̂(T) (d. h., des Problems, das aus T entsteht, indem man auf alle linken und rechten Seiten der Gleichungen σ̂ anwendet). Zeige, daß dann θσ ein mgu von S ∪ T ist.

Literatur

[1] Jürgen Avenhaus. Reduktionssysteme—Rechnen und Schließen in gleichungsdefinierten Strukturen. Springer Verlag, 1995.

[2] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

[3] Reinhard Bündgen. Termersetzungssysteme—Theorie, Implementierung, Anwendung. Vieweg, 1998.

Besprechung in der Übung am 13. Juni 2001.