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

Übungsblatt 3

zur Vorlesung Termersetzungssysteme im Sommersemester 2001 17. Mai 2001

1. [2, Exercise 2.6] Eine Relation → heißt beschränkt, wenn es zu jedem x aus der Trägermenge ein n ∈ ℕ gibt so, daß keine Reduktionsfolge der Länge n von x aus geht, d. h. für alle y gilt: x ↛^{n} y.

• Zeige, daß nicht jede terminierende Relation beschränkt ist.

• Zeige, daß eine endlich verzweigende Relation genau dann beschränkt ist, wenn sie terminiert.

2. [1, Aufgabe 1.2.7] Sei → eine beschränkte Relation. Dann folgt aus der lokalen Konfluenz von → die Konfluenz von →.

3. [2, Exercise 2.25] Sei > strikte Ordnung auf M und m, n ∈ M(M). Dann gilt:

m >_{mul} n ⇔ m ≠ n ∧ ∀x ∈ n \ m ∃y ∈ m \ n.y > x.

Bemerkung: Damit läßt sich in konkreten Fällen leichter prüfen, ob m >_{mul} n gilt.

4. [3, Aufgabe 2.2] Finde eine Signatur, bzgl. der die folgenden Ausdrücke Terme über der Variablenmenge {x, y} sind: f(g(a, x), g(x, a)), h(b, y, f(b, x)), g(g(g(x, x), g(x, x)), x). Stelle sie als Bäume dar. Sei σ := {x ↦ a, y ↦ b} eine Substitution. Wende σ̂ (d. h. die auf Terme erweiterte Substitution σ) auf die obigen Terme an.

5. [2, Exercise 3.3] Definiere für Substitutionen σ, τ : X → T (Σ, X) die Substitution στ durch (στ)(x) := σ̂(τ(x)). Zeige, daß dies in der Tat eine Substitution ergibt und daß die so definierte Komposition von Substitutionen assoziativ ist, d.h. (σ_{1}σ_{2})σ_{3} = σ_{1}(σ_{2}σ_{3}).

6. [2, Exercise 2.37] sowie [1, Aufgabe 1.3.3] Seien →_{1} und →_{2} Reduktionsrelationen über derselben Trägermenge und sei →:=→_{1} ∪ →_{2} transitiv. Zeige, daß → genau dann terminiert, wenn →_{1} und →_{2} terminieren.

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 23. Mai 2001.