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

Übungsblatt 7

zur Vorlesung Termersetzungssysteme im Sommersemester 2001 29. Juni 2001

1. [1, Exercise 5.26] Gegeben sei die Signatur Σ := {a, s, 0} und das Termer-

setzungssystem

\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}

Zeige dessen Terminierung mittels einer lexikografischen Pfadeordnung. (Damit ist dann insbesondere die Ackermannfunktion als total nachgewiesen, vgl. Übungsblatt 2, Aufgabe 3.) Zeige weiter, daß keine Knuth-Bendix-Ordnung zum Beweis der Terminierung benutzt werden kann.

2. [2, Aufgabe 7.2] Zeige, daß das folgende Lemma (Dicksons Lemma, 1913) als Anwendung des Satzes von Kruskal zu erhalten ist: Sei A_{1}, A_{2}, … eine unendliche Folge von n-Tupeln natürlicher Zahlen. Dann gibt es Indizes i < j mit A_{i} komponentenweise kleiner als A_{j}.

3. [2, Aufgabe 7.6] Zeige die Terminierung von

\begin{matrix}¬¬x → & x \\ ¬(x ∧ y) → & ¬¬¬x ∨ ¬¬¬y \\ ¬(x ∨ y) → & ¬¬¬x ∧ ¬¬¬y \end{matrix}

mittels einer Knuth-Bendix-Ordnung. Geht das auch mit einer lexikografischen Pfadeordnung?

Literatur

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

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

Besprechung in der Übung am 4. Juli 2001.