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

Übungsblatt 6

zur Vorlesung Termersetzungssysteme im Sommersemester 2001 15. Juni 2001

1. [1, Exercise 5.11] Sei Σ := {+, s, d, q, 0} mit + zweistellig, s, q, d einstellig und 0 Konstante. Das

Termersetzungssystem R bestehe aus den Regeln \begin{matrix}x + 0 → & x \\ x + s(y) → & s(x + y) \\ d(0) → & 0 \\ d(s(x)) → & s(s(d(x))) \\ q(0) → & 0 \\ q(s(x)) → & q(x) + s(d(x)) \end{matrix}

Zeige, daß man mit A := ℕ \ {0, 1} und P_{0} := 2, P_{s} := X + 1, P_{+} := X + 2Y, P_{d} := 3X sowie P_{q} := X^{3} die Terminierung von R mittels Polynominterpretation beweisen kann.

2. [2, Example 11] Wir betrachten Terme, die einstellige Funktionen syntaktisch beschreiben. Setze Σ := \{\underline{c} | c ∈ ℝ\}∪\{I, +, −, ×, /, ↑, ln, D\}. Dabei beschreibe \underline{c} die entsprechende konstante Funktion, I die Identität, +, −, ×, / die naheliegenden binären Verknüpfungen einstelliger Funktionen, ↑ die Exponentiation, ln das Nachschalten des natürlichen Logarithmus sowie D die Differentiation. Die

Termersetzungsregeln seien \begin{matrix}D(\underline{c}) → & \underline{0} \\ D(I) → & \underline{1} \\ D(x + y) → & D(x) + D(y) \\ D(x − y) → & D(x) − D(y) \\ D(x × y) → & (y × D(x)) + (x × D(y)) \\ D(x/y) → & (D(x)/y) − x × (D(y)/(y ↑ \underline{2})) \\ D(x ↑ y) → & (y × (x ↑ (y − \underline{1})) × D(x)) + ((x ↑ y) × ln(x) × D(y)) \\ D(ln(x)) → & D(x)/x \end{matrix}

Zeige, daß man mit A := ℕ \ \{0, 1, 2, 3\} und P\underline{c} := 4, P_{I} := 4, P_{op} := X + Y für op ∈ \{+, −, ×, /, ↑\}, P_{ln} := X + 1 sowie P_{D} := X^{2} die Terminierung dieses Systems mittels Polynominterpretation beweisen kann.

3. [1, Exercise 5.6] Sei Σ eine Signatur mit mindestens einer Konstanten und sei > eine totale Reduktionsordnung auf T (Σ, ∅), d. h., > ist Reduktionsordnung auf T (Σ, ∅), die zusätzlich total ist (für alle s, t gilt: s > t oder s = t oder t > s). Sei weiter V eine beliebige Variablenmenge. Eine Substitution σ auf T (Σ, V) heißt geschlossen auf X ⊆ V, wenn σ(x) ∈ T (Σ, ∅) für alle x ∈ X.

Definiere eine binäre Relation ≻ auf T (Σ, V) durch s_{1} ≻ s_{2} :⇔ σ̂(s_{1}) > σ̂(s_{2}) für alle auf V ar(s_{1}) ∪ V ar(s_{2}) geschlossenen Substitutionen σ.

Zeige, daß ≻ die größte Reduktionsordnung auf T (Σ, V) ist, die > umfaßt.

Literatur

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

[2] Nachum Dershowitz. 33 examples of termination. In H. Comon and J.-P. Jouannaud, editors, Term Rewriting, French Spring School of Theoretical Computer Science, Font Romeux, France, May 1993, volume 909 of Lecture Notes in Computer Science, pages 16–26. Springer Verlag, 1995.

Besprechung in der Übung am 20. Juni 2001.