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

Übungsblatt 9

zur Vorlesung Termersetzungssysteme im Sommersemester 2001 13. Juli 2001

1. [2, Exercise 7.1, E_{2}] Sei Σ := {f, g} mit zwei einstelligen Funktionssymbolen. Beschreibe das Ergebnis der Anwendung des grundlegenden Vervollständigungsalgorithmus auf das Gleichungssystem

{f(g(f(x))) ≈ f(g(x))}

nach Zugrundelegung einer passenden Reduktionsordnung. Beweise die Richtigkeit dieser Beschreibung. Was genau sagt uns der Satz über die Korrektheit (7.1.4) des grundlegenden Vervollständigungsalgorithmus in diesem Beispiel? Hinweis: Die Klammern sollten hier wie in Aufgabe 2 von Blatt 8 grundsätzlich weggelassen werden.

2. [3, Variante von Aufgaben 7.7 und 10.3] Seien

R_{0} := {x + (y + z) → (x + y) + z, f(x) + f(y) → f(x + y)}

und

R := R_{0} ∪ {x + f(y + z) → (x + f(y)) + f(z)}

Zeige die Terminierung von R mittels einer Polynomordnung. (Tip: P_{f} := X + 1, P_{+} := XY^{2}). Zeige, daß x + f(y + z) ↔_{R_{0}}^{∗} (x + f(y)) + f(z) gilt. Ist R konfluent?

3. [1, Aufgabe 3.7.6 a)] (Die Notation folgt [2, Exercise 7.12].) Zeige, daß das folgende Termersetzungssystem für die Gruppentheorie terminiert. (Tip: Es geht mit >_{lpo}.) Σ := {1, i, ∗} mit 1 Konstante, i einstellig (Inverse), ∗ binär.

\begin{matrix}(x ∗ y) ∗ z → & x ∗ (y ∗ z) \\ 1 ∗ x → & x \\ i(x) ∗ x → & 1 \\ x ∗ 1 → & 1 \\ x ∗ i(x) → & 1 \\ i(1) → & 1 \\ i(i(x)) → & x \\ i(x ∗ y) → & i(y) ∗ i(x) \\ x ∗ (i(x) ∗ y) → & y \\ i(x) ∗ (x ∗ y) → & y \end{matrix}

Bemerkung: Die ersten 3 Regeln entsprechen den minimalen Axiomen der Gruppentheorie, die anderen lassen sich durch Vervollständigung daraus gewinnen (in der Algebra zieht man diese Regeln ”aus dem Hut“). Den Nachweis der Konfluenz des Systems überläßt man einer Implementierung des Vervollständigungsalgorithmus.

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.

Abgabe vor und Besprechung in der Übung am 18. Juli 2001.