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

Übungsblatt 8

zur Vorlesung Termersetzungssysteme im Sommersemester 2001 6. Juli 2001

1. Zeige, daß das Termersetzungssystem von Aufgabe 1 auf Blatt 7 konfluent ist. Zur Erinnerung

dessen Ersetzungsregeln:

\begin{matrix}a(0, y) → & s(y) \\ a(s(x), 0) → & a(x, s(0)) \\ a(s(x), s(y)) → & a(x, a(s(x), y)) \end{matrix}

2. [1, Exercise 7.1, E_{1}] Sei Σ := {f, g} mit nur zwei einstelligen Funktionssymbolen. Sei V eine abzählbar unendliche Variablenmenge. Zeige die Konfluenz des folgenden Termersetzungssystems über T (Σ, V):

\begin{matrix}f(g(f(x))) → & x \\ f(g(x)) → & g(f(x)) \\ g(f(f(x))) → & x \end{matrix}

Zeige weiter, daß für die von der ersten Regel erzeugte Gleichheitsrelation ≈ auf T (Σ, V) [i. a. W.: ≈:=↔_{0}^{∗} für →_{0} nur mit Regel f(g(f(x))) →_{0} x gebildet] gilt:

f(g(x)) ≈ g(f(x)) und g(f(f(x))) ≈ x

Hinweise: Die Klammern tragen hier keine Information und sollten grundsätzlich weggelassen werden. Die Regelmenge ist damit {fgfx → x, fgx → gfx, gffx → x}. Die starke Normalisierung sieht man am leichtesten mit einer lexikografischen Pfadeordnung.

3. [1, Exercise 7.2] (langwierig) Sei Σ := {∗} mit nur einer zweistelligen binären Verknüpfung, für die wir Infix-Notation verwenden. Sei V eine abzählbar unendliche Variablenmenge. Gegeben sei das folgende Termersetzungssystem über T (Σ, V):

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

Benutze das Lemma über kritische Paare, um das Termersetzungssystem als konfluent nachzuweisen. (Wie erkennt man dessen starke Normalisierung?)

Hilfestellung: Es handelt sich hier um 3^{3} Kombinationsmöglichkeiten von Regeln zur Berechnung der kritischen Paare. Davon gelten bestimmte Kombinationen nicht als kritische Paare, andere würden schlicht Doubletten liefern. Manchmal schlägt die Unifikation fehl. Weitere Arbeitsersparnis ergibt sich aus einer offensichtlichen Symmetrie zwischen der zweiten und dritten Regel. Gehe systematisch vor, zähle mit und vergleiche mit den ”Kostenvoranschlägen“, um kein kritisches Paar zu übersehen. Es genügt, nur einmal das genaue Vorgehen bei der Unifikation zu beschreiben. In den anderen Fällen ist eine intuitive Herangehensweise vorzuziehen.

Literatur

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

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