Termersetzungssysteme SS 2004 Prof. Dr. Jürgen Giesl

Mitgeschrieben von Timo Boettcher

Dieses Skript ist meine Mitschrift der Vorlesung Termersetzungssysteme im SS 2004 an der RWTH Aachen (Dozent: Prof. Dr. J. Giesl). Es handelt sich nicht um eine offizielle Veröffentlichung des “Lehr- und Forschungsgebiet Informatik II“. Ich übernehme keine Gewähr für die Fehlerfreiheit und Vollständigkeit des Skripts. Korrekturen und Ergänzungen bitte ich an timo_boettcher@post.rwth-aachen.de zu mailen. Timo Boettcher, 30. Juli 2004

Inhaltsverzeichnis

1 Einführung 5

2 Grundlagen 7 2.1 Syntax von Gleichungssytemen . . . . . . . . . . . . . . . . . . . 7 2.2 Semantik von Gleichungssystemen . . . . . . . . . . . . . . . . . 8

3 Termersetzung und Deduktion von Gleichungen 11 3.1 Deduktion von Gleichungen . . . . . . . . . . . . . . . . . . . . . 11 3.2 Der Kongruenzabschluss bei Grundidentitäten . . . . . . . . . . . 22 3.3 Termersetzungssysteme . . . . . . . . . . . . . . . . . . . . . . . 28

4 Terminierung von Termersetzungssystemen 43 4.1 Noethersche Induktion . . . . . . . . . . . . . . . . . . . . . . . . 43 4.2 Entscheidbarkeitsresultate zur Terminierung . . . . . . . . . . . . 45 4.3 Terminierung mit Reduktionsrelationen . . . . . . . . . . . . . . 48 4.4 Simplifikationsordnungen und rekursive Pfadordnungen . . . . . 51

5 Konfluenz von Termersetzungssystemen 63 5.1 Unifikation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 5.2 Lokale Konfluenz und Kritische Paare . . . . . . . . . . . . . . . 69

6 Vervollständigung von Termersetzungssystemen 81 6.1 Der grundlegende Vervollständigungsalgorithmus . . . . . . . . . 81 6.2 Ein vernesserter Vervollständigungsalgorithmus . . . . . . . . . . 85 6.3 Implizite Induktion . . . . . . . . . . . . . . . . . . . . . . . . . . 88 4 INHALTSVERZEICHNIS

Kapitel 1

Einführung

[20.04.04]

Grundformalismus zum Rechnen und Beweisen mit Gleichungen

• Spezifikation von Programmen

• Programmanalyse und Programmverifikation

• Ausführung von Programmen

• Symbolisches Rechnen

Beispiel: Datentyp zur Darstellung natürlicher Zahlen: Zwei Konstruktoren: O ← repräsentiert 0 succ ← “successor“, repräsentiert Nachfolgerfunktion 0ˆ=O 1ˆ=succ(O) 2ˆ=succ(succ(O))

Additionsalgorithmus: plus(O, Y) ≡ Y plus(succ(x), y) ≡ succ(plus(x, y))

Berechnungen: “Anwendungen“ der Gleichungen von links nach rechts Berechne 2+1:

plus(succ(succ(O)), succ(O))
→ succ(plus(succ(O), succ(O)))
→ succ(succ(plus(O, succ(O))))
→ succ(succ(succ(O)))ˆ=3

Systeme von Gleichungen wie oben bezeichnet man als Termersetzungssysteme Schreibweise: “→“ statt “≡“, um anzudeuten, das die Gleichungen von links nach rechts ausgewertet werden

Fragestellungen der Programmanalyse und Programmverifikation die man mit Termersetzungstechniken automatisch lösen will:

• Ist das Resultat eines Programmes immer eindeutig? (Konfluenz) plus(O, plus(succ(O), O))

→ plus(succ(O), O) oder → plus(O, succ(plus(O, O)))

→ succ(O)

plus ist deterministisch, andere Programme nicht.

• Hält das Programm immer nach endlich vielen Schritten an? (Terminierung)

plus terminiert, denn in jedem rekursiven Aufruf wird das 1. Argument kleiner

• Erfüllt das Programm seine Spezifikation? (Korrektheit)

Gilt zum Beispiel plus(succ(succ(O)), X) ≡ plus(succ(O), succ(X)), das heisst, folgt eine bestimmte Aussage aus bestimmten Axiomen?

Anderes Beispiel: Axiome zur Spezifikation von Gruppen:

f(x, f(y, z)) ≡ f(f(x, y), z)
f(x, e) ≡  x
f(x, i(x)) ≡  e

Gilt i(i(n)) ≡ n? Kann man durch „Probieren“ lösen. (lang und umständlich) Mit Termersetzung kann man solche Beweise automatisch führen. Wie kann man ein unvollständiges Programm automatisch vervollständigen?

Grundlagen

Sprache der Terme und der Gleichungen: (Teilmenge der) Prädikatenlogik 1. Stufe (Syntax und Semantik)

2.1 Syntax von Gleichungssytemen

Definition 2.1.1: Signatur (Alphabet, aus dem Ausdrücke unserer Sprache, also Terme, gebildet werden) Eine Signatur Σ = ∪_{i∈ℕ}Σ_{i} ist eine Vereinigung von paarweise disjunkten endlichen Mengen Σ_{i}. Jedes f ∈ Σ_{i} heisst i-stelliges Funktionssymbol. Elemente von Σ_{0} heissen auch Konstanten. Wir verlangen stets, das Σ endlich ist und es mindestens eine Konstante gibt.

Beispiel 2.1.2: Σ = Σ_{0} ∪ Σ_{1} ∪ Σ_{2}, Σ_{0} = O, Σ_{1} = succ, Σ_{2} = plus, times

Definition 2.1.3: Terme (“Datenobjekte“) Sei Σ eine Signatur, sei V eine nicht-leere unendliche Menge von Variablen mit Σ ∩ V = ∅. T (Σ, V) ist die Menge der Terme über Σ und V, wobei T (Σ, V) die kleinste Teilmenge von (Σ ∪ V ∪ {(,), “, “}^{∗} mit:

1. V ⊆ T (Σ, V)

2. f(t_{1}, …, t_{n}) ∈ T (Σ, V) falls, f ∈ Σ_{n}, t_{i} ∈ T (Σ, V) für alle i ∈ {1, …, n}

Falls f ∈ Σ_{0}, dann ist f ∈ T (Σ, V) Für einen Term t ist V(t) die Menge der Variablen in t und für T ⊆ T (Σ, V) ist V(T) = ∪_{t∈T} V(t) T (Σ) steht für T (Σ, ∅) (Menge der Grundterme).

Beispiel 2.1.4: Sei Σ wie in Beispiel 2.1.2 (Σ = {O, succ, plus, times}) O, succ(O), plus(O, succ(O)) ∈ T (Σ)

plus(times(O, \underbrace{X}_{∈V}, succ(\underbrace{Y}_{∈V}) ∈ T (Σ, V)

Terme lassen sich als Vielwegbäume darstellen:

\xymatrix{ &  &  & plus \ar[dll] \ar[dr] \\  & times \ar[dl] \ar[dr] &  &  & succ \ar[d] \\ O &  & X &  & Y}

Definition 2.1.3: (Fortsetzung) Ein Term q ist Teilterm von t (t ⊵ q) gdw. t = q, oder t = f(t_{1}, …, t_{n}) und t_{i} ⊵ q für ein i ∈ {1, …, n} Die Terme t_{1}, …, t_{n} sind direkte Teilterme von f(t_{1}, …, t_{n}). Ein Teilterm q von t ist echter Teilterm von t(t ▷ q) wenn t ⊵ q und t ≠ q.

Beispiel 2.1.4: (Fortsetzung) t = plus(times(O, X), succ(y)) direkte Teilterme: times(O, X), succ(y). Andere echte Teilterme O, X, Y

Definition 2.1.5: Gleichungen Für t_{1}, t_{2} ∈ T (Σ, V) heisst t_{1} ≡ t_{2} Gleichung (über Σ und V). (“≡“ bezeichnet Gleichheitssymbol) Eine Menge E von Gleichungen heisst Gleichungssystem. Mit Gleichungen kann man \underbrace{Programme}_{z.B. plus}, \underbrace{Datentypen}_{z.B. Gruppen} etc. axiomatisieren.

2.2 Semantik von Gleichungssystemen

Zur Definition der Semantik versucht man Interpretationen, die eine Menge von Objekten A festlegen und jedem Funktionssymbol f eine Funktion A_{f} zuordnen, jeder Variable X ein Objekt β(X) ∈ A zuordnen.

Definition 2.2.1: Interpretation, Algebra Für eine Signatur Σ ist eine Σ-Interpretation ein Tupel I = (A, α, β). A ist der Träger der Interpretation mit A ≠ ∅, A = (α_{f})_{f} ∈ Σ, wobei α_{f} : A × A × ⋯ × A → A für f ∈ Σ_{n}

[23.04.04] Beispiel 2.2.2: I = (A, α, β), Σ aus Beispiel 2.1.2, V = X, Y, … A = ℕ = 0, 1, 2, … α_{0} = 0

\begin{matrix}α_{succ}(n) & = n + 1 \\ α_{plus}(n, m) & = n + m \\ α_{times}(n, m) & = n ∗ m \end{matrix}\} (n, m ∈ ℕ)

Definition 2.2.1: (Fortsetzung) α_{f} heisst Deutung des Funktionssymbols f unter der Interpretation I. Die Abbildung β : V → A heisst Variablenbelegung für die Interpretation I. Zu jeder Interpretation erhält man eine Funktion I: T (Σ, V) → A wie folgt: I(x) = β(x) für alle x ∈ V I(f(t_{1}, …, t_{n})) = α_{f}(I(t_{1}), …, I(t_{n})) für alle f ∈ Σ_{n} und t_{1}, …, t_{n} ∈ T (Σ, V) I(t) heisst Interpretation des Terms t. Eine Σ-Interpretation ohne Variablenbelegung (A, α) heisst Σ-Algebra

Beispiel 2.2.2: (Fortsetzung)

I(plus(succ(x), y)) = α_{plus}(\underbrace{α_{succ}(\underbrace{β(x)}_{5})}_{6}, \underbrace{β(y)}_{3})

I′ = (A, α, β′) mit β′(x) = 2, β′(y) = 1 I′(plus(succ(x), y)) = (2 + 1) + 1 = 4

I′′ = (ℚ, α′′, β) wobei  α′′ = 0
α′′_{succ}(n) = n + 1
α′′_{plus}(n, m) = \frac{n}{m},  falls m ≠ 0

sonst 0 (α_{f} muss total sein)

α′′_{times}(n, m) = n ∗ m I′′(plus(succ(x), y) = \frac{6}{3} = 2

Definition 2.2.3: Erfüllen von Gleichungen, Modell Eine Interpretation I = (A, α, β) erfüllt eine Gleichung t_{1} ≡ t_{2} gdw. I(t_{1}) = I(t_{2}) Eine Algebra A = (A, α) erfüllt eine Gleichung t_{1} ≡ t_{2} gdw. I(t_{1}) = I(t_{2}) für alle Interpretationen I = (A, α, β) Für alle Variablenbelegungen β müssen die Deutungen von t_{1} und t_{2} also identisch sein. (Variablen sind implizit allquantifiziert). Schreibweise: I ⊨ t_{1} ≡ t_{2} bzw. A ⊨ t_{1} ≡ t_{2}.

Anstelle von Erfüllbarkeit spricht man auch von Modellen: A ⊨ t_{1} ≡ t_{2} bedeutet „A ist Modell von t_{1} ≡ t_{2}“ Algebra A ist Modell einer Gleichungsmenge E(A ⊨ E) gdw. A ⊨ t_{1} ≡ t_{2} für alle t_{1} ≡ t_{2} ∈ E

Beispiel 2.2.4: I = (ℕ, α, β) (β(x) = 5, β(y) = 3) I ⊨ plus(x, y) ≡ succ(succ(succ(succ(succ(succ(succ(succ(O)))))))) (I Interpretiert beide Terme als 8) A = (ℕ, α) A ⊭ plus(x, y) ≡ succ(succ(succ(succ(succ(succ(succ(succ(O)))))))) A ⊨ plus(x, y) ≡ plus(y, x) I′′ ⊭ plus(x, y) ≡ plus(y, x) (α′′_{plus}(n, m) = \frac{n}{m}, falls m ≠ 0)

Definition 2.2.3: (Fortsetzung) Aus einer Gleichungsmenge E folgt die Gleichung t_{1} ≡ t_{2} (E ⊨ t_{1} ≡ t_{2}) gdw. Für alle Algebren A mit A ⊨ E auch A ⊨ t_{1} ≡ t_{2} gilt. Statt ∅ ⊨ t_{1} ≡ t_{2} schreibt man auch ⊨ t_{1} ≡ t_{2}. Solche Gleichungen heissen allgemeingültig (alle Algebren sind Modelle von t_{1} ≡ t_{2}). “⊨“ wird sowohl für Erfüllbarkeit als auch für Folgerbarkeit benutzt, was gemeint ist, erkennt man daran, ob links eine Interpretation/Algebra oder eine Gleichungsmenge steht. Wir definieren die Relation ≡_{E} auf T (E, V) × T (Σ, V) als s ≡_{E} t gdw. E ⊨ s ≡ t.

Beispiel 2.2.4: (Fortsetzung) {plus(x, y) ≡ plus(y, x)} ⊨ plus(O, succ(O)) ≡ plus(succ(O), O) Falls E = {plus(x, y) ≡ plus(y, x)} dann plus(O, succ(O)) ≡_{E} plus(succ(O), O) Wäre E = Gruppenaxiome, dann i(i(n)) ≡_{E} n

Die Frage, ob s ≡_{E} t für zwei Terme s, t und ein Gleichungssystem E gilt, heisst Wortproblem. Ziel: Löse Wortproblem (möglichst automatisch)

Termersetzung und Deduktion von Gleichungen

3.1 erstes naives Verfahren 3.2 Verfahren für den Spezialfall der Grundterme (Kongruenzabschluss) 3.3 Vefahren für den allgemeinen Fall (Termersetzungssysteme)

3.1 Deduktion von Gleichungen

Um s ≡_{E} t zu untersuchen, müssen unendlich viele Algebren und unendlich viele Variablenbelegungen betrachtet werden. ≡_{E} ist semantisch definiert, ungeeignet für Automatisierung. Ziel: Definiere eine syntaktische Relation, die ≡_{E} entspricht, aber für die Automatisierung geeignet ist. → syntaktische Begriffe zur Manipulation von Termen.

Definition 3.1.1: Substitution, Matching Eine Abbildung σ : V → T (Σ, V) mit σ(x) ≠ x für endlich viele Variablen x heisst Subsitution. SUB(Σ, V) ist die Menge aller Substitutionen. Die identische Substitution wird mit id bezeichnet (d.h. id(x) = x für alle x ∈ V) DOM(σ) = {x ∈ V|σ(x) ≠ x} heisst die Domain von σ. Da DOM(σ) endlich ist, kann man jede Substitution als endliche Menge von Paaren darstellen: {x/σ(x)|x ∈ DOM(σ)}

12KAPITEL 3. TERMERSETZUNG UND DEDUKTION VON GLEICHUNGEN

Beispiel 3.1.2: Σ wie in Beispiel 2.1.2 σ(x) = plus(x, y), σ(y) = O, σ(z) = succ(z), σ(u) = u für alle u ∈ V\{x, y, z}. DOM(σ) = {x, y, z} Schreibweise: σ = {x/plus(x, y), y/O, z/succ(z)} Definition 3.1.1: (Fortsetzung) Substitutionen werden homomorph zu Abbildungen auf Termen erweitert (σ : T (Σ, V) → T (Σ, V)), wobei: σ(f(t_{1}, …, t_{n})) = f(σ(t_{1}), …, σ(t_{n})). Für zwei Terme s, t sagt man, dass s den Term t matcht gdw. es eine Substitution σ gibt mit σ(s) = t. Die Substitution σ heisst Matcher von s und t.

Beispiel 3.1.2: (Fortsetzung) σ(plus(x, y)) = plus(σ(x), σ(y)) = plus(plus(x, y), O) Der Term plus(x,y) matcht den Term plus(plus(x, y), O) und σ ist ein Matcher

Um ≡_{E} auf syntaktische Weise nachzubilden, versuchen wir, die Eigenschaften von ≡_{E} zu untersuchen. Eine Eigenschaft ≡_{E} ist stabil (d.h. abgeschlossen unter Subtitutionen)

Definition 3.1.3: Stabilität Eine Relation → über Termen (d.h. → ⊆ T (Σ, V) × T (Σ, V)) heisst stabil (oder abgeschlossen unter Substitution) gdw. für alle Terme t_{1}, t_{2} und alle Substitutionen σ gilt: Falls t_{1} → t_{2}, dann σ(t_{1}) → σ(t_{2})

[30.04.04] Ziel: Ersetze die semantische Relation ≡_{E} durch eine syntaktische Relation, die sich automatisch überprüfen lässt. Hierzu: Untersuche die Eigenschaften von ≡_{E}. Schreibweise für Substitution: Für x^{∗} = x_{1}, …, x_{n} ∈ V^{∗} mit x_{i} ≠ x_{j} für i ≠ j

und t^{∗} = \underbrace{t_{1}}_{∈V}, …, \underbrace{t_{n}}_{∈ T (Σ, V)^{∗}}schreiben statt \{x_{1}/t_{1}, …, x_{n}/t_{n}\} auch \{x^{∗}/t^{∗}\}, statt

“σ(t)“ schreiben wir auch “tσ“. Stabilität: plus(x, y) → plus(O, x) ↷ plus(s(O), s(s(O))) → plus(O, s(O)). Wir zeigen ≡_{E} ist stabil.: t_{1} ≡_{E} t_{2} ↷ t_{1}σ ≡_{E} t_{2}σ wenn: plus(x, y) ≡ plus(O, x) ∈ E dann: plus(s(O), s(s(O))) ≡_{E} plus(O, s(O)) Beweisprinzip: strukturelle Induktion über Terme zu Zeigen: φ(t) für alle t ∈ T (E, V) Induktionsanfang:

• t ist eine Variable t ∈ V zeige: φ(t)

• t ist eine Konstante c ∈ Σ_{0} zeige: φ(t)

Induktionsschluss: t = f(t_{1}, …, t_{n}), n > 0 zeige: \underbrace{φ(t_{1}) ∧ ⋯ ∧ φ(t_{n})}_{Induktionshypothese} → \underbrace{φ(f(t_{1}, …, t_{n}))}_{Induktionskonklusion}

Intuitiv: Beweisprinzip korrekt, da es direkt dem rekursiven Aufbau der Datenstruktur der Terme entspricht. Analoge Induktionsbeweise sind für alle rekursiv definierten Datenstrukturen möglich.

Formal: ist Spezialfall eines allgemeinen Beweisprinzips (noethersche Induktion) ↷ Kapitel 4

Lemma 3.1.4: ≡_{E} stabil (Teil (a) zeigt Zusammenhang zwischen “Substitution“ (syntaktisch) und “Variablenbelegung“ (semantisch)) Sei I = (A, α, β) eine Σ-Interpretation, seien s, t ∈ T (Σ, V)), sei σ ∈ SUB(Σ, V) und sei I′ = (A, α, β′) mit β′(x) = I(xσ) für alle x ∈ V z.B.

I = (ℕ, α, β),
α_{succ}(n) = n + 1,

α_{plus}(n, m) = n + m, I′ = (ℕ, α, β′) mit β(x) = 5

β′(x) = I( \underbrace{xσ}_{\xymatrix{ & succ(x) \ar[dl] \ar[dr] \\ α_{succ} & & 5}} ) = 6

a) I( \underbrace{plus(x, x)σ}_{plus(s(x),s(x))}) = 12

I′(plus(\underbrace{x}_{6}, \underbrace{x}_{6})) = 12

b) I ⊨ \underbrace{s^{6}(x)σ}_{\underbrace{s^{7}(x)}_{12}} = \underbrace{plus(x, x)σ}_{\underbrace{plus(s(x), s(x))}_{12}}

I′ ⊨ \underbrace{s^{6}(x)}_{12} ≡ \underbrace{plus(x, x)}_{12}

c) A ⊨ plus(x, O) ≡ x ↷ A ⊨ plus(s(x), O) ≡ s(x)

a) I(tσ) = I′(t) (Substitutionslemma)

b) I ⊨ sσ ≡ tσ gdw. I′ ⊨ s ≡ t

c) Für alle Σ-Algebren A gilt: Wenn A ⊨ s ≡ t, dann A ⊨ sσ ≡ tσ

d) für alle Gleichungssysteme E: Falls s ≡_{E} t, dann sσ ≡_{E} tσ

d.h.: ≡_{E} ist stabil

Beweis: a) Zeige φ(t) durch strukturelle Induktion über t

φ(t): „Für alle Substitutionen σ und alle Interpretationen I, I′ wie oben gilt: I(tσ) = I′(t)“ Induktionsanfang: t ist eine Variable x ∈ V: I(xσ) ∥ I′(x) = β′(x) = I(xσ) Vereinfachung: Betrachte den Fall t = c ∈ Σ_{0} nicht extra, sondern nur den Fall t = f(t_{1}, ..t_{n}), n ≥ 0 zu Zeigen: \underbrace{φ(t_{1}) ∧ … ∧ φ(t_{n})}_{im Fall n=0 steht hier “nichts“, d.h. dort muss man φ(f) direkt zeigen} → φ(f(t_{1}, …, t_{n}))

Induktionsschluss: t = f(t_{1}, …, t_{n}), n ≥ 0 Induktionshypothese: φ(t_{1}) für alle 1 ≤ i ≤ n „Für alle σ, I, I′ : I(t_{i}σ) = I′(t_{i})´ ´

I(tσ) = I(f(t_{1}, …, t_{n})σ) = I(f(t_{1}σ, …, t_{n}σ)) = α_{f}(I(t_{1}σ), …, I(t_{n}σ)) =^{I.H.}

α_{f}(I′(t_{1}), …, I′(t_{n})) = I′(f(t_{1}, …, t_{n})) = I′(t)

b) I ⊨ sσ ≡ tσ gdw. I(sσ) = I(tσ) gdw. I(sσ) = I(sσ) gdw. I′(s) = I′(t) gdw. I′ ⊨ s ≡ t

c) Sei A = (A, α) mit A ⊨ s ≡ t. Zu Zeigen ist: A ⊨ sσ ≡ tσ, d.h. für alle Interpretationen I = (A, α, β) gilt: I ⊨ sσ ≡ tσ Nach (b) genügt es zu zeigen, dass I′ ⊨ s ≡ t, wobei I′(A, α, β′) mit β′(x) = I(xσ) für alle x ∈ V Aus A ⊨ s ≡ t folgt aber I′ ⊨ s ≡ t, da I’ und A gleichen Träger A und gleiche Deutungsfunktion α haben.

d) Sei s ≡_{E} t, d.h. E ⊨ s ≡ t. Das bedeutet: Für alle Algebren A mit A ⊨ E gilt: A ⊨ s ≡ t. ↷^{(c)} Für alle Algebren A mit A ⊨ E gilt A ⊨ sσ ≡ tσ ↷ sσ ≡_{E} tσ

□

Definition 3.1.5: Stelle Für einen Term t ist Occ(t) die Menge aller Stellen von t, wobei Occ(t) die kleinste Teilmenge von ℕ^{∗} ist mit:

• ϵ ∈ Occ(t)

• iπ ∈ Occ(t), falls t = f(t_{1}, …, t_{n}), 1 ≤ i ≤ n, π ∈ Occ(t_{i})

Für einen Term t und π ∈ Occ(t) bezeichnet t|_{π} den Teilterm von t an der Stelle π, wobei

• t|_{ϵ} = t

• f(t_{1}, …, t_{n})|_{iπ} = t_{i}|_{π}

Beispiel 3.1.6: t = plus(s(plus(O, s(O))), s(O)),

\xymatrix{ &  & plus \ar[dl]_{1} \ar[dr]^{2} \\  & s \ar[d]_{1} &  & s \ar[d]^{1} \\  & plus \ar[dl]_{1} \ar[dr]^{2} &  & O \\ O &  & s \ar[d]^{1} \\  &  & O}

t|_{ϵ} = t t|_{1} = s(plus(O, s(O))) t|_{112} = s(O) t|_{21} = O

Definition 3.1.5: (Fortsetzung) Für t und π ∈ Occ(t) und Term v bezeichnet t[v]_{π} den Term, der aus t entsteht, indem t|_{π} durch v ersetzt wird, d.h.

• t[v]_{ϵ} = v

• f(t_{1}, …, t_{n})[v]_{iπ} = f(t_{1}, …, t_{i−1}, t_{i}[v]_{π}, t_{i+1}, …, t_{n})

Beispiel 3.1.6: (Fortsetzung) t[times(O, O)]_{112} = plus(s(plus(O, times(O, O))), s(O))

Definition 3.1.5: (Fortsetzung) Für π_{1}, π_{2} ∈ Occ(t) ist π_{1} unterhalb von π_{2} (π_{1} >_{ℕ^{∗}} π_{2}) gdw. π_{2} ein echtes Anfangsstück von π_{1} ist (d.h.: π_{1} = π_{2}π für ein π ∈ ℕ^{+}). π_{1} und π_{2} sind voneinander unabhängig (π_{1} ⊥ π_{2}) gdw. weder π_{1} >_{ℕ^{∗}} π_{2} noch π_{2} >_{ℕ^{∗}} π_{1} Beispiel: 112 >_{ℕ^{∗}} 11 >_{ℕ^{∗}} 1 >_{ℕ^{∗}} ϵ, 111 ⊥ 112

Definition 3.1.7: Monotonie Eine Relation → über Termen heisst monoton gdw. für alle Terme t_{1}, t_{2}, q und alle π ∈ Occ(q) gilt: Wenn t_{1} → t_{2}, dann q[t_{1}]_{π} → q[t_{2}]_{π} Beispiel: plus(x, O) → x ↷ s(plus(x, O)) → s(x) Strukturelle Induktion ist auch über Stellen π möglich.

[07.05.04] Lemma 3.1.8: ≡_{E} monoton Seien s, t, q ∈ T (Σ, V) und π ∈ Occ(q). Dann gilt:

a) Für alle Σ-Algebren A gilt: Falls A ⊨ s ≡ t, dann A ⊨ q[s]_{π} ≡ q[t]_{π}

b) Für alle Gleichungssysteme E gilt: Falls s ≡_{E} t, dann q[s]_{π} ≡_{E} q[t]_{π}, d.h.

≡_{E} ist monoton. Beweis:

a) Strukturelle Induktion über π. Die Aussage φ(π), die wir beweisen wollen, lautet: φ(π): „Für alle Algebren A und alle Terme s, t, q mit π ∈ Occ(q) gilt: A ⊨ s ≡ t ↷ A ⊨ q[s]_{π} ≡ q[t]_{π}.“ Induktionsanfang: π = ϵ q[s]_{ϵ} = s, q[t]_{ϵ} = t

↷ A ⊨ s ≡ t ↷ A ⊨ \underbrace{q[s]_{ϵ}}_{s} ≡ \underbrace{q[s]_{ϵ}}_{t}

Induktionsschluss: π = iπ′ Da iπ′ ∈ Occ(q), hat q die Gestalt f(q_{1}, …, q_{i}, …, q_{n}) und π′ ∈ Occ(q_{i}). q[s]_{iπ′} = f(q_{1}, …, q_{i}[s]_{π′}, …, q_{n}) q[t]_{iπ′} = f(q_{1}, …, q_{i}[t]_{π′}, …, q_{n}) Sei A = (A, α) mit A ⊨ s ≡ t. Zu zeigen ist, dass für alle Interpretationen I = (A, α, β) mit beliebigen β gilt: I ⊨ f(q_{1}, …, q_{i}[s]_{π′}, …, q_{n}) ≡ f(q_{1}, …, q_{i}[t]_{π′}, …, q_{n}) d.h.: α_{f}(I(q_{1}), …, I(q_{i}[s]_{π′}), …, I(q_{n})) = α_{f}(I(q_{1}), …, I(q_{i}[t]_{π′}), …, I(q_{n})) Hierfür genügt es zu zeigen, dass I(q_{i}[s]_{π′}) = I(q_{i}[t]_{π′}). Induktionshypothese: φ(π′): „Für alle A, s, t, q̄ mit π′ ∈ Occ(q̄) gilt: A ⊨ s ≡ t ↷ A ⊨ q̄[s]_{π′} ≡ q̄[t]_{π′}.“ Da die Induktionshypothese für alle q̄ zur Verfügung steht, steht sie auch für q̄:= q_{i} zur Verfügung. D.h.: Da π′ ∈ Occ(q_{i}), gilt aufgrund der Induktionshypothese: A ⊨ q_{0}[s]_{π′} ≡ q_{i}[t]_{π′} ↷ I ⊨ q_{i}[s]_{π′} ≡ q_{i}[t]_{π′} ↷ (*) gilt.

3.1. DEDUKTION VON GLEICHUNGEN 17

b) s ≡_{E} t ↷ E ⊨ s ≡ t ↷ für alle Algebren A: A ⊨ E ↷ A ⊨ s ≡ t ↷^{(a)} für alle Algebren A: A ⊨ E ↷ A ⊨ q[s]_{π} ≡ q[t]_{π} ↷ q[s]_{π} ≡_{E} q[t]_{π} ≡_{E} stabil und monoton

□

Definition 3.1.9: Äquivalenzrelation, Kongruenzrelation Sei M eine Menge und sei → eine Relation auf M (→ ⊆ M × M). Man sagt auch, (M, →) ist ein abstraktes Reduktionssystem (ARS). Die Relation „→“ heisst

• reflexiv, falls t → t für alle t ∈ M gilt (Bsp:. ≥ auf ℕ, ⊵ (Teiltermrelation), = auf ℕ, …)

• symmetrisch, falls aus t_{1} → t_{2} jeweils t_{2} → t_{1} folgt, für alle t_{1}, t_{2} ∈ M (Bsp.: = auf ℕ)

• transitiv, falls aus t_{1} → t_{2} und t_{2} → t_{3} jeweils t_{1} → t_{3} folgt, für alle t_{1}, t_{2}, t_{3} ∈ M (Bsp.: ≥ auf ℕ, ⊵, =)

• Äquivalenzrelation, falls → reflexiv, symmetrisch und transitiv ist (Bsp.:

= auf ℕ) Die reflexive Hülle von → (Bezeichnung: →^{=}) ist die kleinste reflexive Relation, die → enthält, d.h.:

• wenn t_{1} → t_{2}, dann t_{1} →^{=} t_{2}

• t →^{=} t (>^{=}=≥, ▷^{=} = ⊵) Die transitive Hülle →^{+} ist die kleinste transitive Relation, die → enthält, d.h.:

• wenn t_{1} → t_{2}, dann t_{1} →^{+} t_{2}

• wenn t_{1} → t_{2} →^{+} t_{3}, dann t_{1} →^{+} t_{3} (s → t bedeutet also, dass es s_{0}, …, s_{n} mit n > 0 gibt, mit s = s_{0} → s_{1} → … → s_{n} = t) (Bsp.: →⊆ ℕ × ℕ, x → y gdw. x = y + 1 5 → 4, 4 → 3

Die transitiv-reflexive Hülle →^{∗} ist die kleinste transitive und reflexive Relation, die → enthält, d.h.:

• wenn t_{1} →^{+} t_{2}, dann t_{1} →^{∗} t_{2}

• t →^{∗} t Die Relation ↔ ist die symmetrische Hülle von →, d.h. es gilt t_{1} ↔ t_{2} gdw. t_{1} → t_{2} oder t_{2} → t_{1}. Die Relation ↔^{∗} ist also die kleinste Äquivalenzrelation, die → enthält. Eine Äquivalenzrelation → über Termen T (Σ, V) heisst Kongruenzrelation, wenn für alle f ∈ Σ und alle s_{1}, …, s_{n}, t_{1}, …, t_{n} ∈ T (Σ, V) mit s_{1} → t_{1}, …, s_{n} → t_{n} folgt: f(s_{1}, …, s_{n}) → f(t_{1}, …, t_{n})

Lemma 3.1.10: ≡_{E} ist Kongruenzrelation Für alle Gleichungssysteme E ist ≡_{E} eine Äquivalenz- und Kongruenzrelation. Beweis: Übung Beweisidee: Äquivalenz: (A ⊨ t ≡ t, A ⊨ s ≡ t ↷ A ⊨ t ≡ s, A ⊨ s ≡ t und A ⊨ t ≡ r ↷ A ⊨ s ≡ r) Kongruenz: ≡_{E} monoton; Jede monotone Äquivalenzrelation ist eine Kongruenzrelation.

Ziel: s ≡_{E} t automatisch beweisen. Dann: Ersetze semantische Relation ≡_{E} durch eine syntaktische Relation, die automatisch überprüft werden kann.

Definition 3.1.11: Ersetzungsrelation Für ein Gleichungssystem E ist die Ersetzungsrelation →_{E}⊆ T (Σ, V) × T (Σ, V) definiert als: s →_{E} gdw. s|_{π} = t_{1}σ und t = s[t_{2}σ]_{π} für eine Stelle π ∈ Occ(s), eine Gleichung t_{1} ≡ t_{2} ∈ E und eine Substitution σ ∈ SUB(Σ, V) (Bsp.: plus(x, O) ≡ x ∈ E plus(O, O) →_{E} O, s(plus(O, O)) →_{E} s(O)) Die Relation ↔_{E}^{∗} heisst Beweisrelation von E (s ↔_{E}^{∗} t falls s = s_{0} ↔_{E} s_{1} ↔_{E} … ↔_{E} s_{n} = t). Wir sagen s ≡ t ist aus E herleitbar („E ⊢ s ≡ t“) gdw. s ↔_{E}^{∗} t D.h.: \underbrace{E ⊨ s ≡ t}_{Semantik(s≡_{E}t)} \underbrace{gdw.}_{(Satz von Birkhoff)} \underbrace{E ⊢ s ≡ t}_{Syntax(↔_{E}^{∗}t)}

Beispiel 3.1.12: E = {plus(O, y) ≡ y, plus(succ(x), y) ≡ succ(plus(x, y))} Gilt: plus(s(s(O)), x) ≡_{E} plus(s(O), s(x))? Es gilt: plus(s(s(O)), x) ⇔_{E}^{∗} plus(s(O), s(x)) [Folie] Erstes automatisierbares Verfahren, um das Wortproblem zu lösen.

Lemma 3.1.13: ↔_{E}^{∗} stabile und monotone Kongruenzrelation Sei E ein Gleichungssystem, s, t, q ∈ T (Σ, V), π ∈ Occ(q), σ ∈ SUB(Σ, V) Dann ist ↔_{E}^{∗} eine Äquivalenz- und Kongruenzrelation und es gilt: a)

\begin{matrix}Falls →_{E} t, dann sσ →_{E} tσ \\ Falls ↔_{E}^{∗} t, dann sσ ↔_{E}^{∗} tσ \end{matrix}\} d.h. →_{E} und ↔_{E}^{+} sind stabil.

b)

\begin{matrix}Falls →_{E} t, dann sq[s]_{π} →_{E} q[t]_{π} \\ Falls ↔_{E}^{∗} t, dann sq[s]_{π} ↔_{E}^{∗} q[t]_{π} \end{matrix}\} d.h. →_{E} und ↔_{E}^{+} sind monoton.

Beweis: Übung Schritt von →_{E} nach ↔_{E}^{∗}: Induktion über Anzahl der ↔_{E} Schritte

[11.05.04]

Wortproblem: s ≡_{E} t(E ⊨ s ≡ t) Eigenschaften von ≡_{E} : stabil, monoton, Äquivalenzrelation, Kongruenzrelation Beweisrelation: s ↔_{E}^{∗} t(E ⊢ s ≡ t) (Syntax)

Satz 3.1.14: Birkhoff, 1935 Sei E ein Gleichungssystem. Dann sind die Relationen ≡_{E} und ↔_{E}^{∗} identisch, d.h. es gilt E ⊨ s ≡ t gdw. E ⊢ s ≡ t für alle Terme s und t. Beweis: Korrektheit (s ↔_{E}^{∗} t ↷ s ≡_{E} t) Zeige zunächst: s ↔_{E} t ↷ s ≡_{E} t (*) Es existiert eine Gleichung t_{1} ≡ t_{2} oder t_{2} ≡ t_{1} in E, so dass s|_{π} = t_{1}σ und t = s[t_{2}σ]_{π} für ein π ∈ Occ(s) une eine Substitution σ. Es gilt: t_{1} ≡_{E} t_{2} (wegen der Symmetrie von ≡_{E}, Lemma 3.1.10) t_{1}σ ≡_{E} t_{2}σ (wegen Stabilität von ≡_{E}, Lemma 3.1.4(d)) \underbrace{s[t_{1}σ]_{π}}_{s} ≡_{E} \underbrace{s[t_{2}σ]_{π}}_{t} (wegen Monotonie von ≡_{E}, Lemma 3.1.8 (b))

somit gilt (*) Zeigen nun s ↔_{E}^{∗} t ↷ s ≡_{E} t, d.h. für alle n ∈ ℕ: s ↔_{E}^{n} t ↷ s ≡_{E} t Induktion über n (ˆ= Induktion über die Länge der Herleitung s ↔_{E}^{∗} t) Induktionsanfang: n = 0 s ↔_{E}^{0} t ↷ s = t ↷ s ≡_{E} t (wegen der Reflexivität von ≡_{E}, Lemma 3.1.10) Induktionsschluss: n > 0 s = s_{0} ↔_{E} s_{1} ↔_{E} s_{2} ↔_{E} … ↔_{E} s_{n−1} ↔_{E} s_{n} = t

\begin{matrix}Induktionshypothese: s ↔_{E}^{n−1} s_{n−1} ↷ s ≡_{E} s_{n−1} \\ wegen (*): s_{n−1} ↔_{E} t ↷ s_{n−1} ≡_{E} t \end{matrix}\}

s ≡_{E} t

(wegen Transitivität von ≡_{E} , Lemma 3.1.10)

Vollständigkeit s ≡_{E} t ↷ s ↔_{E}^{∗} t s ≡_{E} t bedeutet: A ⊨ E ↷ A ⊨ s ≡ t Vorgehen:

1. Definiere eine Interpretation I = (A, α, β), so dass I ⊨ s ≡ t gdw s ↔_{E}^{∗} t

2. Zeige, dass A = (A, α) ein Modell von E ist, d.h. A ⊨ E ↷ Dann ist die Vollständigkeit bewiesen: s ≡_{E} t ↷ A ⊨ s ≡ t (denn A ⊨ E nach (2)) ↷ I ⊨ s ≡ t ↷ s ↔_{E}^{∗} t (nach (1))

Schritt (1):

1.Idee: A = T (Σ, V), Interpretiere jeden Term t als „sich selbst“ α_{f} = f, β(x) = x Dann gilt: I(t) = t für alle Terme t (strukturelle Induktion über t) (Falls E die plus-Gleichungen sind, dann: plus(O, O) ↔_{E} O

I ⊭ plus(O, O) ≡ O, denn \underbrace{I(plus(O, O))}_{plus(O,O)} ≠ \underbrace{I(O)}_{O})

2.Idee: Wähle Träger A anders: Wir wissen, dass ↔_{E}^{∗} eine Äquivalenzrelation ist (Lemma 3.1.13). [s]_{↔_{E}^{∗}} ist die Äquivalenzklasse von s, wobei [s]_{↔_{E}^{∗}} = t|s ↔_{E}^{∗} t Da ↔_{E}^{∗} eine Äquivalenzrelation ist, sind zwei Äquivalenzklassen [s]_{↔_{E}^{∗}} und [t]_{↔_{E}^{∗}} entweder identisch oder disjunkt. ↷ Die Menge der Terme T (Σ, V) zerfällt also in mehrer disjunkte Äquivalenzklassen. Die Menge dieser Äquivalenzklassen ist die Quotientenmenge T (Σ, V)/_{↔_{E}^{∗}} = [s]_{{} ↔_{E}^{∗}|s ∈ T (Σ, V)} (Beispiel: E_{plus}T (Σ, V)/_{↔_{E}^{∗}} = {[0]_{↔_{E}^{∗}} , [s(O)]_{↔_{E}^{∗}} , …, [x]_{↔_{E}^{∗}} , [y]_{↔_{E}^{∗}} , …, [plus(x, y)]_{↔_{E}^{∗}} , …} [O]_{↔_{E}^{∗}} = {O, plus(O, O), plus(plus(O, O), O), …} [X]_{↔_{E}^{∗}} = {x, plus(O, x), …}) Definiere I so, dass A = T (Σ, V)/_{↔_{E}^{∗}} und I(t) = [t]_{↔_{E}^{∗}} (jeder Term soll als seine Äquivalenzklasse interpretiert werden) Dann gilt I ⊨ s ≡ t gdw. I(s) = I(t) gdw. [s]_{↔_{E}^{∗}} = [t]_{↔_{E}^{∗}} gdw. s_{↔_{E}^{∗}} t

α_{f}: Wir wollen, dass I(f(t_{1}, …, t_{n})) = α_{f}(I(t_{1}), …, I(t_{n})) = α_{f}([t_{1}], …, [t_{n}]) =^{!}

[f(t_{1}, …, t_{n})] Definiere daher: α_{f}([t_{1}]_{↔_{E}^{∗}} , .., [t_{n}]_{↔_{E}^{∗}}) = [f( \underbrace{t_{1}}_{irgendein Term aus [t_{1}]_{↔_{E}^{∗}}, man könnte auch einen beliebigen Term s_{1} ∈ [t_{1}] nehmen, denn aus s_{1} ↔_{E}^{∗} t_{1} ↷ f(s_{1}, …) ↔_{E}^{∗} \underbrace{f(t_{1}, …)}_{weil↔_{E}^{∗}Kongruenzrelation}} , …, t_{n})]_{↔_{E}^{∗}}

β: Wir wollen, dass I(x) = [x] ↷ β(x) = [x] Strukturelle Induktion: I(t) = [t]_{↔_{E}^{∗}} Schritt(2): Zeige: A = (A, α_{f}) ist Modell von E, d.h. für alle Variablenbelegungen γ gilt für J = (A, α, γ), dass J ⊨ E Sei u ≡ v ∈ E. Zu Zeigen: J ⊨ u ≡ v Für x ∈ V ist γ(x) ∈ T (Σ, V)/_{↔_{E}^{∗}}, d.h. γ(x) = [s_{x}]_{↔_{E}^{∗}} für einen Term s_{x} Sei σ die Substitution {x/s_{x}|^{E} für alle x ∈ V, die in E auftreten} Dann gilt: J(x) = γ(x) = [s_{x}]_{↔_{E}^{∗}} = [xσ]_{↔_{E}^{∗}} (Beispiel: E_{plus} zu Zeigen: J ⊨ plus(O, x) ≡ Y. γ(y) = [s(O)]_{↔_{E}^{∗}} s_{y} = succ(O) σ = {y/succ(O), } J(y) = [yσ]_{↔_{E}^{∗}} = [succ(O)]_{↔_{E}^{∗}} J(t) = [tσ]_{↔_{E}^{∗}} J(plus(O, y)σ) = [plus(O, y)σ] = [plus(O, succ(O))]

Durch strukturelle Induktion zeigt man J(t) = [tσ]_{↔_{E}^{∗}} zu Zeigen war: J ⊨ u ≡ v, d.h. J(u) = J(v), d.h. [uσ]_{↔_{E}^{∗}} = [vσ]_{↔_{E}^{∗}} d.h. uσ ↔_{E}^{∗} vσ (Dies folgt aus u ↔_{E} v und Stabilität von ↔_{E}, Lemma 3.1.13) □ (endlich)

Korrektheit: Wenn wir eine Gleichung beweisen durch Herleitung (s ↔_{E}^{∗} t), dann ist sie wirklich wahr. Vollständigkeit: Auf diese Weise kann man jede wahre Gleichung beweisen. Vorteil: Man kann s ≡_{E} t ohne Rückgriff auf die Semantik systematisch / automatisch beweisen: s ↔_{E}^{∗} t ist semi-entscheidbar (d.h: es exisitert ein autmatisches Verfahren, dass s ↔_{E}^{∗} t beweisen kann, wenn es gilt. Wenn s ↮_{E}^{∗} t, dann terminiert das Verfahren eventuell nicht) Da ↔_{E}^{∗} = ≡_{E} ist auch das Wortproblem semi-entscheidbar. Arbeitsweise des Semi-Entscheidbaren-Verfahrens:

[figure: s; u; v; t]

Wurzel: mit s markiert Kinder: Terme u mit s ↔_{E} u Falls s ↔_{E}^{∗} t, dann tritt irgendwann t im Baum auf ↷ Abbruch mit Erfolg Sonst terminiert das Verfahren nicht.

Problem: Wenn t_{1} ≡ t_{2} ∈ E mit V(t_{1}) ≠ V(t_{1}), dann existieren unendlich viele u mit s ↔_{E} u Aber auch dann lässt sich jeder Knoten konstruieren ↷ bleibt semi-entscheidbar [14.05.04] Satz von Birkhoff: s ≡_{E} t gdw. s ↔_{E}^{∗} t Überprüfung von s ≡_{E} t durch s ↔_{E}^{∗} t: automatisierbar, aber:

• Semi-Entscheidungsverfahren: ungeeignet, falls s ≢_{E} t (Verfahren terminiert dann nicht)

• ineffizient (zuviel Wahlmöglichkeiten: welche Gleichung in welcher Richtung auf welchen Teilterm anwenden?)

Bsp: i(i(n)) ≡ n Suchbaum der Tiefe 3: > 20 Knoten Suchbaum der Tiefe 15: Falls jeder Knoten 3 Kinder hat: 3^{15} Knoten > 14 Millionen im folgenden: verbesserte Verfahren, die auf dem Satz von Birkhoff beruhen, aber zielgerichteter vorgehen. 3.2 Spezialfall: Keine Variablen ⇒ Kongruenzabschluss 3.3 Allgemeiner Fall (mit Variablen) ⇒ Termersetzung

3.2 Der Kongruenzabschluss bei Grundidentitäten

Spezialfall: E, s, t enthalten keine Variablen Anwendungen:

• Compilerbau: Optimierungen des zu compilierenden Programms

Bsp: common subexpression Problem

Mehrfach auftretende \underbrace{gleiche}_{müssen nicht syntaktisch gleich sein, sondern es reicht, wenn aus dem davorstehenden Programmcode folgt, das die Ausdrücke gleich sind} Teilausdrücke sollten nur einmal ausgewer-

tet werden

• Programmverifikation: Kongruenzabschluss lässt sich verwenden, um ein Entscheidungsverfahren für Allgemeingültigkeit universeller prädikantenlogischer Aussagen zu erhalten.

• Kombination von Entscheidungsverfahren

Definition 3.2.1: Grundidentität Eine Termgleichung s ≡ t ist eine Grundidentität, falls sie keine Variablen enthält, d.h. V(s) = V(t) = ∅

Beispiel 3.2.2: Variablen für Zahlen: i, j , k, l, m Variablen für Arrays: f, g

i = j;

k = l;

f[i] = g[k];

if j==f[j] then m=g[l]; . . ← (*) .

end if An der Stelle (*) tritt Ausdruck auf, der sowohl f[m] als auch g[k] enthält. gilt an der Stelle (*), dass f[m] = g[k]? Obige Frage lässt sich wie folgt umformulieren:

E = {i ≡ j, k ≡ l, f(i) ≡ g(k), j ≡ f(j), m ≡ g(l)} : Gilt: f(m) ≡_{E} g(k)

• Jetzt sind i, j, k, l, m Konstanten, keine Variablen. Sonst würde „i ≡ j“ bedeuten, das „∀i, j i ≡ j“, d.h. alle Terme wären “gleich“. ⇒ Sind wirklich Grundidentitäten.

• Ablesen der Gleichungen E aus dem Programm benötigt im Allgemeinen Programmanalyse aufgrund von Seiteneffekten

i = j E = {i ≡ j, j ≡ j + 1} ist falsch, beschreibt nicht den Zustand an Stelle (*)

j = j+1 Richtig wäre E = {i = j − 1} (*)

Wie untersucht man f(m) ≡_{E} g(k)?

1. Möglichkeit: Versuche, f(m) ↔_{E}^{∗} g(k)

• ineffizient, nicht tolerierbar, es existiert ein Entscheidungsverfahren mit polynomiellen Aufwand

• Semi-entscheidungsverfahren. Hier nicht tolerierbar, denn bei Grundidentitäten ist das Wortproblem entscheidbar!

Wesentliche Eigenschaften von ≡_{E}: stabil, monoton/kongruent, reflexiv, symmetrisch, transitiv

Äquivalenzrelation

Bei Grundidentitäten gibt es keine Variablen ↷ Stabilität uninteressant Idee: Starte mit den Gleichungen aus E und berechne alle Gleichungen, die aus E aufgrund der direkten Anwendung von Reflexivität, Symmetrie, Transitivität und Kongruenz folgen.

Definition 3.2.3: Direkte Anwendung von Reflexivität, Symmetrie, Transitivität, Kongruenz Für jede Menge E von Grundidentitäten definieren wir:

• R = {t ≡ t|t ∈ T (E)}

• S(E) = {t ≡ s|s ≡ t ∈ E}

• T (E) = {s ≡ v| es existiert ein t ∈ T (Σ) mit s ≡ t und t ≡ v ∈ E}

• C(E) = {f(s_{1}, …, s_{n}) ≡ f(t_{1}, …, t_{n})|f ∈ Σ, s_{i} ≡ t_{i} ∈ E für alle 1 ≤ i ≤ n}

Beispiel 3.2.4: Sei E wie in Beispiel 3.2.2, E = \underbrace{i, j, k, l, m}_{Σ_{0}}, \underbrace{f, g}_{Σ_{1}}:

R = {i ≡ i, j ≡ j, f(i) ≡ f(i), f(f(i)) ≡ f(f(i)), …} S = {j ≡ i, l ≡ k, g(k) ≡ f(i), f(j) ≡ j, g(l) ≡ m} T (E) = {i ≡ f(j)} C(E) = {f(i) ≡ f(j), g(i) ≡ g(j), …} (10 Gleichungen) In E ∪ R ∪ S(E) ∪ T (E) ∪ C(E) stehen nur Gleichungen, die aus E folgen. um s ≡_{E} t zu überprüfen, könnte man testen, ob s ≡ t ∈ E ∪R∪S(E)∪T (E)∪C(E). Aber aus s ≡ t ∉ \underbrace{E ∪ R ∪ S(E) ∪ T (E) ∪ C(E)}_{enthält nicht alle Gleichungen, die aus E folgen} folgt nicht s ≢_{E} t.

Problem: Symmetrie, Transitivität, Kongruenz müssten mehrfach angewendet werden.

Definition 3.2.5: Kongruenzabschluss Für eine Menge von Grundidentitäten E definieren wir die Mengen E_{0}, E_{1}, E_{2}, … wie folgt:

• E_{0} = E ∪ R

• E_{i+1} = E_{i} ∪ S(E_{i}) ∪ T (E_{i}) ∪ C(E_{i})

Der Kongruenzabschluss CC(E) (“congruence closure“) ist der “Limes“ der FOlge E_{0}, E_{1}, …, d.h. CC(E) = ∪_{i∈ℕ}E_{i}

Beispiel 3.2.6: Wir zeigen f(m) ≡ g(k) ∈ CC(E), denn f(m) ≡ g(k) ∈ E_{g}

\begin{matrix}oberste Zeile: Gleichungen aus E_{0} \\ nächste Zeile: Gleichungen aus E_{1} \\ letzte Zeile: Gleichungen aus E_{g} \end{matrix}\}

nur die Gleichungen aus E_{i} ausgeben, die für den Beweis von f(m) = g(k) wichtig sind

Satz 3.2.7: Kongruenzabschluss ist korrekt und vollständig Sei E eine Mengen von Grundindentitäten über Σ und sei s, t ∈ T (Σ). Dann gilt s ≡_{E} t, gdw. s ≡_{E} t ∈ CC(E)

Beweis: Korrektheit: s ≡ t ∈ \underbrace{CC(E)}_{E_{0}∪E_{1}∪...} ↷ s ≡_{E} t d.h. falls s ≡ t ∈ E_{i} ↷ s ≡_{E} t

Induktion über i Induktionsanfang i=0 E_{0} = E ∪ R, denn ≡_{E} ist reflexiv Induktionsschluss i ↷ i + 1 s ≡ t ∈ E_{i+1} = E_{i} ∪ S(E_{i}) ∪ T (E_{i}) ∪ C(E_{i}) Induktionshypothese: für alle u ≡ v ∈ E_{i} gilt: u ≡_{E} v. Damit folgt s ≡_{E} t, da ≡_{E} reflexiv, symmetrisch, transitiv, Kongruent (Lemma 3.1.10) Vollständigkeit s ≡_{E} t ↷ s ≡ t ∈ CC(E) Wir zeigen später (Satz 3.2.12) eine stärkere Aussage ↷ lasse Beweis hier weg □ Alternative Methode (statt s ↔_{E}^{∗} t) um Wortproblem bei Grundidentitäten zu lösen: Konstruiere E_{0}, E_{1}, … bis man ein E_{i} findet mit s ≡ t ∈ E_{i} ist immer noch ineffizient und Semi-Entscheidungsverfahren.

Um Entscheidungverfahren zu bekommen: stoppe Iteration E_{0}, E_{1}, … nach endlicher Zeit. Im Allgemeinen gilt: E_{i} ⊊ E_{i+1} für alle i: i ≡ j ∈ E_{0} g(i) ≡ g(j) ∈ E_{1}\E_{0} g(g(i)) ≡ g(g(j)) ∈ E_{2}\E_{1} Die meisten dieser Gleichungen sind für den Beweis einer vorgegebenen Gleichung s ≡ t unnötig! Erkenntnis: Man muss nur Gleichungen u ≡ v betrachten, bei denen u, v Teilterme aus E, s, t sind.

[18.05.04]

Ziel: s ≡_{E} t? Spezialfall: Keine Variablen Problem bei Kongruenzabschluss: Wenn s ≢_{E} t, dann terminiert das Verfahren im Allgemeinen nicht. Abhilfe: Konstruiere nicht mehr alle Terme in E_{i}.

Definition 3.2.8: Teiltermmenge Zu jedem Term s sei Subterms(s) = {s|_{π}|π ∈ Occ(s)} die Menge seiner Teilterme. Zu einer Menge von Gleichungen E sei Subterms(s) = ∪_{s≡t∈E}Subterms(s)∪ Subterms(t)

Wenn E endlich ist, ist auch Subterms(E) endlich. Bei der Bildung des Kongruenzabschlusses zum Nachweis von s ≡_{E} t muss man nur Gleichungen zwischen Termen aus S = Subterms(E) ∪ Subterms(s) ∪ Subterms(t) berücksichtigen.

Definition 3.2.9: Kongruenzabschluss bezüglich einer Menge von Termen Sei E eine Menge von Grundidentitäten, sein s, t, ∈ T (Σ). Sei S = Subterms(E)∪ Subterms(s) ∪ Subterms(t) Wir definieren: E_{0}^{S} = (E ∪ R) ∩ S × S ← Hier sehen wir die Gleichungen als Paare von Termen an (bedeutet E_{0}^{S} = {u ≡ v ∈ E ∪ R|u ∈ S, v ∈ S} E_{i+1}^{S} = (E_{i}^{S} ∪ S(E_{i}^{S}) ∪ T (E_{i}^{S}) ∪ C(E_{i}^{S})) ∩ S × S

(Wenn |S| = n, dann |E_{i}^{S}| ≤ n^{2}. Nach spätestens n^{2} Schritten stoppt die Iteration) Der Kongruenzabschluss bezüglich S ist CC^{S}(E) = ∪_{i∈ℕ}E_{i}^{S}

Beispiel 3.2.10: Kongruenzabschluss bezüglich S für E aus Beispiel 3.2.2 E_{0} = E ∪ {t ≡ t|t ∈ T (Σ)} E_{0}^{S} = E ∪ {t ≡ t|t ∈ S} (5 Gleichungen)

E_{1} = E_{0} ∪ \{j ≡ i, …, g(l) ≡ m\} ∪ \{i ≡ f(j)\} ∪ \underbrace{\{f(i) ≡ f(j), g(i) ≡ g(j), …\}}_{10 Gleichungen}

E_{i}^{S} = E_{0}^{S} ∪ \{j ≡ i, …, g(l) ≡ m\} ∪ \{i ≡ f(j)\} ∪ \underbrace{\{f(i) ≡ f(j), g(k) ≡ g(l)\}}_{2 Gleichungen}

Lemma 3.2.11: CC^{S}(E) wird nach endlich vielen Schritten erreicht Seien E, s, t wie in Definition 3.2.9, E endlich. Dann existiert ein i ∈ ℕ mit E_{i}^{S} = E_{i+1}^{S}. Daraus folgt: CC^{S}(E) = E_{i}^{S} Beweis: Für alle i ∈ ℕ: E_{i}^{S} ⊆ E_{i+1}^{S}. (|E_{i}^{S}| = n^{2} Wenn alle Gleichungen in E “gleich“ sind)! Da E_{i}^{S} ⊆ S × S und da S × S endlich ist, muss es ein i ∈ ℕ geben mit E_{i}^{S} = E_{i+1}^{S}. Dann gilt E_{i}^{S} = E_{j}^{S} für j ≥ i. Somit: CC^{S}(E) = ∪_{j∈ℕ}E_{j}^{S} = E_{i}^{S} □

Satz 3.2.12: Kongruenzabschluss bezüglich S ist korrekt und vollständig Sei E eine Menge von Grundidentitäten, s, t, ∈ T (Σ), Sei Subterms(E)∪Subterms(s)∪ Subterms(t) ⊆ S. Dann gilt: s ≡_{E} t gdw. s ≡_{E} t ∈ CC^{S}(E)

Beweis: Korrektheit: s ≡ t ∈ CC^{S}(E) ⊆ CC(E) ↷^{Satz 3.2.71} s ≡_{E} t Vollständigkeit: zu Zeigen: s ≡_{E} t ↷ s ≡ t ∈ CC^{S}(E) Satz von Birkhoff (Satz 3.1.14): s ≡_{E} t ↶ s ↔_{E}^{∗} t. Es reicht also zu Zeigen: s ↔_{E}^{∗} t ↷ s ≡ t ∈ CC^{S}(E) Vorraussetzung: s ↔_{E}^{n} t Induktion über n (Länge der Herleitung) Induktionsanfang: n = 0 ↷ s = t ↷ s ≡ t ∈ R ∩ (S × S) ⊆ E_{0}^{S} ⊆ CC^{S}(E). Induktionsschluss: n > 0 : s = s_{0} ↔_{E} s_{1} ↔_{E} … ↔_{E} s_{n} = t

Fall 1 Mindestens einmal wurde eine Gleichung aus E an der obersten Stelle E ausgewertet.

Es existiert k mit 1 ≤ k < n mit s_{k} = u, s_{k+1} = v und u ≡ v oder v ≡ u ∈ E.

s = s_{0} ↔_{E} … ↔_{E} s_{k} = u, v = s_{k+1} ↔_{E} … ↔_{E} s_{n} = t. Beide Herleitungen s ↔_{E}^{∗} u, v ↔_{E}^{∗} t sind kürzer als s ↔_{E}^{∗} t

Es gilt Subterms(u) ⊆ S, Subterms(v) ⊆ S, denn u ≡ v oder v ≡ u ∈ E

Induktionshypothese: s ≡ u ∈ CC^{S}(E), v ≡ t ∈ CC^{S}(E)

↷ es existiert i ∈ ℕ: s ≡ u ∈ E_{i}^{S}, v ≡ t ∈ E^{S}, u ≡ v ∈ E_{1}^{S} ⊆ E_{i}^{S}

↷ s ≡ v ∈ E_{i+1}^{S} ↷ s ≡ t ∈ E_{i+2}^{S} ⊆ CC^{S}(E)

Fall 2 In der Herleitung S ↔_{E}^{∗} t wurde nie eine Gleichung ganz aussen angewendet.

[Grafik] Seien π_{1}, …, π_{k} mit π_{i} ⊥ π_{j} für i ≠ j, die obersten Stellen in S, an denen in der Herleitung jemals Gleichungen angewendet werden.

↷ s|_{π_{i}} = p_{i}, p_{i} ↔_{E}^{∗} q_{i}, t = s[q_{1}]_{π_{1}} … [q_{k}]_{π_{k}}

Länge der Herleitung P_{i} ↔_{E}^{∗} q_{i} ist höchstens n. In jeder dieser Herleitungen wird aber mindestens einmal eine Gleichung aus E ganz aussen angewendet

↷^{Fall 1} p_{i} ≡ q_{i} ∈ CC^{S}(E)

Da CC^{S}(E) unter Kongruenz abgeschlossen ist (auf Termen von S) folgt auch s ≡ t ∈ CC^{S}(E)

1Korrektheit von CC(E)

□

Aus der Vollständigkeit von CC^{S}(E) folgt Vollständigkeit von CC(E) (Satz 3.2.7): s ≡_{E} t ↷ s ≡ t ∈ CC^{S}(E) ⊆ CC(E)

Beispiel 3.2.13: Im Beweis von f(m) ≡_{E} g(k) erkennt man: es traten nur Gleichungen aus S × S auf: f(m) ≡ g(k) ∈ E_{g}^{S}.

Korollar 3.2.14: Sei E eine endliche Menge von Grundidentitäten. Dann ist das Wortproblem (d.h.: „s ≡_{E} t“) entscheidbar.

Praktische Berechnung: Bilde nicht alle Gleichungen in E_{i}^{S}, sondern repräsentiere Äquivalenzklassen.

Definition 3.2.15: ↔_{E} als u ↔_{E} v gdw. u ≡ v ∈ E

Bilde reflexiv-symmetrisch-transitive Hülle von ↔_{E}: ↔_{E}^{∗}. S_{0} = {[s]_{↔_{E}^{∗}} |s ∈ S} Starte mit {{s, t}|s ≡ t ∈ E} ∪ {{s}|s ∈ S} und vereinige danach Mengen, die nicht disjunkt sind. Bilde zusätzlich f(s1, …, s_{n}), f(t_{1}, …, t_{n}) falls s, t zusammen in einer Äquivalenzklasse auftreten und f(s_{1}, …, s_{n}), f(t_{1}, …, t_{n}) ∈ E. Wende abwechselnd Kongruenz und Äquivalenz an. [21.05.04] Algorithmus für Kongruenzabschluss: Konstruiere nicht alle Gleichungen in CC^{S}(E), sondern konstruiere nur Äquivalenzklassen. s ↔_{E} t gdw. s ≡ t ∈ E

S_{0} = \{[S]_{↔_{E}^{∗}} |s ∈ S\}  E_{0}^{s′} = \{s ≡ t| es existiert M ∈ S_{0} mit s, t \underbrace{∈}_{d.h. s↔_{E}^{∗}t} M\}

S_{1} = \{[S]_{↔_{0}^{S′} ∪C(E_{0}^{S})′}|s ∈ S\} E_{1}^{s′} = \{s ≡ t| es existiert M ∈ S_{1} mit s, t \underbrace{∈}_{d.h. s↔_{E}^{∗}t} M\}

S_{2} = \{[S]_{↔_{0}^{S′} ∪C(E_{1}^{S})′}|s ∈ S\} E_{2}^{s′} = \{s ≡ t| es existiert M ∈ S_{2} mit s, t \underbrace{∈}_{d.h. s↔_{E}^{∗}t} M\}

Algorithmus: Kongruenzabschluss (E, s, t) Eingabe: endliche Menge von Grundidentitäten E, zwei Grundterme s, t Ausgabe: „True“, falls s ↔_{E}^{∗} t, sonst „False“

1. Sei S = Subterms(E) ∪ Subterms(s) ∪ Subterms(t)

2. Sei L = {{s, t}|s ≡ t ∈ E} ∪ {{s}|s ∈ S} „Äq“ 3. Vereinige alle Mengen M_{1}, M_{2} ∈ L mit M_{1}∩M_{2} ≠ ∅. (danach gilt: L = S_{0})

„Kon“ 4. Sei K = L∪{{f(s_{1}, …, s_{n}), f(t_{1}, …, t_{n})}|f ∈ Σ es existiert M_{i} ∈ L mit s_{i}, t_{i} ∈ M_{i}(für alle1 ≤ i ≤ n), f(s_{1}, …, s_{n}), f(t_{1}, .., t_{n}) ∈ S}

„Äq“ 5. Vereinige alle Mengen M_{1}, M_{2} ∈ K mit M_{1} ∩ M_{2} ≠ ∅.

6. Falls K ≠ L, dann setze L = K und gehe zu Schritt 4. (Hier gilt L = S_{i} im i-ten Schleifendurchlauf)

7. Falls es ein M ∈ L gibt mit s, t ∈ M, dann gib „True“ aus, sonst gib „False“ aus.

Kongruenzabschluss beruht auf der Idee, dass man zum Beweis von s ↔_{E}^{∗} t nur Teilterme von E, s, t betrachten muss. Stimmt nicht mehr, wenn Variablen auftreten: E = {f(f(x)) ≡ g(x)} Gilt f(g(a)) ≡_{E} g(f(a))? f(g(a)) ←_{E} f(f(f(a))) →_{E} g(f(a)) Herleitung gelingt nur, wenn zwischendurch Terme wie f^{3}(a) betrachtet werden, die keine Teilterme E, s, t sind.

3.3 Termersetzungssysteme

Satz von Birkhoff: Statt s ≡_{E} t kann man s ↔_{E}^{∗} t zeigen. Nachteile: ineffizient und falls s ≢_{E} t, dann terminiert das Verfahren nicht. Erhöhung der Effizienz: verringere Indeterminismen des obigen Verfahrens:

1. in welche Richtung soll eine Gleichung angewendet werden?

2. welche Gleichung soll auf welchen Teilterm angewendet werden?

3. wie lange sollte man Gleichungen anwenden?

Lösung von (1): Gleichungen nur noch von links nach rechts anwenden. Schreibweise für gerichtete Gleichung: ersetze „≡“ durch „→“. Eine gerichtete Gleichung nennt man Regel, eine Menge von gerichteten Gleichungen nennt man Termersetzungssystem

Definition 3.3.1: Termersetzungssystem Für l, r ∈ T (Σ, V) heisst l ← r Regel, falls

• V(r) ⊆ V(l)

• l ∉ V Eine Menge R von Regeln heisst Termersetzungssystem (TES, term rewriting system, TRS) Für ein TES R ist Ersetzungsrelation →_{R}⊆ T (Σ, V) × T (Σ, V) definiert als s →_{R} t gdw. s|_{p}i = lσ und t = s[rσ]_{π} für π ∈ Occ(s), l → r ∈ R, σ ∈ SUB(Σ, V). Man nennt s →_{R} t „Termersetzungsschritt“, bei dem s an der Stelle π reduziert wird. Ein Teilterm s|_{π}, auf den die linke Seite einer Regel matcht, heisst Redex („Reducible expression“) Schreibe auch „s → t“ statt „s →_{R} t“, wenn R klar ist. Schreibe auch „t ← s“ statt „s →_{R} t“, wenn R klar ist.

Grund für V(r) ⊆ V(l): Für jeden Term s existieren nur endlich viele \underbrace{t}_{Wie bei Gleichungssystemen beschränken wir uns auf endliche TESe.} mit

s →_{R} t sonst: e → f(x, i(x)) ∈ R:

\xymatrix{e \ar[r] \ar[dr] \ar[ddr] & f(x, i(x)) ∈ R \\  & f(i(x), i^{2}(x)) ∈ R \\  & f(i^{2}(x), i^{3}(x)) ∈ R}

V(r) ⊆ V(l) garantiert, dass der Matcher σ eindeutig festliegt, wenn s|_{π} = lσ. Hierdurch liegt dann auch rσ fest. Weiterer Grund: sonst würde Anwendung von Regeln nie terminieren Grund für l ∉ V: Reduziere Indeterminismen (x → t wäre immer / auf jeden Term anwendbar) und Terminierung

Beispiel 3.3.2: Ziel: Löse Wortproblem für Gleichungssystem E Vorgehen: Überführe E in ein TES R plus(O, y) ≡ y plus(O, y) → y (Richtung y → plus(O, y) verletzt Variablen-bedingung) plus(succ(x), y) ≡ succ(plus(x, y)) plus(succ(x), y) → succ(plus(x, y)) (Andere Richtung wäre auch möglich) Um von E zu R zu kommen, ist es nicht immer ratsam, eine Gleichung s ≡ t durch s → t oder t → s zu ersetzen. Grund: Um Indeterminismen (2) und (3) zu lösen, möchte man TESe R konstruieren, bei denen →_{R}-Anwendung terminiert und eindeutige Ergebnisse liefert.

Damit sich E und R „entsprechen“, müssen sie „äquivalent“ sein:

Definition 3.3.3: Äquivalenz von Gleichungssystem und TES Sei E ein Gleichungssystem, sei R ein TES über Σ und V. Dann ist R äquivalent zu E gdw. ↔_{R}^{∗}=↔_{E}^{∗} Falls E und R äquivalent sind, dann s ≡_{E} t \underbrace{gdw.}_{Birkhoff} s ↔_{E}^{∗} t \underbrace{gdw.}_{Äquivalenz} s ↔_{R}^{∗} t.

Also: Durch Anwendung von Regeln aus R (in beide Richtungen) kann man genau alle wahren Aussagen beweisen. Wenn R und E gegeben, wie kann man überprüfen, ob sie äquivalent sind?

Satz 3.3.4: Zusammenhang zwischen Gleichungssystem und TES Sei E ein Gleichungssystem, Sei R ein TES über Σ, V. R ist äquivalent zu E gdw.

• l ↔_{E}^{∗} r für alle Regeln l → r ∈ R („R ist korrekt für E“)

• s ↔_{R}^{∗} t für alle Gleichungen s ≡ t ∈ E („R ist adäquat für E“)

Beweis: Übung. (Äquivalenz ↷ Korrektheit und Adäquanz (trivial). „↶“ folgt aus Monotonie und Stabilität von ↔_{E}^{∗}, ↔_{R}^{∗} Induktion über die Anzahl der Herleitungsschritte). □

Falls R aus E entsteht, indem „s ≡ t“ durch „s → t“, oder „t → s“ ersetzt wird, so sind R und E trivialerweise äquivalent.

Beispiel 3.3.5: E = {b ≡ c, b ≡ a, f(a) ≡ f(f(a))} R = {c → b, a → b, f(f(b)) → f(b)}

R ist korrekt für E :c ←_{E} b
a ←_{E} b
f(f(b)) →_{E} (f(f(a))) ←_{E} f(a) ←_{E} f(b)
R ist adäquat für E :b ←_{R} c
b ←_{R} a
f(a) →_{R} (f(b)) ←_{R} f(f(b)) ←_{R} f(f(a))

R′ = {c → a, f(f(b)) → f(b)} korrekt, aber nicht adäquat ↷ nicht äquivalent

[25.05.04] Wortproblem: s ≡_{E} t Vorgehen: Suche TES R, das zu E äquivalent ist Birkhoff: s ≡_{E} t gdw. s ↔_{E}^{∗} t gdw. s ↔_{R}^{∗} t Um TESe effizient und als Entscheidungsverfahren anwenden zu köennen, wollen wir wie folgt vorgehen, um s ≡_{E} t zu überprüfen.

• Werte s und t solange wie möglich aus, d.h. wende TES-Regeln von links nach rechts an solange möglich.

s →_{R} s_{1} →_{R} s_{2} →_{R} … →_{R} s_{n}

t →_{R} t_{1} →_{R} … →_{R} t_{n}

• Überprüfe, ob s_{n} und t_{n} syntaktisch gleich sind. Wenn ja, gib „True“ aus, wenn nein, gib „False“ aus.

Beispiel 3.3.6: E = plus-Gleichungen, R = TES auf Folie (äquivalent zu E) untersuche: plus(succ(succ(O)), x) ≡_{E} plus(succ(O), succ(x)) ? plus(succ(succ(O)), x) →_{R} succ(plus(succ(O), x)) →_{R} succ(succ(plus(O, x))) →_{R} succ(succ(x)) plus(succ(O), succ(x)) →_{R} succ(plus(O, succ(x))) →_{R} succ(succ(x)) Sind syntaktisch gleich ↷ Gleichung folgt aus E s ≡ t plus(succ(O), succ(x)) →_{R} succ(plus(O, succ(x))) →_{R} succ(succ(x))

Probleme bei diesem Verfahren:

1. Mann kann s und t nicht zu s_{n}, t_{n} reduzieren, die selbst nicht mehr reduzierbar sind

2. s und t könnten zwar endliche Reduktionen, aber auch unendliche Reduktionen haben. Wie findet man die endlichen Reduktionen?

⇒ Einschränkung auf terminierende TESe, d.h. jede Reduktion … →_{R} … →_{R} … ist endlich.

Beispiel 3.3.7: E = {b ≡ c; b ≡ a, f(a) ≡ f(f(a))} R_{1} = {b → c, b → a, f(a) → f(f(a))} Untersuche f(a) ≡_{E} f(c)? f(a) →_{R_{1}} f(f(a)) →_{R_{1}} f^{3}(a) →_{R_{1}} f^{4}(a) →_{R_{1}} …f(a) hat nur unendliche Auswertungen (1) Definieren uns neues TES: R_{2} = {b → c, b → a, f(a) → f(f(b))} Untersuche f(a) ≡_{E} f(c)?

\xymatrix{f(a) \ar[r] & f(f(b)) \ar[r] \ar[dr] & f(f(c)) &  & f^{3}(c) \\  &  & f(f(a)) \ar[r] & f^{3}(b) \ar@{-->}[ur] \ar[r] & f^{3}(a) \ar[r] & ….}

f(a) hat sowohl endliche als auch unendliche Auswertungen (2).

Probleme: (3) Ziel: s ↔_{R}^{∗} t zeigen. Wir wollen aber nur untersuchen, ob es einen Term q mit s →_{R}^{∗} q ←_{R}^{∗} t. Es könnte sein, das man zum Nachweis von s ↔_{E}^{∗} t die Richtung der Regelanwendung mehrmals ändern muss.

(4) Es könnte sein, das man bei geeigneter Regelanwendung s →^{∗} q ←^{∗} t zeigen könnte, bei ungeeigneter Regelanwendung aber nicht. (Probleme (3) + (4): betreffen Eindeutigkeit) ⇒ Einschränkung auf konfluente TESe, d.h. jede maximale Reduktion liefert das gleiche Ergebnis.

Beispiel 3.3.7: (Fortsetzung)

R_{3} = {b → c, b → a, f(f(a)) → f(a)} terminiert Untersuche f(a) ≡_{E} f(c)? Weder f(a) noch f(c) lassen sich reduzieren ↷ „False“ Aber: f(a) ←_{R} f(b) →_{R} f(c)

Untersuche f(f(b)) ≡_{E} f(a) mit R_{3}: f(a) nicht weiter reduzierbar

\xymatrix{f(f(b)) \ar[r] \ar[dr] & f(f(c)) & „False“ \\  & f(f(a)) \ar[r] & f(a) & „True“ & (4)}

In diesem Beispiel: keines der TESe, die aus E entstehen, in dem man s ≡ t durch s → t oder t → s ersetzt, ist sowohl terminierend als auch konfluent. ein äquivalentes TES, das terminiert und konfluent ist, ist: R = {c → b, a → b, f(f(b)) → f(b)} ⇒ Es kann sinnvoll sein, zu einem Gleichungssystem E ein äquivalentes TES R zu konstruieren, das nicht aus Gleichungen durch Ersetzung von „≡“ durch „→“ oder „←“ entsteht, denn dann ist R eventuell nicht terminierend bzw. nicht konfluent. Fragen:

• Wie zeigt man die Terminierung eines TES? ← Terminierung von Programmen (Kapitel 4)

• Wie zeigt man die Konfluenz eines TES? ← Eindeutigkeit von Programmen (Kapitel 5)

• Wie bekommt man zu einem Gleichungssytsem E ein dazu äquivalentes TES Wie zeigt man die Terminierung eines TES R, das terminiert und konfluent ist? ← Vervollständigung von Programmen (Kapitel 6)

Vorher: Definiere „Terminierung“, „Konfluenz“ etc. TES R terminiert gdw. es keine unendlichen Reduktionen … →_{R} … →_{R} … →_{R} … →_{R} … gibt

Definition 3.3.8: Fundierte Relation Sei → eine Relation über einer Menge M. Die Relation ist fundiert (well-founded) gdw. es keine unendliche Folge t_{0}, t_{1}, … ∈ M gibt mit t_{0} → t_{1} → t_{2} → t_{3} → …

Beispiel 3.3.9:

• Die Relation >_{ℕ} ist fundiert (10 > 7 > 3 > 1 > 0)

• Die echte Teiltermrelation ▷ auf T (Σ, V) ist fundiert

(f(g(x), h(x)) ▷ g(x) ▷ x)

• Die Relation <_{ℕ} ist nicht fundiert (0 < 1 < 2 < 3 …)

• Die Relation >_{ℤ} ist nicht fundiert (2 > 1 > 0 > −1 > −2 > …)

• Die Relation >_{ℚ^{+}} ist nicht fundiert (1 > \frac{1}{2} > \frac{1}{3} > \frac{1}{4} > …)

• Die Relation >_{ℕ^{∗}} (π_{1} >_{ℕ^{∗}} π_{2} gdw. π_{1} = π_{2} π für ein π ≠ E) ist fundiert 31240 >_{ℕ^{∗}} 312 >_{ℕ^{∗}} 3 >_{ℕ^{∗}} E |π_{1}| >_{ℕ} |π_{2}|

Unser Ziel ist also, TESe R zu verwenden, bei denen →_{R} fundiert ist t →_{R} … →_{R} q und q ist nicht reduzierbar.

Definition 3.3.10: Normalform Sei → eine Relation über Menge M. Ein Objekt q ∈ M heisst Normalform gdw. es kein Objekt q′ ∈ M gibt mit q → q′. Ein Objekt heisst Normalform eines Objektes t gdw t →^{∗} q und q Normalform ist. Falls die Normalform eindeutig ist, so bezeichnet t ↓ die Normalform von t. Die Relation → ist normalisierend, wenn es zu jedem Objekt t mindestens eine Normalform g gibt. Die Relation → ist eindeutig normalisierend, wenn es zu jedem Objekt t genau eine Normalform g gibt.

\xymatrix{fundiert \ar[dr] &  & eindeutig normalisierend \ar[dl] \\  & normalisierend}

Lemma 3.3.11: Jede fundierte Relation ist normalisierend. Beweis: Annahme: es existiert t ∈ M ohne Normalform. t → t_{1} → t_{2} → t_{3} → … ⚡ zur Fundiertheit □

Definition 3.3.12: Terminierung von TESen Ein TES R terminiert gdw. →_{R} fundiert ist. Ein TES R ist normalisierend gdw. →_{R} normalisierend ist. (d.h. jeder Term hat mindestens eine Normalform) Analog „eindeutig Normalisierend“.

Beispiel 3.3.13:

a) R = {b → a, b → f(b)}

\xymatrix{b \ar[r] \ar[d] & f(b) \ar[r] \ar[d] & f(f(b)) \ar[r] \ar[d] & f^{3}(b) & … \\ a & f(a) & f^{2}(a)}

[28.05.04] nicht terminierend, normalisierend, nicht eindeutig normalisierend

b) R = {b → a, b → b}

nicht terminierend. (b → b → b → b...) eindeutig normalisierend

c) R = {b → c, b → a}

terminiert. nicht endlich normalisierend.

d) R = {c → b, a → b}

terminiert, eindeutig normalisierend

• fundiert/terminiert

• normalisierend (folgt aus Fundiertheit/Terminierung oder eindeutiger Normalisierung)

• eindeutig normalisierend

Einige Einschänkungen an die Gestalt von Regeln sind für Terminierung nötig:

• V(r) ⊆ V(l) für alle Regeln l → r:

Bsp: a → f(x) a → f(a) → f(f(a)) → f^{3}(a) → …

Allgemein: Falls x ∈ V(x)\V(l) : σ = {x/l} r|_{π} = x

l → rσ = rσ[l]_{π} → rσ[rσ]_{π} = rσ[rσ[l]_{π}]_{π} → …

• l ∉ V für alle Regeln l → r:

Bsp: x → f(x): x → f(x) → f^{2}(x) → f^{3}(x) → …

Allgemein: Falls es Regel x → r gibt, gilt: σ_{1} = {x/r}, σ_{2} = {x/rσ_{1}}, σ_{3} = {x/rσ_{2}}, …

x → r → rσ_{1} → rσ_{2} → rσ_{3} → ...

Terminierung alleine reicht nicht aus, um das gewünschte Verfahren für das Wortproblem verwenden zu können: R = {b → c, b → a} terminiert. Um zu beweisen, dass a ≡_{E} c gilt: a und c sind schon Normalformen ↷ „False“ Aber: a ≡_{E} c gilt, denn a ↔_{R}^{∗} c: a ←_{R} b →_{R} c Wir wollen aber nicht „s ↔_{R}^{∗} t“ untersuchen, sondern wir untersuchen nur, ob s und t zusammenführbar sind, d.h., ob es einen Term q gibt mit: „s ←_{R}^{∗} q →_{R}^{∗} t“ Im allgemeinen ist das eine deutliche Einschränkung ↷ Betrachte nur noch solche TESe, wo „s ↔_{R}^{∗} t“ und Zusammführbarkeit dasselbe sind.

Definition 3.3.14: Zusammenführbarkeit, Church-Rosser-Eigenschaft Sei → eine Relation auf Menge M. Zwei Elemente s, t ∈ M sind zusammenführbar (joinable, schreibweise s ↓ t) gdw. es ein q ∈ M gibt mit s →^{∗} q ←^{∗} t. Die Relation hat die Church-Rosser-Eigenschaft gdw. für alle s, t ∈ M gilt: wenn s ↔^{∗} t, dann s ↓ t.

Ein TES R hat die Church-Rosser-Eigenschaft gdw. →_{R} die Church-Rosser-Eigenschaft hat.

(Church und Rosser haben die Church-Rosser-Eigenschaft des Lambda-Kalküls 1936 gezeigt)

Beispiel 3.3.15:

• {b → c, b → a} hat die Church-Rosser-Eigenschaft nicht: a ↔_{R}^{∗} c, aber a ↓̸_{R} c

• plus-TES hat die Church-Rosser-Eigenschaft:

plus(succ(succ(O)), x) ↔_{R}^{∗} plus(succ(O)succ(x)) und

\xymatrix{plus(succ(succ(O)), x) \ar[dr] & & plus(succ(O), succ(x)) \ar[dl] \\ & succ(succ(x))}↷↓

Um die Church-Rosser-Eigenschaft zu überprüfen, müsste man unendlich viele Termpaare s, t untersuchen. Besser für die (automatische) Überprüfung geeignet: Konfluenz. Konfluenz: Wenn ein Indeterminismus auftritt:

\xymatrix{ & P \ar[dl]_{∗} \ar[dr]^{∗} \\ s \ar@{.>}[dr]_{+} & & t \ar@{.>}[dl]^{∗} \\ & q}

→ Wenn diese Pfeile existieren, dann auch die −−→

dann ist es egal, für welche welche Alternative man sich entscheidet.

Definition 3.3.16: Konfluenz Eine Relation → über der Menge M heisst Konfluent gdw. für alle p, s, t ∈ M gilt: Wenn p →^{∗} s und p →^{∗} t, \underbrace{dann existiert ein q ∈ M mit s →^{∗} q und t →^{∗} q}_{d.h.s↓t.}

Ein TES R heisst konfluent gdw. →_{R} konfluent ist.

Satz 3.3.17: Church-Rosser gdw. Konfluent Für alle Relationen → gilt: → hat die Church-Rosser-Eigenschaft gdw. → konfluent ist. Beweis: „Church-Rosser ↷ Konfluenz“: → habe die Church-Rosser-Eigenschaft. zu Zeigen:

\xymatrix{ & P \ar[dl] \ar[dr] \\ s &  & t}  ↷ s ↓ t

Es gilt:

\xymatrix{ & P \ar[dl] \ar[dr] \\ s &  & t}  ↷ s ↔^{∗} t ↷^{CR} s ↓ t

„Konfluenz ↷ Church-Rosser“: Sei → Konfluent. z.Z.: \underbrace{s ↔^{∗} t}_{s↔^{n}t(n∈ℕ)} ↷ s ↓ t. Induktion über n (über die Länge von s ↔ … ↔ t).

Induktionsanfang: n = 0 s = t ↷ s ↓ t√ Induktionsschluss: n > 0:

[figure: s; n−1; I.H.; ∗; s′; ∗; t; q]

Fall 1  [figure: s; n−1; ∗; s′; ∗; t; q]  ↷ s ↓ t

Fall 2

[figure: s; n−1; ∗; s′; ∗; t; q; p]

← wegen der Konfluenz, da q und t einen gemeinsamen Vorgänger s’ haben ↷ s ↓ t

Bsp: {b → c, b → a} Problem liegt im Endeffekt daran, dass ein Term (b) 2 Normalformen hat.

Konfluenz garantiert, dass es höchstens eine Normalform gibt. ↷ Konfluenz generell wichtig bei Programmen, da unabhängig von der verwendeten Auswertungsstrategie das Resultat eines Programms eindeutig sein sollte. (→ vergleiche Diskussionen über „call-by-value“ und „call-by-name“)

Lemma 3.3.18: Konfluenz bedeutet eindeutige Normalformen

a) Wenn eine Relation ↷ konfluent ist, dann hat jedes Objekt höchstens eine Normalform.

b) Wenn eine Relation ↷ konfluent und normalisierend ist, dann hat jedes Objekt genau eine Normalform. (d.h. → ist eindeutig normalisierend)

c) Jede eindeutig normalisierende Relation ist konfluent.

Beweis:

a) Annahme: Es existiert ein Objekt t mit 2 verschiedenen Normalformen q_{1} und q_{2}

\xymatrix{ & t \ar[dl] \ar[dr] \\ q_{1} \ar@{.>}[dr] &  & q_{2} \ar@{.>}[dl] \\  & p}

Da q_{1} ud q_{2} Normalformen sind, gilt q_{1} = p = q_{2} ⚡

b) Konfluenz ↷ höchstens eine NF (a) √

Normalisierend ↷ mindestens eine NF √

c) Sei → eindeutig normalisierend, z.z: → ist konfluent.

\xymatrix{ & p \ar[dl]_{∗} \ar[dr]^{∗} \\ s \ar@{.>}[d] &  & t \ar@{.>}[d]^{∗} \\ s ↓ &  & t ↓}

s ↓ und t ↓ existieren, beide sind Normalformen von P. Wegen eindeutig normalisierend: s ↓= t ↓ Satz 3.3.19: Überführbarkeit und Zusammenführbarkeit Sei → eine normalisierende konfluente Relation über M, seien s, t ∈ M Dann gilt: s ↔^{∗} t gdw. s ↓= t ↓ Beweis: „↶“: s ↓= t ↓↷ s ↓ t ↷ s ↔^{∗} t√

„↷“: s ↔^{∗} t ↷^{Satz 3.3.17^{1}}

s ↓ t, d.h. es existiert q mit

\xymatrix{s \ar[dr]_{∗} &  & t \ar[dl]^{∗} \\  & q \ar@{.>}[d]_{∗} &  & existiert, weil → normalisierend ist \ar[ll] \\  & q ↓}

↷ wegen der Eindeutigkeit der Normalformen. s ↓ q ↓= t ↓ (Lemma 3.3.18)

□ [08.06.04]

Ziel: s ≡_{E} t, s, t, E dürfen Variablen enthalten ↷ TES Eigenschaften:

• Terminierung

↓

• Normalisierung (jeder Term hat mindestens eine Normalform)

• CR-Eigenschaft

↕ ( ↷ jeder Term hat höchstens eine Normalform)

• Konfluenz

Eigentlich müssten wir s ↔_{R}^{∗} t untersuchen. Wenn R normalisierend und Konfluent ist, dann reicht es, stattdessen s ↓_{R}= t ↓_{R} zu untersuchen. Normalisierung alleine hat den Nachteil, dass man s ↓_{R} eventuell nicht berechnen kann, da s auch unendliche Reduktionen haben kann. Deshalb: Einschränkung auf terminierende und konfluente TESe

Definition 3.3.20: Ein TES ist konvergent, gdw. es terminiert und konfluent ist.

Beispiel 3.3.21: plusTES ist konvergent Bei konvergenten TESen kann man das Berechnen von Normalformen als “Interpreter“ des TES-Programms ansehen.

0Konfluenz äquivalent zur CR-Eigenschaft

↷ konvergente TESe können zum „Rechnen“ benutzt werden. Beispiel 2+1: Rufe „plus“ mit der „rechnerinternen“ Darstellung“ von 2 und 1 auf: plus(s(s(O)),s(O)) Anwenden des Interpreters “↓_{R} “ : plus(s(s(O)), s(O)) ↓_{R}= \underbrace{s(s(s(O)))}_{rechnerinterne Darstellung von 3}

Wir wollen konvergente TESe nicht nur zum Rechnen, sondern zum Beweisen benutzen. ↷ Algorithmus WORTPROBLEM

Satz 3.3.22:

a) Der Algorithmus WORTPROBLEM terminiert

b) Falls R äquivalent zum Gleichungssystem E ist, dann ist das Algorithmus WORTPROBLEM korrekt

c) Existiert zu einem Gleichungssystem ein äquivalentes konvergentes TES, so ist das Wortproblem über diesem Gleichungsystem entscheidbar

Beweis:

a) folgt aus der Terminierung von R, da jede Reduktionsfolge endlich ist

b) s ≡_{E} \underbrace{gdw}_{Satz von Birkhoff 3.1.14} s ↔_{E}^{∗} t \underbrace{gdw.}_{Äquivalenz von E und R} s ↔_{R}^{∗} t \underbrace{gdw.}_{Satz 3.3.19Rnormalisierend und konfluent} s ↓_{R}=

t ↓_{R}

c) WORTPROBLEM ist ein Entscheidungsverfahren (alle Schritte des Algorithmus sind effektiv durchführbar)

Um s zu reduzieren, muss man alle (endlich vielen) Teilterme von s und alle (endlich vielen) linken Regelseiten untersuchen und überprüfen, ob die linke Regelseite den Teilterm matcht. Matching kann automatisch durchgeführt werden ↷ Kapitel 5

□

Wortproblem ist im Allgemeinen unentscheidbar:

• es existieren Gleichungssysteme E, zu denen kein äquivalentes, konvergentes TES existiert

• selbst wenn es ein äquivalentes, konvergentes TES gibt, so findet man dieses nicht unbedingt ↷ im Folgenden: Wie findet man zu E ain äquivalentes, konvergentes TES?

Beispiel 3.3.23: Gruppenbeispiel. Wie erhält man ein äquivalentes, konvergentes TES f(x, f(y, z)) → f(f(x, y), z) f(x, e) → x f(x, i(x)) → e ist äquivalent, terminiert, aber ist nicht konfluent.

\xymatrix{ & f(x, f(y, i(y))) \ar[dl]_{(1)} \ar[dr]^{(3)} \\ f(f(x, y), i(y)) \ar[d] &  & f(x, e) \ar[d] \\ 2 verschiedene Normalformen &  & x \ar[ll]}

Wenn man Wortproblem benutzt, um mit diesem TES i(i(n)) ≡_{E} n zu untersuchen, so ergibt sich „ False“ (beide sind Normalformen). Lösung, um ein konvergentes TES zu erhalten: Starte mit (1), (2), (3) und vervollständige TES um zusätzliche Regeln l → r.

• Äquivalenz muss erhalten bleiben (d.h. es muss l ≡_{E} r gelten)

• Terminierung muss erhalten bleiben

• Füge solange neue Regeln hinzu, bis das TES konfluent ist.

Im Beispiel: es existiert ein 10-Regel TES, das zu E äquivalent und konvergent ist. ↷ Automatischer Beweis, der alle Aussagen über Gruppen entscheiden kann. Es gilt:

\xymatrix{i(i(n)) \ar[dr]^{∗} &  & n \ar[dl] \\  & n^{∗}}

Ziel jetzt: Generiere zu einer Gleichungsmenge automatisch ein äquivalentes, konvergentes TES. (Erzeuge automatisch einen automatischen Beweiser, der Aussagen über der Gleichungsmenge entscheidet) Vorgehen, um zu E ein äquivalentes, konvergentes TES zu konstruieren:

1. Konstruiere ein äquivalentes TES, z.B. durch Richten von Gleichungen

2. Überprüfe, ob R terminiert. Wenn nein, gib auf (oder richte Gleichungen anders)

3. Überprüfe, ob R konfluent ist. Falls ja: konvergentes äquivalentes TES. Ende mit Erfolg.

4. Falls nein, vervollständige R um zusätzliche Regeln l → r wobei l ≡_{E} r. Zuück zu Schritt 2.

3 Möglichkeiten:

3.3. TERMERSETZUNGSSYSTEME 41

• nach endlich vielen Schritten erhält man äquivalentes konvergentes TES • Scheitern aufgrund fehlgeschlagenen Terminierungsbeweis (→ scheitern

wird bemerkt, wiederholter Versuch mit anderer Technik für Terminierungsbeweise möglich)

• Verfahren terminiert nicht (Vervollständigung mit unendlich vielen Re-

geln, scheitern wird nicht bemerkt) Folgende Fragen sind zu lösen:

• Wie kann man zu einem TES herausfinden, ob es terminiert? (Kapitel 4, unentscheidbar)

• Wie kann man zu einem TES herausfinden, ob es konfluent ist? (Kapitel 5, entscheidbar bei terminierenden TESen)

• Wie kann man ein TES vervollständigen? (Kapitel 6)

42KAPITEL 3. TERMERSETZUNG UND DEDUKTION VON GLEICHUNGEN

Terminierung von Termersetzungssystemen

Warum interessant?

1. Nötig, um Wortproblem zu lösen (d.h., um zu einer Gleichungsmenge ein konvergentes, äquivalentes TES zu konstruieren)

2. Nötig, um Konfluenz zu entscheiden (ohne Terminierung ist konfluenz unentscheidbar)

3. Generelle essentielle Eigenschaft korrekter Programme (Terminierungsanalyse grundlegend in Software-Verifikation)

4. Nachweis anderer Programm-Eigenschaften benötigt Induktion. Hierfür braucht man Terminierung des Programmes.

Vorgehen: 4.1 Zusammenhang Terminierung/ Induktion 4.2 Entscheidbarkeitsresultate zur Terminierung (und Verfahren zum automatischen Terminierungsnachweis bei TESen ohne Variablen auf rechten Seiten) 4.3 Ansatz für automatische Terminierungsbeweise 4.4 Automatische Erzeugung von Reduktionsrelationen

4.1 Noethersche Induktion

Bisher: Induktionsbeweise anhand von Datenstrukturen. Schreibweise: ∀, ⇒ auf der Meta-Ebene Natürliche Zahlen (Peano-Induktion): Induktionsanfang φ(0) Induktionsschluss: ∀y ∈ ℕ φ(y) ⇒ φ(y + 1) Jetzt: ein allgemeineres Induktionsprinzip, so dass alle bisherigen Induktionsprinzipien Spezialfälle davon sind. [11.06.04] Induktion:

44 KAPITEL 4. TERMINIERUNG VON TERMERSETZUNGSSYSTEMEN

• über beliebige Mengen M (ℕ, T (Σ, V), ℕ^{∗}, …)

• beliebige Induktionsrelationen ≻ (Idee der Induktion: wenn man im Induktionsschritt die Aussage für m ∈ ℕ zeigen will, dann darf man sie für alle bezüglich ≻ kleineren Objekte vorraussetzen)

• Peano-Induktion: m ≻ k gdw. m = k + 1 (m, k ∈ ℕ)

• Strukturelle Induktion über Terme: s ≻ t gdw. t ist direkter Teilterm von s (s, t, ∈ T (Σ, V))

Induktionsrelation darf nicht ganz beliebig sein: Bsp: Induktion auf ℕ, m ≻ k gdw. m=k Zeige: ∀x ∈ ℕ: x = 0 Induktionsschritt: ∀m ∈ ℕ, m = 0, Induktionshypothese: k = 0, für alle k mit m ≻ k d.h. ∀m m = 0 ⇒ m = 0√ Bedingung: ≻ muss fundiert sein! (d.h. keine ∞ Folgen m_{0} ≻ m_{1} ≻ m_{2} ≻ …)

Definition 4.1.1: Noethersches Induktionsprinzip Sei ≻ eine fundierte Relation über einer Menge M. Sei φ(m) eine Aussage über Objekte m ∈ M. Falls für alle m ∈ M gilt: Wenn φ(k) für alle k ∈ M mit m ≻ k gilt, dann gilt auch φ(m). Dann gilt φ(m) für alle n ∈ M.

D.h.: (∀m ∈ M : \underbrace{(\underbrace{∀k ∈ M.m ≻ k ⇒ φ(k)}_{Induktionshypothese}) ⇒ \underbrace{φ(m)}_{Induktionskonklusion})}_{(∗)} ⇒ ∀n ∈ M.

φ(n) (“⇒“ gilt auch) In der noetherschen Induktion gibt es keinen Induktionsanfang und Induktionsschluss. Beweisstechnisch ist es oft vorteilhaft, beim Beweis der noetherschen Induktionsformel (*), die Fälle mit m ∈ M, zu dene es kein k mit m ≻ k gibt, getrennt zu betrachten. (Diese Fälle entsprechen dem Induktionsanfang)

Satz 4.1.2: Das noethersche Induktionsprinzip ist korrekt Beweis: Annahme: Noethersche Induktionsformel (*) gilt, aber es existiert ein Gegenbeispiel n_{0} ∈ M, so dass φ(n_{0}) nicht gilt. Wegen (*): φ(n_{0}) wäre wahr, wenn φ(m) für alle n_{0} ≻ k gelten würde. ↷ es existiert also ein kleineres Gegebeispiel als n_{0}, d.h. ein n_{1} mit n_{0} ≻ n_{1} und φ(n_{1}) gilt nicht. Wegen (*): φ(n_{1}) wäre wahr, wenn φ(m) für alle n_{1} ≻ k gelten würde. ↷ es existiert also ein kleineres Gegenbeispiel als n_{1}, d.h. ein n_{2} mit n_{0} ≻ n_{1} ≻ n_{2} und φ(n_{2}) gilt nicht. … ⇒ es existiert eine unendliche absteigende Folge n_{0} ≻ n_{1} ≻ n_{2} ≻ … von Gegenbeispielen (φ(n_{i}) gilt nicht für alle i) ⚡ zur Fundiertheit. □ Satz 4.1.3: Lemma von König Anwendungsbeispiel für noethersche Induktion, wird später benötigt Ein Baum mit endlichem Verzweigungsgrad (d.h. jeder Knoten hat nur endlich viele Kinder), in dem jeder Pfad endlich ist, besitzt nur endlich viele Knoten. Beweis: Sei B ein Baum wie oben. Sei M die Menge aller Knoten des Baums. Zu m ∈ M sei B_{m} der Teilbaum, der vom Knoten m aufgespannt wird. Sein ≻ eine Relation auf Knoten, wobei m ≻ k gdw. k (direktes) Kind von m ist. ≻ ist fundiert, weil jeder Pfad endlich ist. Wir zeigen die folgende Aussage φ(n) für alle Knoten n ∈ M: φ(n): Der von n aufgespannte Teilbaum B_{n} hat nur endlich viele Knoten. Da φ(n) auch für die Wurzel n gilt, folgt daraus der Satz. Beweis mit noetherscher Induktion: Für alle m ∈ M: Wenn φ(k) für alle m ≻ k gilt, dann gilt φ(m). D.h.: Für alle Knoten m: Wenn \underbrace{|B_{k}|}_{Anzahl Knoten inB_{k}} endlich ist

für alle direkten Kinder k von M, dann ist auch \underbrace{|B_{m}|}_{|B_{m}|=1+∑_{k ist direktes Kind von m|B_{k}|}}

endlich √ B_{k} ist endlich, weil Verzweigungsgrad endlich ist und weil (wegen Induktionshypothese) |B_{k}| endlich ist.

4.2 Entscheidbarkeitsresultate zur Terminierung

Satz 4.2.1: Unentscheidbarkeit des Halteproblems für TESe Sei R ein TES über Σ und V, sei t ∈ T (Σ, V). Das Problem, ob t keine unendliche Reduktionen mit →_{R} hat, ist unentscheidbar, aber semi-entscheidbar (Halteproblem). Das Problem, ob R terminiert, d.h. ob alle Terme nur endlich viele Reduktionen haben, ist nicht einmal semi-entscheidbar (universelles Halteproblem). Beweisskizze: Für jede Turingmaschine TM kann man ein TES R(T M) angeben, das TM simuliert. (↷ TESe sind eine turing-vollständige Programmiersprache). Die Unentscheidbarkeitsaussagen folgen daher aus den Unentscheidbarkeitsaussagen für Turigmaschinen. Semi-entscheidbarkeit des Halteproblems: Konstruiere Suchbaum

[figure: t; •; •; •]

wobei u als Kinder die Knoten v_{1}, …, v_{n}, wobei u →_{R} v_{i}.

Endlicher Verzweigungsgrad, weil R endlich und V(r) ⊆ V(l) für alle Regeln l → r. t terminiert gdw. alle Pfade des Suchbaums endlich sind. Lemma von König ↷ wenn t terminiert, dann hat der Baum endlich viele Knoten ↷ dann terminiert das Semi-entscheidungsverfahren mit Erfolg. □

Spezialfall, in dem Terminierung von TES entscheidbar ist: TESe ohne Variablen auf rechten Seiten von Regeln.

Beispiel 4.2.2: and(true, true) → true and(x, false) → false and(false, x) → and(true, not(false)) not(false) → true not(true) → and(false, false) and(false, false) →_{R} and(true, not(true)) →_{R} and(true, and(false, false)) →_{R} and(true, and(true, not(true))) →_{R} and(true, and(true, and(false, false)))

Lemma 4.2.3: Sei R ein TES, wobei V(r) = ∅ für alle l → r ∈ R. Dann terminiert R gdw. es keine Regel l → r ∈ R gibt, so dass r →_{R}^{+} t für einen Term t gilt, der r als Teilterm enthält. Beweis: “⇒“: Falls r →_{R}^{+} t mit t ⊵ r (▷ = echte Teiltermrelation, ⊵ Teiltermrelation) dann terminert R nicht: Sei t|_{π} = r: r →_{R}^{+} t = t[r

[15.06.04] _{π} →_{R}^{+} t[t]_{π} = t[t[r]_{π}]_{π} →_{R} t[t[r]_{π}]_{π} etc. Spezialfall: TESe ohne Variablen auf rechten Seiten: a(t, t) → t a(x, f) → f a(f, x) → a(t, n(t)) n(f) → t n(t) → f a(t, n(t)) → a(t, a(f, f)) → a(t, a(t, n(t))) Beweis von Lemma 4.2.3 “⇐“: Induktion über die Anzahl der Regeln in R: Induktionsanfang: R = ∅ trivial, R terminiert Induktionsschluss: R ≠ ∅ Annahme: r terminiert nicht. Dann existiert ein minimaler Term s, der eine unendliche Reduktion hat ( d.h. alle echten Teilterme von s terminieren) s = s_{0} →_{R} s_{1} →_{R} s_{2} →_{R} … Aufgrund der Minimalität muss in der Auswertung irgendwann eine Regel an der obersten Position E angewendet werden. Es existiert ein s_{i} mit s_{i} = lσ, s_{i+1} = rσ für eine Regel l → r ∈ R. Da V(r) = ∅, ist s_{i+1} = r. Es existiert eine unendliche Reduktion r = s_{i+1} → s_{i+2} → …, die mit der rechten Seite einer Regel startet.

Fall 1 Die Regel l → r wird in der unendliche Reduktion r → s_{i+2} → s_{i+3} → … nicht mehr verwendet.

I.H.: R\{l → r} terminiert. ⚡

Fall 2 Die Regel l → r wird in r → s_{i+2} → s_{i+3} → … verwendet.

Es existiert also j ≥ i + 1 mit r →^{∗} s_{j} = s_{j}[lσ′]_{π} → s_{j}[\underbrace{rσ′}_{r}]_{π} = s_{j+1} →

s_{j+2} → …

Also: r →_{R}^{+} s_{j}[r]_{π}

⚡ zur Vorraussetzung. □

Idee für Entscheidungsverfahren für Terminierung:

• Konstruiere Suchbäume für alle rechten Seiten

[figure: t; •; •; •]

(u hat Kind v gdw. u →_{R} v)

• (a) Wenn Suchbaum für r einen Term \underbrace{t}_{nicht an Wurzel} mit t ⊵ r enthält, dann bricht

man ab, R terminiert also nicht.

• (b) Wenn alle Suchbäume endlich sind, dann stoppt man, R terminiert

(Einer der Fälle a, b tritt immer auf.)

Unterschied zur Terminierung bei allgemeinen TESen:

• bei allgemeinen TESen folgt aus der Terminierung der rechten Seiten nicht die Terminierung des TES. (R = {f(a, x) → f(x, x)} f(a, a) → f(a, a) → … terminiert nicht, Aber die rechte Seite f(x,x) ist Normalform)

• selbst wenn die rechte Seite r eine unendliche Auswertung hat, muss es keinen Term t mit r →^{+} t und t⊵r geben. (R = \{f(x) → f(s(x))\} \underbrace{f(s(x))}_{tritt in der Reduktion nie wieder als Teilterm auf} →

f(s(s(x))) → f(s^{3}(x)) → …)

[Folie Right-ground-Terminierung] T_{i} = Blätter des i-ten Suchbaums (für jede rechte Seite S existiert ein Suchbaum) Schritt 2: Konstruiere die nächste Ebene die Suchbäume T_{1} = {t} T_{2} = {f} T_{3} = {a(t, n(t))} T_{4} = {t} T_{5} = {a(f, f)} T_{1} = ∅ T_{2} = ∅ T_{3} = {a(t, a(f, f))} T_{4} = ∅ T_{5} = {f, a(t, n(t))} T_{1} = ∅ T_{2} = ∅ T_{3} = {a(t, a(t, a(t, n(t))))} T_{4} = ∅ T_{5} = {a(t, a(f, f))} ⇒ “False“

Satz 4.2.4: Sei R ein TES mit V(r) = ∅ für alle l → r ∈ R. Dann ist entscheidbar, ob R terminiert und der Algorithmus RIGHT-GROUND-TERMINIERUNG ist ein Entscheidungsverfahren. Beweis:

Fall 1 R terminiert.

Dann existiert keine rechte Seite r_{i} mit r_{i} →^{+} t ⊵ r_{i}. ↷ Algorithmus gibt nicht “False“ aus.

Kein r_{i} hat unendlich lange Reduktionen und der Suchbaum, der vom Algorithmus konstruiert wird, hat endlichen Verzweigungsgrad. ↷^{Lemma von König} Suchbaum hat nur endlich viele Knoten ↷ Algorithmus terminiert (und gibt “true“ aus).

Fall 2 R terminiert nicht

Wegen Lemma 4.2.3 existiert ein r_{i} →^{+} t⊵r_{i}.Nach endlich vielen Schritten gilt t ∈ T_{i} und der Algorithmus terminiert mit “False“.

□

4.3 Terminierung mit Reduktionsrelationen

Jetzt: untersuche Terminierung von beliebigen TESen (mit Variablen rechts) R terminiert gdw. →_{R} fundiert ist. Grundidee: Nimm eine Relation ≻ auf Termen, von der man weiß, dass sie fundiert ist, und zeige, dass aus s →_{R} t jeweils s ≻ t folgt. Da man dies automatisch überprüfen will, kann man nicht alle unendlich vielen Terme s und t untersuchen. Lösung: Zeige nur l ≻ r für alle (endlich vielen) Regeln l → r. Reicht das, um sicher zu stellen, dass dann aus s →_{R} t auch s ≻ t für alle Terme s, t folgt (d.h. reicht das für die Terminierung?)? Bsp: endless(x) → endless(s(x)) Definieren ≻ wie folgt: t_{1} ≻ t_{2} gdw. t_{1} = endless(x) und t_{2} = endless(s(x)) Es gilt also: endless(x) ≻ endless(s(x)) ⊁ endless(s(s(x))) Problem: ≻ ist nicht stabil! (Aber da Regeln in beliebigen Instantiierungen angewendet werden dürfen, sollte aus l ≻ r auch lσ ≻ rσ für alle σ folgen).

Lösung: Finde fundierte, stabile Relation ≻ und zeige l ≻ r für alle Regeln l → r. Bsp: Echte Teiltermrelation ▷ (s ▷ t ↷ sσ ▷ tσ) Reicht das für die Terminierung? Bsp: infty(x) → s(infty(x)) Definieren ≻ wie folgt: t_{1} ≻ t_{2} gdw. t_{1} = infty(…) und t_{2} = s(…)

• ≻ ist fundiert (infty(…) ≻ s(…))

• ≻ ist stabil

Problem: ≻ ist nicht monoton! (Aus l ≻ r sollte q[lσ]_{π} ≻ q[rσ]_{π} folgen: ≻ muss stabil und monoton sein). ▷: fundiert, stabil, nicht monoton. (f(x) ▷ x, s(f(x)) ⋫ s(x)) →_{||}: t_{1} →_{||} t_{2}, falls t_{1} mehr Symbole enthält als t_{2}: fundiert, nicht stabil(f(x) →_{||} y, f(x)σ ↛_{||} yσ wenn σ(x) = x, σ(y) = s(s(s(s(y))))), monoton Idee für fundierte, stabile, monotone Relation: Modifiziere ▷ so, dass sie auch monoton wird ⇒ Einbettungsordnung

Definition 4.3.1: Für eine Signatur Σ ist die Einbettungsordnung ≻_{emb} (“embedding order“) über T (Σ, V) definiert als s ≻_{emb} t gdw.

• s. Folie (t ist echter Teilterm von s oder kleiner als ein echter Teilterm von s)

• s. Folie (Monotonie)

Hierbei bezeichnet ⪰_{emb} die reflexive Hülle von ≻_{emb}

s(plus(infty(s(x)), y)) ≻_{emb} plus(infty)(x), y), denn plus(infty(s(x)), y) ≻_{emb} plus(infty(x), y) (Punkt 1), denn infty(s(x) ≻_{emb} infty(x) (Punkt 2), denn s(x) ≻_{emb} x (Punkt 2), denn x ⪰_{emb} x (Punkt 1) [18.06.04] Terminierung beliebiger TESe: Zeige l ≻ r für alle Regeln l → r ∈ R (Ziel: s →_{R} t ↷ s ≻ t) ≻ : fundiert, stabil, monoton

\begin{matrix}▷: fundiert, stabil, nicht monoton \\ →_{||} : fundiert, nicht stabil, monoton \end{matrix}\} ↷ Einbettungsordnung

Terminierung lässt sich jetzt mit Hilfe der Einbettungsordnung automatisch nachweisen (denn s ≻_{emb} t lässt sich automatisch untersuchen – Definition von ≻_{emb} lässt sich direkt in einen rekusiven Algorithmus übersetzen) m(x, O) ≻_{emb} x, denn x ⪰_{emb} x (wegen Punkt 1) m(O, s(y)) ≻_{emb} O, denn O ⪰_{emb} O (wegen Punkt 1) m(s(x), s(y)) ≻_{emb} m(x, y), denn s(x) ≻_{emb} x, s(y) ≻_{emb} y (wegen Punkt 2)

Lemma 4.3.2: Die Einbettunsgordnung ist fundiert, stabil, monoton und transitiv Beweis: Fundiertheit: ≻_{emb}⊆→_{||} (d.h. wenn s ≻_{emb} t, dann enthält s mehr Symbole als t). Lässt sich leicht durch strukturelle Induktion zeigen. Da →_{||} fundiert ist, ist auch ≻_{emb} fundiert. Stabilität: z.Z.: s ≻_{emb} t ↷ sσ ≻_{emb} tσ. Strukturelle Induktion über s. Fallunterscheidung anhand der Definition von ≻_{emb}

Fall 1 s = f(s_{1}, …, s_{n}), s_{i} ⪰_{emb} t

↷^{I.H.} s_{i}σ ⪰_{emb} tσ

↷ sσ = f(s_{1}σ, …, s_{i}σ, …, s_{n}σ) ≻_{emb} tσ, denn s_{i}σ ⪰_{emb} tσ (Punkt 1)

Fall 2 s = f(s_{1}, …, s_{n}), t = f(t_{1}, …, t_{n}), s_{i} ≻_{emb} t_{i}, s_{j} ⪰_{emb} t_{j} für alle j ≠ i

↷^{I.H.} s_{i}σ ⪰_{emb} t_{i}σ, s_{j}σ ⪰_{emb} t_{j}σ für alle j ≠ i

↷^{P unkt2} sσ ≻_{emb} tσ

Beweis für Monotonie und Transitivität analog.

□

Definition 4.3.3: Eine Relation ≻ über Termen, die fundiert, stabil und monoton ist, heisst Reduktionsrelation. Eine transitive Reduktionsrelation heisst Reduktionsordnung

Ordnung = transitive und antisymmetrische Relation. (Antisymmetrie: s ≻ t, t ≻ s ↷ s = t) Aus Fundiertheit folgt Irreflexivität und Asymmetrie. (Asymmetrie: s ≻ t ↷ t ⊁ s) Aus Asymmetrie folgt Antisymmetrie.

Satz 4.3.4: Terminierungskriterium mit Reduktionsrelationen, Manna und Ness 1970 Ein TES R terminiert gdw. es eine Reduktionsrelation ≻ gibt, so dass l ≻ r für alle Regeln l → r ∈ R gilt. Beweis: “⇐“ Sei ≻ eine Reduktionsrelation, so dass l ≻ r für alle Regeln l → r Dann folgt für alle Terme s, t aus s →_{R} t, dass s ≻ t gilt. (Grund: s →_{R} t ↷ es existiert π ∈ Occ(s) und σ ∈ SUB(Σ, V) mit s|_{π} = lσ, t = s[rσ]_{π} für eine Regel l → r ∈ R.

Es gilt l ≻ r ↷^{Stabil} lσ ≻ rσ ↷^{Monoton} \underbrace{s[lσ]_{π}}_{s} ≻ \underbrace{s[rσ]_{π}}_{t}.)

4.4. SIMPLIFIKATIONSORDNUNGEN UND REKURSIVE PFADORDNUNGEN51

Falls R nicht terminieren würde, gäbe es eine unendliche Reduktion: t_{0} →_{R} t_{1} →_{R} t_{2} →_{R} … ↷ t_{0} ≻ t_{1} ≻ t_{2} ≻ … ⚡ zur Fundiertheit von ≻ “⇒“: R terminiert: Finde Reduktionsrelation ≻ mit l ≻ r für alle Regeln l → r ∈ R. Lösung: ≻:=→_{R} (

• l →_{R} r

• →_{R} fundiert, weil R terminiert

• →_{R} stabil und monoton (Lemma 3.1.13: jede Ersetzungsrelation ist monoton und stabil)

) □

Automatische Termverfahren:

• Wähle eine Reduktionsrelation ≻, bei der entscheidbar ist, ob s ≻ t gilt (für alle s, t)

• Untersuche, ob l ≻ r für alle Regeln l → r ∈ R gilt.

• Wenn ja: “TES R terminiert“

(Falls l ⊁ r für eine Regel, so folgt daraus nicht, dass R nicht terminiert. Es könnte eine andere Reduktionsrelation ≻′ geben, bei der l ≻′ r für alle Regeln gilt.) Bsp. plus: plus(O, y) ≻_{emb} y plus(s(x), y) ⊁_{emb} s(plus(x, y)) ⇒ Terminierungsnachweis mit ≻_{emb} scheitert ↷ Verfahren ist zu schwach

4.4 Simplifikationsordnungen und rekursive Pfadordnungen

Einbettungsordnung: 1. Schritt zur Entwicklung von Reduktionsordnungen, die zum Terminierungsnachweis geeignet sind. Entwickle stärkere Ordnungen, die die Einbettungsordnung enthalten.

Definition 4.4.1: Eine Reduktionsordnung ≻ mit ≻_{emb}⊆≻ (d.h.: s ≻_{emb} t ↷ s ≻ t) heisst Simplifikationsordnung.

Wenn man eine neue Relation ≻ definiert, muss man anschliessend zeigen, dass es wirklich eine Reduktionsordnung ist. Wenn man weiss, das ≻ die Einbettungsordnung enthält, reicht es, statt der Fundiertheit nur die Irreflexivität zeigen.

Satz 4.4.2: Satz von Kruskal, 1960

a) Für jede unendliche Folge von Grundtermen t_{0}, t_{1}, … existieren t_{i}, t_{j} mit i < j, so dass t_{i} ⪯_{emb} t_{j} b) Jede stabile, monotone, transitive Relation ≻, die die Teiltermeigenschaft

f(x_{1}, …, x_{n}) ≻ x_{i} für alle f ∈ Σ und alle 1 ≤ i ≤ n erfüllt, enthält die Einbettungsordnung (d.h. ≻_{emb}⊆≻)

c) Jede stabile, monotone, transitive, irreflexive Relation ≻, die die obige Teiltermeigenschaft erhält, ist fundiert (und damit eine Simplifikationsordnung).

(d.h. um zu zeigen, dass ≻ eine Simplifikationsordnung ist, muss man nur diese 5 Fakten nachweisen). Beweis:

a) ist der eigentliche Satz von Kruskal (→ Literatur)

b) zu Zeigen: s ≻_{emb} t ↷ s ≻ t (sehr leicht, strukturelle Induktion über s)

c) Annahme: ≻ nicht fundiert (aber stabil, monoton, transitiv, irreflexiv, hat die Teiltermeigenschaft)

↷ es existiert t_{0} ≻ t_{1} ≻ t_{2} ≻ …

Sei σ eine Substitution, die alle Variablen der t_{i} durch Grundterme instantiiert. (Man kann leicht zeigen, dass V (t_{0}) ⊇ V (t_{1}) ⊇ … ⇒ DOM(σ) ist endlich)

↷^{stabil} t_{0}σ ≻ t_{1}σ ≻ t_{2}σ ≻ …, alle t_{i}σ sind Grundterme.

↷^{(a)} es existiert i < j mit t_{i}σ ⪰_{emb} t_{j}σ ↷^{≻_{emb}⊆≻wegen (b))} t_{i}σ ⪰ t_{j}σ (1)

Andererseits: t_{i}σ ≻ … ≻ t_{j}σ

Transitivität: t_{i}σ ≻ t_{j}σ (2)

t_{i}σ ≻^{(i)} t_{1}σ ⪰ t_{i}σ ↷^{Transitivität} t_{1}σ ≻ t_{i}σ

⚡ zur Irreflexivität

□ [22.06.04]

R TES terminiert gdw. es eine Reduktionsrelation ≻ gibt, mit l ≻ r für alle l → r ∈ R ≻_{emb} ist Reduktionsordnung, aber zu schwach. ⇒ Definition stärkerer Reduktionsordnungen ≻ ( mit ≻_{emb}⊆≻): Simplifikationsordnungen

1. solche Ordnung: lexikographische Pfadordnung (lpo) Zum Vergleich von f(s_{1}, … s_{n}) und f(t_{1}, …, t_{n}) muss man die Argumenten tupel (s_{1}, … s_{n}) und (t_{1}, …, t_{n}) vergleichen. Also: Wie kann man eine Relation auf Termen zu einer Relation auf Tupeln erweitern? Hier: 2 Möglichkeiten: vergleiche Tupel \underbrace{lexikographisch}_{(lpo)} oder als \underbrace{Multimengen}_{rekursive Pfadordnung (rpo)}

Definition 4.4.3: Lexikographische Konbination von Relationen Sei ≻_{1} eine Relation auf einer Menge T_{1} (≻⊆ T_{1} × T_{1}) unde ≻_{2} eine Relation auf T_{2}. Dann wird die lexikographische Kombination ≻_{1×2} auf T_{1} × T_{2} wie folgt definiert: (s_{1}, s_{2}) ≻_{1×2} (t_{1}, t_{2}) gdw. s_{1} ≻_{1} t_{1} oder (s_{1} = t_{1} und s_{1} ≻_{2} t_{2}) Analog dazu kann man die lexikographische Kombination von n Relationen ≻_{1} , ≻_{1}, …, ≻_{n} definieren: (s_{1}, …, s_{n}) ≻_{1×...×n} (t_{1}, …, t_{n}) gdw. es existiert i ∈ {1, …, n} mit s_{i} ≻_{i} t_{i} und s_{j} = t_{j} für alle 1 ≤ j < i. Die n-fache lexikographische Kombination einer Relation ≻ mit sich selbst wird als ≻_{lex}^{n} bezeichnet.

Beispiel 4.4.4: (3, 5)(>_{ℕ})^{2}(2, 6), (3, 5)(>_{ℕ})^{2}(3, 4), (3, 5)(≯_{ℕ})^{2}(4, 1) Im Lexikon: >_{alph} (a >_{alph} b >_{alph} c >_{alph} …) hans >_{alph}^{4} hugo >_{alph}^{4} kurt Fundiertheit bleibt bei lexikographischen Kombinationen erhalten. Hierbei ist es wichtig, dass die Grösse der Tupel, die verglichen werden, nicht wächst. Die Relation in Lexika hat diese Beschränkung nicht und ist deshalb nicht fundiert. a > ba > bba > bbba > …

Satz 4.4.5: Fundiertheit bleibt bei lexikographischen Kombinationen erhalten Sei ≻_{1} eine Relation auf der nicht-leeren Menge T_{1}, sei ≻_{2} eine Relation auf der nicht-leeren Menge T_{2}. Dann gilt: ≻_{1} und ≻_{2} sind fundiert gdw. ihre lexikographische Kombination ≻_{1×2} fundiert ist. Beweis: “⇐“: ≻_{1×2} sei fundiert. ≻_{1} ist auch fundiert: Falls nicht, dann existiert u_{1} ≻_{1} u_{2} ≻_{1} u_{3} ≻_{1} … Sei v ∈ T_{2} beliebig (u_{1}, v) ≻_{1×2} (u_{2}, v) ≻_{1×2} … ⚡ zur Fundiertheit. ≻_{2} ist auch fundiert: Falls nicht, dann existiert v_{1} ≻_{1} v_{2} ≻_{1} v_{3} ≻_{1} … Sei u ∈ T_{1} beliebig (u, v_{1}) ≻_{1×2} (u, v_{2}) ≻_{1×2} … ⚡ zur Fundiertheit. “⇒“: ≻_{1}, ≻_{2} seien fundiert. Annahme: es existiert eine unendliche Folge (u_{1}, v_{1}) ≻_{1×2} (u_{2}, v_{2}) ≻_{1×2} (u_{3}, v_{3}) ≻_{1×2} … Wir wissen u_{1} ⪰_{1} u_{2} ⪰_{1} u_{3} ⪰_{1} … Da ≻_{1} fundiert ist, existiert ein i mit u_{i} = u_{j} für alle j ≥ i. (u_{i}, v_{1}) ≻_{1×2} (u_{i}, v_{i+1}) ≻_{1×2} (u_{i}, v_{i+2}) ≻_{1×2} … ↷ v_{i} ≻_{2} v_{i+1} ≻_{2} v_{i+2} ≻_{2} … ⚡ zur Fundiertheit von ≻_{2} □

Aus Satz folgt: Wenn ≻ eine fundierte Relation auf Termen ist, dann ist ≻_{lex}^{n} eine fundierte Relation auf n-Tupeln von Termen. ⇒ Definieren die lpo: s ≻_{lpo} t – wann soll dies gelten?

1. Es soll gelten, wenn ein direkter Teilterm von s grösser oder gleich t ist (wie bei ≻_{emb})

2. Beim Vergleich von s = f(s_{1}, …, s_{n}) und t = f(t_{1}, …, t_{n}): Vergleiche die Tupel (s_{1}, …, s_{n}) und (t_{1}, …, t_{n}) lexikographisch, d.h. (s_{1}, …, s_{n})(≻_{lpo}^{n} (t_{1}, …, t_{n}).

Problem: So wird die Ordnung nicht fundiert: f(s(O), O) ≻ f(O, f(s(O), O)) (1)

denn s(O) ≻ O (denn O ⪰ O). Andererseits: \underbrace{f(O, f(s(O), O)) ≻ f(s(O), O)}_{(2)},

denn f(s(O), O) ⪰ f(s(O), O)

(1) und (2) verletzen Fundiertheit

Abhilfe: Verlange, dass die Teilterme t_{i+1}, …, t_{n} rechts wenigstens kleiner als die gesamte linke Seite f(s_{1}, …, s_{n}) sind.

3. Ein wesentlicher Grund für die Schwäche von ≻_{emb} ist, dass man Terme mit unterschiedliche äussersten Funktionssymbol schlecht vergleichen kann. Wie vergleicht man s = f(s_{1}, …, s_{n}), t = g(t_{1}, .., t_{m}). Verwende hierzu eine zugrundeliegende Ordnung ] auf Funktionssymbolen (“Präzedenz“) Überprüfe dann, on f]g gilt.

Problem: zerstört Fundiertheit: Sei f g: f(x) ≻ g(f(x)) (1)

Andererseits: \underbrace{g(f(x)) ≻ f(x)}_{(2)}, denn f(x) ⪰ f(x).

(1) und (2) zerstören Fundiertheit

Abhilfe: Verlange zusätzlich, dass die Teilterme t_{1}, …, t_{m} rechts wenigstens kleiner als die gesamte linke Seite f(s_{1}, …, s_{n}) sind.

Definition 4.4.6: Lexikographische Pfadordnung, Kamin und Lévy. 1980

Für eine Signatur Σ und eine fundierte Ordnung ] auf Σ (“Präzedenz“) ist die lexikographische Pfadordnung (lpo) über T (Σ, V) definiert als s ≻_{lpo} t gdw. s. [Folie]

Beispiel 4.4.7:

Verwende lpo für Terminierungsbeweise.

plus(O, y) → y  l ≻_{lpo} r, denn y ⪰_{lpo} y
(folgt auch, da l ≻_{emb} r)
plus(s(x), y) → s(plus(x, y))  Wähle Präzedenz mit plus]s.
z.Z.: plus(s(x), y) ≻_{lpo} plus(x, y)
times(O, y) → O  l ≻_{lpo} r, da l ≻_{emb} r denn s(x) ≻_{lpo} x
times(s(x), y) → plus(y, times(x, y)) wähle Präzedenz times]plus
z.Z. times(s(x), y) ≻_{lpo} y
times(s(x), y) ≻_{lpo} y  ← gilt bereits bei ≻_{emb}
times(s(x), y) ≻_{lpo} times(x, y)  ← gilt bereits bei ≻_{emb}

Für Terminierungsbeweise mit lpo kann man eine beliebige (fundierte) Präzedenz verwenden. Um Terme mit lpo zu untersuchen, könnte man alle (endlich vielen) Präzedenzen durchprobieren. Besser: Lasse Präzedenz offen und erweitere sie nur dann, wenn dies zum beweisen von l ≻ r nötig ist. Bei der Erweiterung von ] muss jeweils die Fundiertheit von ] sichergestellt sein.

Beispiel 4.4.8:

sum(O, y) → y  l ≻_{lpo} r, da l ≻_{emb} r
sum(s(x), y) → sum(x, (s(y)) l ≻_{lpo} r : s(x) ≻_{lpo} x

sum(s(x), y) ≻_{lpo} s(y) wähle Präzedenz sum]s z.Z. sum(s(x), y) ≻_{lpo} y

[25.06.04]

Ziel: Zeige lpo ist eine Simplifikations-Ordnung. Satz von Kruskal: es reicht, folgendes zu zeigen: stabil, monoton, transitiv, Teiltermeigenschaft (f(x_{1}, …, x_{n}) ≻ x_{i}), irreflexiv

Satz 4.4.9: Die lpo ist eine Simplifikationsordnung Beweis: Teiltermeigenschaft: F (x_{1}, …, x_{i}, …, x_{n}) ≻_{lpo} x_{i}, denn x_{i} ⪰ x_{i} (Punkt 1 von Definition 4.4.6) Stabilität: z.Z.: Falls s ≻_{lpo} t, dann sσ ≻_{lpo} tσ (*) Induktion über s, t,. Induktionsrelation: ▷_{lex}^{2} (fundiert, Satz 4.4.5) ↷ noethersche Induktion möglich. D.h.: Wenn wir (*) für s, t zeigen wollen, dürfen wir sie für die Terme s′, t′ als Induktionshypothese voraussetzen, bei denen s ▷ s′ oder (s = s′ und t ▷ t′) gilt. Fallunterscheidung anhand der Definition der lpo: s ≻_{lpo} t

Fall 1 s = f(s_{1}, …, s_{i}, …, s_{n}), s_{i} ⪰_{lpo} t Induktionshypothese: s_{i}σ ⪰_{lpo} tσ

sσ = f(s_{1}σ, …, s_{i}σ, …, s_{n}σ) ≻_{lpo} tσ (Punkt 1 der Definition 4.4.6)

Fall 2 s = (f(s_{1}, …, s_{n}), t = g(t_{1}, …, t_{m}), f]g, s ≻_{lpo} t_{j}∀j ∈ {1, …, m}

Induktionshypothese: sσ ≻_{lpo} t_{j}σ

sσ = f(s_{1}σ, …, s_{n}σ), tσ = g(t_{1}σ, …, t_{m}σ), f]g, sσ ≻_{lpo} t_{j}σ für alle

j ∈ {1, …, m} ↷ sσ ≻_{lpo} tσ (Punkt 2 von Definition 4.4.6)

Fall 3 s = f(s_{1}, …, s_{i−1}, s_{i}, s_{i+1}, …, s_{n}), t = f(s_{1}, …, s_{i−1}, t_{i}, t_{i+1}, …, t_{n}), s_{i} ≻_{lpo} t_{i}, s ≻_{lpo} t_{j} für alle j

Induktionshypothese: s_{i}σ ≻ t_{i}σ, sσ ≻ t_{j}σ ↷ sσ ≻_{lpo} tσ (Punkt 3 von Definition 4.4.6)

Transitivität: z.Z. wenn s ≻_{lpo} t und t_{i} ≻_{lpo} r, dann s ≻_{lpo} r Induktion über s, t, r. Induktionsrelation: ▷_{lex}^{3} (Übung) Monotonie: z.Z. s ≻_{lpo} t ↷ q[s]_{π} ≻_{lpo} q[t]_{π} Induktion über π (Übung) Irreflexivität: z.Z. für alle Terme s gilt: s ⊁_{lpo} s Strukturelle Induktion über s Annahme: s ≻_{lpo} s. Fallunterscheidung anhand Definition 4.4.6

Fall 1 s = f(s_{1}, …, s_{i}, …, s_{n}), s_{i} ⪰_{lpo} s (da s_{i} ≠ s gilt s_{i} ≻_{lpo} s)

Es gilt aber auch: s ≻_{lpo} s_{i} s_{i} ≻_{lpo} s ≻_{lpo} s_{i} ↷^{Transitivität} s_{i} ≻_{lpo} s_{i}

⚡ zur Induktionshypothese

Fall 2 nicht anwendbar, da dann s 2 verschiedene äussere Funktionssymbole f, g haben müsste.

Fall 3 s = f(s_{1}, …, s_{i}, …, s_{n}), s_{i} ≻_{lpo} s_{i}

⚡ zur Induktionshypothese.

□

LPO darf für Terminierungsbeweise verwendet werden, mit beliebiger Präzedenz (fundierte Ordnung auf Funktionssymbolen). Automatisierung: beginne mit unbestimmter Präzedenz und erweitere sie, falls nötig. Hierbei muss Fundiertheit der Präzedenz sicher gestellt sein. → Die Frage, ob ein TES mit einer lpo terminiert, ist entscheidbar, aber NP-vollständig. ⇒ es existieren terminierende TES, deren Terminierung nicht mit lpo gezeigt werden kann.

pred(O) → Opred(succ(x)) → xminus(x, O) → xminus(x, succ(y)) → minus(pred(x), y)

Bei den ersten 3 Regeln gilt schon l ≻_{emb} r. minus(x, s(y)) ⊁_{lpo} minus(pred(x), y), denn x ⊁_{lpo} pred(x) (stattdessen: pred(x) ≻_{lpo} x) Lösung: im lexikalischen Vergleich sollte man hier nicht von links nach rechts, sondern von rechts nach links vorgehen.

⇒ Ändere 3. Punkt der lpo wie folgt: s = f(s_{1}, …, s_{i−1}s_{i}, s_{i+1}, …, s_{n}), t = f(t_{1}, …, t_{i}, s_{i+1}, …, s_{n}), s_{i} ≻_{lpo} t_{j} für alle j. Jetzt minus(x, s(y)) ≻_{lpo} minus(p(x), y), denn s(y) ≻_{lpo} p(x) (bei minus]p) Bsp.: Kombiniere die pred-, minus-Regeln von oben mit den sum-Regeln (vgl. Folie) Problem: Für sum müssen die Argumente von links nach rechts verglichen werden, Für minus müssen die Argumente von rechts nach links verglichen werden. Lösung: Zu jedem n-stelligen Funktionssymbol gibt man einen Status π an, der sagt, in welcher Reihenfolge die Argumente des Funktionssymbols verglichen werden sollen. π ist Permutation der Zahlen 1, …, n im Bsp.: sum bekommt Status <1,2> minus bekommt Status <2,1> ⇒ Lexikalische Pfadordnung mit Status (lpos) (Terminierung mit lpos bleibt unentscheidbar und NP-Vollständig) ↷ es existieren immer noch TESe, bei denen Terminierung nicht mit lpos gezeigt werden kann.

Beispiel 4.4.10: plus(O, y) → y plus(s(x), y) → s(plus(y, x)) Bei lpos ist die Terminierung nicht zu zeigen, denn s(x) ⊁_{lpos} y und y ⊁_{lpos} x Lösung: Man sollte Tupel von Termen so vergleichen, dass die Reihenfolge der Tupelkomponenten keine Rolle spielt. ⇒ Vergleiche Termtupel als Mengen ({y, x} = {x, y}). Problem: bei Mengen werden Duplikate eliminiert ({x, x} = {x}) ⇒ Vergleiche Termtupel als Multimengen (= Mengen, in denen Elemente mehrmals auftreten dürfen {1, 1, 2} = {2, 1, 1} ≠ {1, 2}).

Definition 4.4.11: Multimengen Sei T eine nicht-leere Menge. Eine ungeordnete endliche Folge von Elementen aus T heisst Multimenge über T. M(T) = Menge aller (endlichen) Multimengen über T. Eine Multimenge M ist durch ihre charakteristische Funktion #_{M}: T → ℕ definiert, wobei #_{M}(t) die Anzahl der Vorkommen von t in M angibt. Es gilt also t ∈ M gdw. #_{M}(t) > 0. Auf Multimengen werden folgende Operationen definiert:

• M = N gdw #_{M}(t) = #_{N}(t) für alle t ∈ T

• M ⊆ N gdw #_{M}(t) ≤ #_{N}(t) für alle t ∈ T

• M ⊂ N gdw #_{M}(t) < #_{N}(t) für alle t ∈ T gdw M ⊆ N, M ≠ N

• M ∪ N ist die Multimenge mit #_{M∪N}(t) = #_{M}(t) + #_{N}(t) für alle t ∈ T • M ∩ N ist die Multimenge mit #_{M∩N}(t) = min(#_{M}(t), #_{N}(t)) für alle

t ∈ T

• M\N ist die Multimenge mit #_{M\N}(t) = max(=, #_{M}(t) − #_{N}(t))

[29.06.04] Beispiel 4.4.12: Variation der lpo: Vergleiche Tupel von Argumenten nicht lexikographisch, sondern als Multimengen 4,5,6,6,7,7 Bei lexikographischen Ordnungen: erweitere eine Relation ≻ auf T zu einer Relation ≻_{lex}^{n} auf T^{n}. Fundiertheit bleibt erhalten. Bei Multimengen-Ordnungen: erweitere eine Relation ≻ auf T zu einer Relation ≻_{mul} auf M(T). Fundiertheit bleibt erhalten.

Definition 4.4.13: Multimengenrelation Sei ≻ eine Relation auf T (≻⊆ T × T). Dann ist die Relation ≻_{mul} auf M(T) definiert als M ≻_{mul} N gdw

• X ⊆ M, X ≠ ∅ (Lasse die Elemente X aus M weg und ersetze sie duch die Elemente Y)

• N = (M\X) ∪ Y

• für jedes y ∈ Y existiert ein x ∈ X mit x ≻ y

Beispiel 4.4.14: M = {3, 6, 8} N = {4, 5, 6, 6, 7, 7}: M(>_{ℕ})_{mul}N, denn X = {3, 8} = M\N Idee: Lasse beliebig viele Elemente aus M weg (mindestens eines) und ersetze jedes dieser Elemente durch beliebig viele kleinere (gegebenenfalls durch keines) Y = {4, 5, 6, 7, 7} = N\M für alle y ∈ Y existiert 8 ∈ X mit 8 >_{ℕ} y

Satz 4.4.15: Fundiertheit bleibt bei Multimengen erhalten, Derchowitz 1979 Sei ≻ eine Relation auf der Menge T. Dann gilt: ≻ ist fundiert gdw ≻_{mul} ist fundiert. Beweis: “⇐“: Sei ≻_{mul} fundiert. Ann.: es existiert t_{0}, t_{1}, … ∈ T mit t_{0} ≻ t_{1} ≻ ... ↷ {t_{0}} ≻_{mul} {t_{1}} ≻_{mul} {t_{2}} ≻_{mul} … ⚡ zur Fundiertheit von ≻_{mul} “⇒“: Sei ≻ fundiert. Ann.: es existiert M_{0}, M_{1}, … ∈ M(T) mit {M_{0}} ≻_{mul} {M_{1}} ≻_{mul} {M_{2}} ≻_{mul} … Konstruiere Schritt für Schritt einen unendlichen Baum, dessen Knoten mit Elementen aus T markiert sind.

Baum hat endlichen Verzweigungsgrad und entlang jedes Pfades werden die Elemente aus T bzgl. ≻ kleiner. Lemma von König → Baum muss unendlichen Pfad haben ↷ ⚡ zur Fundiertheit von ≻ Konstruktion des Baumes: erweitere T um ein weiteres Element ⊥ mit t ≻ ⊥ für alle t ∈ T. Fundiertheit von ≻ bleibt erhalten. Im i-ten Schritt der Konstruktion sind die Blätter des Baums mit den Elementen von M_{i} markiert.

0. Schritt: beliebige Wurzel, Kinder der Wurzel sind Elemente von M_{0} (Bsp.: M_{0} = {3, 6, 8}

\xymatrix{ & [] \ar[dl] \ar[d] \ar[dr] \\ [3] & [6] & [8]}

)

1. Schritt M_{0} ≻_{mul} M_{1} ↷ es existiert X ⊆ M_{0}, X ≠ ∅, M_{1} = (M_{0}\X) ∪ Y für alle y ∈ Y existiert x ∈ X mit x ≻ y. Für jedes y ∈ Y fügen wir ein neues Blatt hinzu und machen daraus das Kind eines Knoten x ∈ X mit x ≻ y. Ausserdem erhält jeder Knoten x ∈ X ein Kind ⊥. ↷ Blätter sind die Elemente von M_{1} (und ⊥)

\xymatrix{ & [] \ar[dl] \ar[d] \ar[dr] \\ [3] \ar[d] & [6] & [8] \ar[dl] \ar[d] \ar[dr] \ar[drr] \ar[drrr] \ar[drrrr] \\ [⊥] & [4] & [5] & [6] & [7] & [7] & [⊥]}

(Bsp.: M_{1} = {4, 5, 6, 6, 7, 7} X = {3, 8} Y = {4, 5, 6, 7, 7}) i + 1 - ter Schritt: analog → Verzweigungsgrad bleibt endlich → entlang eines Pfades werden die Knoten immer kleiner bzgl. ≻ (*)

→ in jedem Schritt wächst der Baum ↷ Baum wird unendlich ↷^{LemmavonKönig} es existiert unendlicher Pfad. Mit (*) ergibt sich ⚡ zur Fundiertheit von ≻ □

Definition 4.4.16: Rekursive Pfadordnung, Derchowitz 1982 Für eine Signatur Σ und eine fundierte Ordnung ] über Σ (“Präzedenz“) ist die rekursive Pfadordnung (rpo) über T (Σ, V) definiert als s ≻_{rpo} t gdw

• s = f(s_{1}, …, s_{n}) und s_{i} ⪰_{rpo} t für ein i ∈ {1, …, n} • s = f(s_{1}, …, s_{n}), t = g(t_{1}, …, t_{n}), f]g und s ≻_{rpo} t_{j} für alle j ∈

{1, …, m}

• s = f(s_{1}, …, s_{n}), t = f(t_{1}, …, t_{n}) und {s_{1}, …, s_{n}}(≻_{rpo})_{mul}{t_{1}, …, t_{n}}

Beispiel 4.4.17:

plus(O, y) → yplus(O, y) ≻_{rpo} y
plus(s(x), y) → s(plus(y, x))plus(s(x), y) ≻_{rpo} s(plus(y, x)), denn bei plus]s
plus(s(x), y) ≻_{rpo} plus(y, x), denn {s(x), y}(≻_{rpo})_{mul}{y, x}
\{s(x), y\}(≻_{rpo})_{mul}\{y, \underline{x}\}, denn s(x) ≻_{rpo} x

(Genauso: \{\underline{s(x)}, y\}(≻_{rpo})_{mul}\{\underline{x}, \underline{x}\} ↷ plus(s(x), y) ≻_{rpo} plus(x, x))

Satz 4.4.18: Die rekursive Pfadordnung ist eine Simplifikationsordnung Es existieren Beispiele, bei denen rpo erfolgreich ist und lpos scheitert. Es existieren Beispiele, bei denen lpos erfolgreich ist und rpo scheitert. Bei sum: sum(s(x), y) ⊁_{rpo} sum(x, s(y)), denn \{s(x), y\}(⊁_{rpo})_{mul}\{\underline{x}, \underline{s(y)}\}, denn s(x) ⊁_{rpo} s(y), y ⊁_{rpo} s(y) Vorteil rpo: Reihenfolge der Argumente ist unerheblich. Vorteil lpo: Man kann in manchen Argumenten kleiner und in anderen grösser werden. Wie erhält man eine Ordnung, die die Vorteile von rpo und lpos verbindet? ⇒ Erweitere das Konzept des Status: Jedes Funktionssymbol bekommt einen Status: Entweder Permutation der Zahlen 1, …, n (bei n-stellingen Funktionssymbol) ↷ dann muss man die Argumente lexikographisch wie bei lpos vergleichen. Oder Status ist “mul“ ↷ vergleiche Argumente als Multimenge wie bei rpo. ⇒ rekursive Pfadordnung mit Status (rpos) Zeigt die Terminierung des sum + plus - TES, wenn sum Status <1,2> und plus Status “mul“ bekommt. Es ist entscheidbar, ob es zu einem TES eine rpos gibt, mit der man die Terminierung zeigen kann. Es existieren immer noch terminierendes TESe, deren Terminierung nicht mit rpos gezeigt werden kann. → Andere Simplifikationsordnungnen (Knuth-Bendix Ordnung, Polynomordnungen) → Es existieren auch terminierende TESe, deren Terminierung mit keiner Simplifikationsordnung gezeigt werden kann. Bsp: f(f(x)) → f(g(f(x))) Terminiert, denn in jedem Reduktionsschritt verringert sich die Zahl der nebeneinander stehenden f’s. Aber: f(g(f(x))) ≻_{emb} f(f(x)), d.h. f(g(f(x))) ≻ f(f(x)) in jeder Simplifikationsordnung ≻ ↷ f(f(x)) ⊁ f(g(f(x)))), wegen Fundiertheit von ≻ Es existieren unendlich viele natürliche TESe / Programme mit demselben Problem → Weitergehende Termmethoden, die auf Simplifikationsordnungen aufbauen (z.B Dependency Pairs) Techniken für Terminierungsbeweise von TESen können für Terminierungsnachweis von Programmen in verschiedenen Programmiersprachen angepasst werden.

[02.07.04] 62 KAPITEL 4. TERMINIERUNG VON TERMERSETZUNGSSYSTEMEN

Konfluenz von Termersetzungssystemen

Generell interessant: Techniken zum Nachweis der Eindeutigkeit von Programmen Beruht auf Unifikation

• Konfluenzprüfung und Vervollständigung von TESen

• Haupttechnik zur Auswertung von Logikprogrammen

• Typüberprüfung in polymorph getypten Programmiersprachen (z.B. die meisten funktionalen Sprachen: Haskell, ML)

• Automatisches Beweisen (z.B. Resolutionskalkül)

5.1 Unifikation

Definition 5.1.1: Unifikation Zwei Terme s, t sind unifizierbar gdw. es eine Substitution σ gibt, so dass sσ = tσ. Solch eine Substitution heisst Unifikator von s und t. Bsp.: g(f(x), y) =^{?} g(y, f(z)) ist lösbar. Unifikator σ = {x/z, y/f(z)} Ein Unifikationsproblem über Σ, V ist eine endliche Menge von Termgleichungen S = {s_{1} =^{?} t_{1}, …, s_{n} =^{?} t_{n}} mit s, t ∈ T (Σ, V). Eine Substitution σ ist Lösung oder Unifikator des Unifikationsproblems S gdw. s_{i}σ = t_{i}σ für alle i ∈ {1, …, n}. U(S) ist die Menge aller Unifikatoren von S. Im allgemeinen gibt es mehrere Unifikatoren (meist unendlich viele): Im obigen Beispiel sind neben σ auch die folgenden Substitutionen Unifikatoren: σ_{1} = {x/a, y/f(a), z/a} (a ∈ Σ_{0}) σ_{1} = {x/f(z), y/f(f(z)), z/f(z)} σ_{1} = {z/x, y/f(x)} Die Substitutionen σ und σ_{3} sind allgemeiner als die Substitutionen σ_{1} und σ_{2}: Man kann σ_{1}, σ2 erhalten, indem man erst σ oder σ_{3} anwendet und anschliessend eine weitere Substitution anwendet. σ_{1} = \underbrace{σ ∘ δ_{1}}_{Komposition: erst σ anwenden, dann δ_{1}} mit δ_{1} = \{z/a\}, σ_{2} = σ ∘ δ_{2} mit δ_{2} =

{z/f(z)}, σ_{3} = σ ∘ δ_{3} mit δ_{3} = {z/x} σ_{1} = σ ∘ δ′_{1} mit δ′_{1} = {x/a}, σ_{2} = σ ∘ δ′_{2} mit δ′_{2} = {x/f(z)}, σ_{3} = σ ∘ δ′_{3} mit δ′_{3} = {x/z} ⇒ σ und σ_{3} sind allgemeiner als σ_{1}, σ_{2}. ⇒ sind allgemeine Unifikatoren.

Definition 5.1.2: Allgemeinster Unifikator Eine Substitution σ ist allgemeiner als σ′ gdw. es eine Substitution δ mit σ′ = σ ∘ δ. Eine Substitution σ ist allgemeinster Unifikator (most general unifier, mgu) eines Unifikationsproblems S gdw. σ ∈ U(S) und σ allgemeiner als alle σ′ ∈ U(S) ist. Schreibweise: “σ ∘ δ“ wird oft als “σδ“ geschrieben. ↷ t(σ ∘ δ = tσδ = (tσ)δ Bsp.: verschiedene mgu’s: σ = {x/z, y/f(z)} σ_{3} = {z/x, y/f(x)} Diese beiden Substitutionen sind “gleich allgemein“ ↷ sind identisch bis auf Variablenumbenennung

Lemma 5.1.3: Eindeutigkeit allgemeinster Unifikatioren Seien σ, σ′ zwei Substitutionen. Falls σ allgemeiner als σ′ ist und σ′ allgemeiner als σ ist, dann existiert eine Variablenumbenennung δ mit σ′ = σ ∘ δ. Hierbei heisst eine Substitution δ Variablenumbennenung gdw. δ injektiv ist und xδ ∈ V für alle x ∈ V gilt. Beweis: Übung σ_{3} = σ ∘ δ, δ Variablenumbenennung. δ_{3} = {z/x} ist nicht injektiv δ_{3}(z) = δ_{3}(x) = x δ = {z/x, x/z} Mit einem einzigem mgu kann man die Menge der Lösungen U(S) repräsentieren.

Lemma 5.1.4: Darstellung der Lösungen eines Unifikationsproblems Sei S ein Unifikationsproblem über Σ, V, sei σ ein allgemeinster Unifikator von S. Dann gilt: U(S) = {σδ|δ ∈ SUB(Σ, V)} Beweis: “⊆“: σ′ ∈ U(S). Dann gilt σ′ ∈ {σδ|δ ∈ SUB(Σ, V)}, nach der Definition des mgu. “⊇“: Sei δ ∈ SUB(Σ, V). Dann gilt σδ ∈ U(S), denn für alle s =^{?} t ∈ S gilt: sσ = tσ (denn σ ∈ U(S))

↷ (Sσ)δ = (tσ)δ. □

Ziel: Entwickle Unifikationsalgorithmus, der zu einem Unifikationsproblem S entscheidet, ob es lösbar ist und falls ja, einen mgu berechnet. Vorgehen: Transformiere das Unifikationsproblem S so lange, bis es in “gelöster Form“ ist. Dann kann man den mgu direkt ablesen.

Definition 5.1.5: Ein Unifikationsproblem S = {x_{1} =^{?} t_{1}, …, x_{n} =^{?} t_{n}} ist in gelöster Form gdw. die x_{i} paarweise verschiedene Variablen sind, die in den Termen t_{1}, …, t_{n} nicht vorkommen. Zu einem Unifikationsproblem in gelöster Form wie oben definieren wir die Substitution σ_{S} = {x_{a}/t_{1}, …, x_{n}/t_{n}}. Bsp.: {g(f(x), y) =^{?} g(y, f(z))} ⇒^{∗} {x =^{?} z, y =^{?} f(z)}: σ_{S′} = {x/z, y/f(z)} {x =^{?} f(x)} ist nicht lösbar: Für jede Substitution σ hat f(x)σ ein Zeichen mehr als xσ ↷ f(x)σ ≠ xσ. x =^{?} t mit x ∈ V(t) ist imer unlösbar, falls t = x. (Occur Failure)

Lemma 5.1.6: Sei S ein Unifikationsproblem in gelöster Form. Dann ist σ_{S} mgu von S und für alle Unifikatoren σ′ von S gilt: σ′ = σ_{S} ∘ σ′. Beweis:

• σ_{s} ∈ U(S): Für alle x_{i} =^{?} t_{i} ∈ S gilt: x_{i}σ_{S} = t_{i} t_{i}σ_{S} \underbrace{=}_{denn die Variablen x_{1}, …, x_{n} treten nicht in t_{i} auf} t_{i}σ_{S}

• für alle σ′ ∈ U(S). σ′ = σ_{S}σ′

↷ Zeige yσ′ = yσ_{s}σ′ für alle Variablen y.

Fall 1 y ∈ {x_{1}, …, x_{n}}

x_{i}σ′ \underbrace{=}_{denn σ′∈U(S)} t_{i}σ′ = \underbrace{x_{i}σ_{S}σ′}_{t_{i}}

Fall 2 y ∉ {x_{1}, …, x_{n}}

yσ′ = \underbrace{Y σ_{S}σ′}_{y}

Definition 5.1.7: Transformation von Unifikationsproblemen Wir definieren folgende Relation ⇒ auf Unifikationsproblemen durch 4 Transformationsregeln:

• Löschen: S \underbrace{⊎}_{disjunkte Vereinigung} \{t =^{?} t\} ⇒ S

• Termreduktion: S⊎{f(s_{1}, …, s_{n}) =^{?} f(t_{1}, …, t_{n})} ⇒ S∪{s_{1} =^{?} t_{1}, …, s_{n} =^{?} t_{n}} • Vertauschen: S ⊎ {t =^{?} x} ⇒ S ∪ {x =^{?} t}, falls t ∉ V

• Variablenreduktion: S ⊎ {x =^{?} t} ⇒ {uσ =^{?} vσ für die gilt u =^{?} v ∈ S} ∪ {x =^{?} t}, falls σ = {x/t}, x ∉ V(t), x ∈ V(S)

[09.07.04]

• mgu ist bis auf Variablenumbennenung eindeutig

• Falls σ mgu von S ist, dann U(S) = {σδ|δ ∈ SUB(σ, V)}

• lösen von Unifikationsproblemen S ⇒ S_{1} ⇒ S_{2} ⇒ … ⇒ S_{n}

• Unifikationsproblem S in glöster Form: S = {x_{1} =^{?} t_{k}} x_{1}, …, x_{k} paarweise verschieden, X_{i} ∉ V(t_{0}) für alle i, j mgu ist σ_{S} = {x_{1}/t_{1}, …, x_{k}/t_{k}}

Beispiel 5.1.8: Folie Bsp. für unlösbare Unifikationsprobleme {x =^{?} f(x)}, denn xσ ≠ f(xσ) für alle Substitutionen σ OCCUR FAILURE {g(x) =^{?} g(x)}, denn f(xσ) ≠ g(yσ) für alle Substitutionen σ CLASH FAILU-RE

Unifikationsalgorithmus UNIFY (Robinson 1969, Martell und Montenau 1982 ˆ= unserer Formulierung) Eingabe: Unifikationsproblem S Ausgabe: mgu von S, falls S lösbar ist, sonst “False“ (es existieren Unifikationsalgorithmen mit linearem Aufwand (unserer ist exponentiell))

Satz 5.1.9: Korrektheit des Unifikationsalgorithmus Sei S ein Unifikationsproblem

a) Die Relation ⇒ ist fundiert (↷ UNIFY terminiert)

b) Falls S ⇒ S′, dann gilt U(S) = U(S′) (Menge der Unifikatoren des letzten Problems sind die Unifikatoren des ersten Problems)

c) Falls S lösbar ist und in Normalform bzgl. ⇒ ist, dann ist S in gelöster Form (Korrektheit von Schritt 2 von UNIFY)

d) Der Algorithmus UNIFY terminiert und ist korrekt

Beweis:

1. Ziel: Finde ein Maß, so dass Unifikationsproblem bei jedem Transformationsschritt kleiner wird

Var x ist gelöst gdw. sie genau einmal in S auftritt und zwar in einer Gleichung x =^{?} t (x ∉ V(t))

Messe drei Maße für Unifikationsprobleme:

n_{1} n_{2} n_{3}
{g(f(a), g(x, x)) =^{?} g(x, g(x, y))} ⇒_{Termred}  2 11 0
{f(a) = x, g(x, x) =^{?} g(x, y)} ⇒_{vertauschen}  2 9 1
{x =^{?} f(a), g(x, x) =^{?} g(x, y)} ⇒_{Variablenred}  2 9 0
{x =^{?} f(a), g(f(a), f(a)) =^{?} g(f(a), y)} ⇒_{Termred} 1 12 0
{x =^{?} f(a), f(a) =^{?} f(a), f(a) =^{?} x} ⇒_{Löschen}  1 10 1
{x =^{?} f(a), f(a) =^{?} y}  1 6 1
n_{1} n_{2} n_{3}
Termreduktion  ≥ >
Vertauschen  ≥ = >
Variablenreduktion >
Löschen  ≥ > =

• n_{1} = Anzahl der Variable in S, die noch nicht gelöst sind

• n_{2} = Anzahl der Zeichen in S, d.h. n_{2} = Σ_{S=^{?}t∈S}|S| + |t|

• n_{3} = Anzahl der Gleichungen t =^{?} x in S mit t ∉ V

Maß für Unifikationsprobleme ist (n_{1}, n_{2}, n_{3}). Dieser 3-Tupel wird bei jedem Transformationsschritt bzgl. (>_{ℕ})_{lex}^{3} kleiner [float Box] Generell {f(x) =^{?} f(a)} ⇒ {x =^{?} a} n_{1} = 1 n_{1} = 0 {a =^{?} x} ⇒ ......... [end box]

2. S ⇒ S′ ↷ U(S) = U(S′). Trivial für die ersten 3 Regeln. Zeige es für Variablenreduktion S ⊎ {x =^{?} t} ⇒ {uσ =^{?} u ∈ S} ∪ {x =^{?} t}, wobei σ = {x/t} σ ist mgu von {x =^{?} t} und für alle Θ mit xΘ = tΘ, gilt Θ = σΘ (Lemma 5.1.6, da {x =^{?} t} in gelöster Form) Θ ∈ U(S ⊎ {x =^{?} t}) gdw xΘ = tΘ und Θ ∈ U(S) gdw xΘ = tΘ und σΘ ∈ U(S) (wegen Θ = σΘ) gdw xΘ = tΘ und uσΘ = vσΘ für alle u =^{?} v ∈ S gdw xΘ = tΘ und Θ ∈ U{uσ =^{?} vσ|u =^{?} v ∈ S}) gdw Θ ∈ U({uσ =^{?} vσ|u =^{?} v ∈ S} ∪ {x =^{?} t})

3. S lösbar ↷ S kann keine Gleichung f() =^{?} g() enthalten

S in Normalform ↷ S kann keine Gleichung f() =^{?} f() enthalten (sonst wäre Termreduktion anwendbar)

Aus s =^{?} t ∈ S folgt also S ∈ V oder t ∈ V

Wäre S ∉ V, dann wäre „Vertauschen“ anwendbar

↷ Aus s =^{?} t ∈ S folgt also s ∈ V. S enthält also nur Gleichungen der Form x =^{?} t. Hierbei x ∉ V(t)

• p = x unmöglich da sonst Löschen anwendbar

• x ∈ V(t), x ≠ t das sonst OCCUR FAILURE, S unlösbar

x tritt auch nirgendwo sonst in S auf (ist gelöst), da sonst „Variablenreduktion“ anwendbar wäre.

⇒ S ist in gelöster Form

4. Terminierung folgt aus (a) S ⇒ S_{1} ⇒ … ⇒ S_{n}

wegen (b) U(S) = U(S_{n}) (Induktion über n, Länge der Transformation.

Falls S lösbar ↷ U(S) = U(S_{n}) ≠ ∅ ↷^{(c)} S_{n} ist in gelöster Form, σ_{S_{n}} ist mgu von S_{n} und

Falls S unlösbar ↷ U(S) = U(S_{n}) = ∅ ↷^{(c)} S_{n} ist nicht in gelöster Form ↷ “false“

Korollar 5.1.10: Unifikationssatz Wenn ein Unifikationsproblem lösbar ist, dann hat es einen mgu

[13.07.04] Effizienz von UNIFY kann verbessert werden, in dem man z.B. abbricht (mit “False“), sobald Gleichungen auftreten, die zur unlösbarkeit des Unifikationsproblems führen: f(…) =^{?} g(…) Clash Failure oder x =^{?} t, x ∈ V(t), x ≠ t Occur Failure Unifikation: s unifiziert t gdw. es existiert σ mit sσ = tσ (z.B. nötig, um logische Programmiersprachen zu implementieren) Matching: s matcht t gdw. es existiert σ mit sσ = t (z.B. nötig, um Termersetzung oder funktionale Programmeirsprachen zu implementieren) Idee für einen Matching Algorithmus: Rufe UNIFY mit s und tΘ auf, wobei Θ alle Variablen x ∈ V(t) durch neue Konstanten c_{x} ersetzt. Falls σ der mgu von s und tΘ ist, so erhält man den Matcher von s und t, in dem man in σ alle c_{x} wieder durch x ersetzt. Algorithmus MATCH(s, t) Eingabe: 2 Terme s, t Ausgabe: Matcher σ mit sσ = t, falls er existiert. Sonst “False“.

1. Sei Θ = {x/c_{x}|x ∈ V(T)}, wobei c_{x} neue Konstanten sind.

2. Berechne UNIFY(s, tΘ)

3. Falls UNIFY “False“ liefert, dann brich ab mit “False“

4. Falls UNIFY {x_{1}/t_{1}, …, x_{n}/t_{n}} liefert, so gib aus {x_{1}/t′_{1}, …, x_{n}/t′_{n}}, wobei t′_{i} aus t_{i} entsteht, indem die Konstanten c_{x} wieder durch x ersetzt werden.

Beispiel 5.1.11: Berechne Matcher von s = g(x, y) und t = g(f(x), x). (s, t sind nicht unifizierbar)

Θ = \{x/c_{x}\}. UNIFY(\underbrace{g(x, y)}_{s}, \underbrace{g(f(c_{x}), c_{x})}_{tΘ}) liefert mgu \{x/f(c_{x}), y/c_{x}\}.

Matcher ist {x/f(x), y/x}

5.2 Lokale Konfluenz und Kritische Paare

Im Allgemeinen: Konfluenz von TESen ist unentscheidbar (aber: bei terminierenden TESen ist Konfluenz entscheidbar) Vorgehen: Weise nicht Konfluenz nach, sonder eine schwächere Eigenschaft: lokale Konfluenz Konfluenz untersucht Indeterminismen nach beliebig vielen Schritten:

\xymatrix{ & P \ar[dl]_{∗} \ar[dr]^{∗} \\ s &  & t}

Lokale Konfluenz untersucht Indeterminismen nach einem Schritt:

\xymatrix{ & P \ar[dl] \ar[dr] \\ s &  & t}

Definition 5.2.1: Eine Relation → auf einer Menge M ist lokal Konfluent gdw. für alle p, s, t ∈ M gilt: Falls p → s und p → t gilt, dann existiert ein q ∈ M mit s →^{∗} q, t →^{∗} q

Lokale Konfluenz ← Konfluenz Aber: Lokale Konfluenz ↛ Konfluenz

Beispiel 5.2.2: R = {b → a, b → c, c → b, c → d} Lokale Konfluenz:

\xymatrix{ & b \ar[dl] \ar[dr] &  &  & c \ar[dl] \ar[dr] \\ a \ar[dr]_{∗} &  & c \ar[dl]^{∗} & b \ar[dr]_{∗} &  & d \ar[dl]^{∗} \\  & a &  &  & d}

R ist lokal konfluent Konfluenz:

\xymatrix{ & b \ar[dl]_{∗} \ar[dr]^{∗} &  &  & c \ar[dl]_{∗} \ar[dr]^{∗} \\ a &  & d & a &  & d}

R ist nicht konfluent Aber bei terminierenden TESen: lokale Konfluenz → Konfluenz

Satz 5.2.3: Diamond Lemma, Satz von Newman, 1942 Sei → eine fundierte Relation über einer Menge M. Dann ist → konfluent gdw. sie lokal konfluent ist. Beweis: “⇒“: trivial “⇐“: Vorraussetzung: → ist lokal Konfluent. Zu zeigen ist die folgende Aussage für alle p ∈ M:

Falls \xymatrix{ & p \ar[dl]_{∗} \ar[dr]^{∗} \\ s & & t} , dann s ↓ t. (d.h. es existiert q mit \xymatrix{s \ar[dr]^{∗} & & t \ar[dl]_{∗} \\ & q} ) (*)

Zeige (*) durch noethersche Induktion über p und verwenden → als Induktionsrelation. ⇐ nur möglich, weil “→“ fundiert ist Für alle p′ mit p → p′ können wir (*) als Induktionshypothese voraussetzen. Sei

\xymatrix{ & p \ar[dl]_{∗} \ar[dr]^{∗} \\ s &  & t}

Fall 1 p = s

\xymatrix{ & p \ar[dl]_{∗} \ar[dr]^{∗} \\ s \ar@{.>}[dr]^{∗} &  & t \ar@{.>}[dl]_{∗} \\  & t}

Fall 2 p = t

\xymatrix{ & p \ar[dl]_{∗} \ar[dr]^{∗} \\ s \ar@{.>}[dr]^{∗} &  & p \ar@{.>}[dl]_{∗} \\  & s}

Fall 3 p ≠ s, p ≠ t Man braucht also mindestens einen Schritt von p zu s und zu t

\xymatrix{ &  & p \ar[dl] \ar[dr] \\  & s′ \ar@{.>}[dl]_{∗} \ar@{.>}[dr]^{∗} &  & t′ \ar@{.>}[dl]_{∗} \ar[dr]^{∗} \\ s \ar@{.>}[dr]^{∗} &  & u \ar@{.>}[dl]_{∗} &  & t \ar@{.>}[ddll]_{∗} \\  & v \ar@{.>}[dr]_{∗} \\  &  & q}

\xymatrix{s′ \ar[dr]^{∗} &  & t′ \ar[dl]_{∗} \\  & u}

weil → lokal konfluent ist

\xymatrix{ & s′ \ar[dl]_{∗} \ar[dr]^{∗} \\ s \ar@{.>}[dr]^{∗} &  & u \ar@{.>}[dl]_{∗} \\  & v}

weil t′ kleiner als p ist bzgl. Induktionsrelation und man daher die Induktionshypothese (*) für s′ benutzen darf

\xymatrix{ & t′ \ar[dl]_{∗} \ar[dr]^{∗} \\ v \ar@{.>}[dr]^{∗} &  & t \ar@{.>}[dl]_{∗} \\  & q}

weil t′ kleiner als p ist bzgl. Induktionsrelation und man daher die Induktionshypothese (*) für t′ benutzen darf

□

Bei terminierenden TESen: Konfluenztest kann lokalisiert werden – betrachte nur noch Indeterminismen nach 1 Schritt. (Lokale) Konfluenz ist bei terminierenden TESen entscheidbar: die meisten dieser Indeterminsimen sind immer zusammenführbar. Es gibt nur endlich viele Indeterminismen, die man tatsächlich für lokale Konfluenz untersuchen muss. Vorgehen: Untersuche alle kritischen Situationen der Art:

\xymatrix{ & p \ar[dl]_{l_{1}→r_{1}} \ar[dr]^{l_{2}→r_{2}} \\ s &  & t}

Analysiere an welchen Stellen von p die Regeln angewendet wurden. l_{1} → r_{1} wird an Stelle π_{1} angewendet, l_{1} → r_{2} wird an Stelle π_{2} angewendet. p hat also folgende Gestalt:

[figure: π_{1}; l_{1}; p; x; y; z; σ_{1}]

P |_{Π_{1}} = l_{1}σ_{1} und s = p[r_{1}σ_{1}]_{Π_{1}} P |_{Π_{2}} = l_{2}σ_{2} und s = p[r_{2}σ_{2}]_{Π_{2}} Betrachte, wie Π_{1} und Π_{2} zueinander liegen und ob durch die Reduktion an Π_{1} der Redex an Π_{2} zerstört werden kann (u. u.) Nur dann sind s, t evtl nicht mehr zusammnführbar.

Fall 1 Π_{1}⊥Π_{2} (d.h. Π_{2} ≱_{ℕ^{∗}} Π_{1}, Π_{1} ≱_{ℕ^{∗}} Π_{2})

[figure: l_{1} → r_{1}; l_{2} → r_{2}; l_{2} → r_{2}; l_{1} → r_{1}; p; π_{1}; π_{2}; l_{1}σ_{1}; l_{2}σ_{2}; s; r_{1}σ_{1}; l_{2}σ_{2}; t; l_{1}σ_{1}; r_{2}σ_{2}; q; r_{1}σ_{1}; r_{2}σ_{2}]

p = p[l_{1}σ_{1}]_{π_{1}}[l_{2}σ_{2}]_{π_{2}} s = p[r_{1}σ_{1}]_{π_{1}}[l_{2}σ_{2}]_{π_{2}} t = p[l_{1}σ_{1}]_{π_{1}}[r_{2}σ_{2}]_{π_{2}} s → q, t → q mit q = p[r_{1}σ_{1}]_{π_{1}}[r_{1}σ_{2}]_{π_{2}} s und t lassen sich also in 1 Schritt zusammenführen. ⇒ muss man nicht untersuchen. Bsp.: f(x, f(y, z))) → f(f(x, y), z) f(x, e) → x f(x, i(x)) → e

\xymatrix{ & f(f(x, i(x)), f(x, e) \ar[dl] \ar[dr] \\ f(e, f(x, e)) \ar[dr] &  & f(f(x, i(x)), x) \ar[dl] \\  & f(e, x)}

π_{1} = 1 π_{2} = 2

π_{1} ↓ π_{2}

[16.07.04]

\xymatrix{ & p \ar[dl]_{l_{1}→r_{1}} \ar[dr]^{l_{2}→r_{2}} \\ s &  & t}

p|_{π_{1}} = l_{1}σ_{1}, s = p[r_{1}σ_{1}]_{π_{1}} p|_{π_{2}} = l_{2}σ_{2}, s = p[r_{2}σ_{2}]_{π_{2}} Untersuche die Fälle, wie sich π_{1} und π_{2} zueinander verhalten.

Fall 1 Dann sind s und t immer zusammenführbar.

\begin{matrix}f(x, f(y, z)) → f(f(x, y), z) & (G1) \\ f(x, e) → x & (G2) \\ f(x, i(x)) → e & (G3) \end{matrix}

\xymatrix{ & f(f(x, i(x)), f(x, e) \ar[dl]_{(G1)} \ar[dr]^{(G2)} \\ f(e, f(x, e)) \ar[dr]^{(G2)} &  & f(f(x, i(x)), x) \ar[dl]_{(G3)} \\  & f(e, x)}

Fall 2 π_{1} liegt über π_{2} (π_{2} ≥_{ℕ^{∗}} π_{1})

[figure: p; π_{1}; π; l_{2}σ_{2}]

π_{2} = π_{1}π (π = E ist möglich)

Anstelle der kritischen Situation

\xymatrix{ & p \ar[dl] \ar[dr] \\ s &  & t}

betrachten wir nun

\xymatrix{ & p|_{π_{1}} \ar[dl] \ar[dr] \\ s|_{π_{1}} &  & t|_{π_{1}}}

Grund: Wenn s|_{π_{1}} und t|_{π_{1}} zusammenführbar sind, dann auch s und t. p|_{π_{1}} = lσ_{1} = l_{1}σ_{1}[l_{2}σ_{2}]_{π} s|_{π_{1}} = rσ_{1} t|_{π_{1}} = l_{a}σ_{1}[r_{2}σ_{2}]_{π} Falls

\xymatrix{s|_{π_{1}} \ar[dr]_{∗} &  & t|_{π_{1}} \ar[dl]^{∗} \\  & q}

dann

\xymatrix{s = p[r_{1}σ_{1}]_{π_{1}} = p[s|_{π_{1}}]_{π_{1}} \ar[dr]_{∗} &  & t = p[r_{2}σ_{2}]_{π_{2}} = p[t|_{π_{1}}]_{π_{1}} \ar[dl]^{∗} \\  & q[q]_{π_{1}}}

Unterscheide danach, wie “tief“ l_{2}σ_{2} in l_{1}σ_{1} liegt. Fall 2.1: l_{2}σ_{2} liegt „im Subsitutionsteil“, d.h. π ∉ Occ(l_{1}), l_{1}|_{π′} = x ∈ V

[figure: x; y; z; π′; π′′; π; l_{2}σ_{2}; σ_{1}; l_{1}σ_{1} :]

π = π′π′′ mit π ∈ Occ(l_{1}), l_{1}|_{π′} = x ∈ V, π′′ = E ist möglich l_{2}σ_{2} = xσ_{1}|_{π′′} Wenn l_{1} die Variable x n-mal enthält, dann tritt l_{2}σ_{2} n-mal in l_{1}σ_{1} auf. ↷ Die Regel l_{2} → r_{2} lässt sich also n-mal auf l_{1}σ_{1} anwenden.

[figure: p|_{π_{1}} = l_{1}σ; x; l_{2}σ_{2}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; s|_{π_{1}} = r_{1}σ_{1}; r_{1}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; t|_{π_{1}}; l_{1}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; l_{2} → r_{2}(mehrfach); l_{2} → r_{2}(mehrfach); r_{1}σ_{1}; r_{1}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; l_{1}σ′; l_{1}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; x; l_{2}σ_{2}; l_{1} → r_{1}]

Wenn r_{1} die Variable x m-mal enthält, dann tritt l_{2}σ_{2} m-mal in r_{1}σ_{1} auf. Daher:

\xymatrix{s_{π_{1}} \ar[dr]_{m-mal l_{2}→r_{2}} &  & t_{π_{1}} \ar[dl]^{(n−1)-mal l_{2}→r_{2}} \\  & r_{1}σ′ ← l_{1}σ′}

wobei σ′ wie σ ist, aber xσ′ = xσ[r_{1}σ_{2}]_{π′′} ⇒ Die Indeterminismen im Fall 2.1. Kann man immer zusammenfassen!

\xymatrix{ & f(f(y, e), i(f(y, e))) \ar[dl]_{(G3)} \ar[dr]^{(G2)} \\ e \ar[d]_{m-mal} &  & f(f(y, e), i(y)) \ar[d]^{(n−1)mal} \\ e &  & f(y, i(y)) \ar[ll]_{(G3)}}

π_{1} = E 5.2. LOKALE KONFLUENZ UND KRITISCHE PAARE 77

π_{2} = 2 1 l_{1} = {x/f(y, e)} l_{2}σ_{2} = f(y, e) r_{2}σ_{2} = y n = 2 m = 0 σ′ = {x/y} Fall 2.2 l_{2}σ_{2} liegt nicht „im Substitutionsteil“, d.h. π ∈ Occ(l_{1}) und l_{1}|_{π} ∉ V

[figure: l_{2}σ_{2}; l_{1}; σ_{1}]

Kritische Überlappung ⇒ dies sind die einzigen Fälle, die man zur Untersuchung der lokalen Konfluenz betrachten muss. Allgemein: Dieser Fall tritt auf, wenn es 2 Regeln l_{1} → r_{1}, l_{2} → r_{2} gibt (l_{1} → r_{1} = l_{2} → r_{2} ist möglich) und es existiert π ∈ Occ(l_{1}) mit l_{1}|_{π} ∉ V mit l_{1}|_{π}σ_{1} = l_{2}σ_{2}. Wenn wir die Variablen von l_{1} → r_{1} und l_{2} → r_{2} so umbenennen, dass sie disjunkt sind, dann muss man untersuchen, ob l_{1}|πσ = l_{2}σ gelten kann. D.h.: Zu jeder linken Seite l_{1}, l_{2} und jedem Nicht-Variablen-Teilterm von l_{1} muss man untersuchen: Sind l_{1}|_{π} und l_{2} unifizierbar? Falls ja, so muss man für den aus l_{1}|_{π}σ = l_{2}σ entstehenden Indeterminismus untersuchen, ob er zusammenführbar ist (σ sei mgu von l_{1}|_{π} und l_{2} sein). D.h.: untersuche, ob r_{1}σ und l_{1}σ[r_{2}σ]_{π} zusammenführbar sind ⇒ es genügt, die Zusammenführbarkeit der (endlich vielen) kritischen Paare zu überprüfen.

\xymatrix{ & l_{1}σ = l_{1}[l_{1}|_{π}]_{π}σ \\  & = l_{1}σ[\underbrace{l_{1}|_{π}σ}_{l_{2}σ}]_{π} \ar@{-->}[dl] \ar@{-->}[dr] \\ r_{1}σ &  & l_{1}σ[r_{2}σ]_{π}}

Fall 3 „π_{2} liegt vor π_{1}“

analog

Definition 5.2.4: Kritisches Paar, Knuth + Bendix, 1970

Sei R ein TES mit l_{1} → r_{1}, l_{2} → r_{2} ∈ R. Hierbei seien die Variablen so umbenannt, dass V(l_{1}) ∩ V(l_{2}) = ∅. Sei π ∈ Occ(l_{1}) mit l_{1}|_{π} ∉ V und sei σ mgu von l_{1}|_{π} und l_{2}. Dann ist ⟨r_{1}σ, l_{1}σ[r_{2}σ]_{π}⟩ ein kritisches Paar von R. Die beiden Regeln l_{1} → r_{1}, l_{2} → r_{2} dürfen bis auf Variablenumbenennung identisch sein. In diesem Fall betrachtet man nur Überlappungen mit π ≠ E. Die Menge der kritischen Paare von R wird mit CP (R) bezeichnet.

Es existieren stets nur endlich viele kritische Paare und CP (R) kann mit Hilfe von UNIFY berechnet werden.

Beispiel 5.2.5: Kritische Paare von {(G1), (G2), (G3)}

• (G1) + (G2): \underbrace{f(x′, e)}_{l_{2}} und \underbrace{f(y, z)}_{l_{1}|_{π}} unif. mit mgu \{x′/y, z/e\}

\xymatrix{ & f(x, f(y, e)) \ar[dl]_{(G1)} \ar[dr]^{(G2)} \\ f(f(x, y), e) \ar[dr]_{(G2)^{∗}} &  & f(x, y) \ar[dl]^{∗} \\  & f(x, y)}

⟨f(f(x, y), e), f(x, y)⟩ • (G1) + (G3): f(x′, i(x′)) und f(y, z) unif. mit mgu {x′/y, z/i(y)}

\xymatrix{ & f(x, f(y, i(y))) \ar[dl]_{(G1)} \ar[dr]^{(G3)} \\ f(f(x, y), i(y)) &  & f(x, e) \ar[d]^{∗} \\  &  & x}

⟨f(f(x, y)i(y)), f(x, e)⟩

nicht zusammenführbar ↷ TES ist nicht konfluent

• (G1) + (G1): f(x′, f(y′, z′)) und f(y, z) unif mit mgu {x′/y, z/f(y′, z′)}

\xymatrix{ & f(x, f(y, f(y′, z′)) \ar[dl]_{(G1)} \ar[dr] \\ f(f(x, y), f(y′, z′)) &  & f(x, f(f(y, y′), z′))}

⟨…, …⟩ ist zusammenführbar

Satz 5.2.6: Kritisches Paar Lemma, Knuth + Bendix, 1970 Sei R ein TES. R ist lokal konfluent gdw. alle seine kritischen Paare zusammenführbar sind. (auch wenn R nicht terminiert) Beweis: siehe vorige Überlegungen, alle Indeterminismen, die keinem kritischen Paar entsprechen, sind zusammenführbar □

Algorithmus CONFLUENCE(R)

1. Berechne CP (R)

2. Falls CP (R) = ∅, gib aus “True“ und brich ab

3. Wähle ⟨s, t⟩ ∈ CP (R)

4. Reduziere s, t zu Normalformen s′, t′

5. Falls s′ ≠ t′, dann gib aus “False“ und brich ab

6. Setze CP (R) = CP (R){⟨s, t⟩}

7. zurück zu 2

[20.07.04]

[Folie] Diamond-Lemma: R lokal konfluent ⇔ R konfluent, falls R terminiert Überprüfung der Konfluenz bei terminierenden TESen:

80 KAPITEL 5. KONFLUENZ VON TERMERSETZUNGSSYSTEMEN

1. Bilde alle Kritischen Paare ⟨s, t⟩

2. Berechne beliebige Normalformen s’ von s, t’ von t.

3. s′ = t′, dann ist das kritische Paar zusammenführbar

4. Falls s′ ≠ t′, dann ist R nicht konfluent

\xymatrix{ & p \ar[dl] \ar[dr] \\ s \ar[d]_{∗} &  & t \ar[d]^{∗} \\ s′ &  & t′}

Satz 5.2.7:

a) Der Algorithmus CONFLUENCE terminiert und ist korrekt

b) Für terminierende TESe ist Konfluenz entscheidbar Beweis:

a) Terminierung, denn UNIFY terminiert, |CP (R)| ist endlich, Berechnung der Normalformen in Schritt 4 terminiert (weil R terminiert), bei jedem Durchlauf der Schritte 2-7 wird CP (R) kleiner. Falls der Algorithmus “True“ ausgibt ↷ alle kritischen Paare zusammenführbar ↷^{Satz 5.3.6 ^{1}} lokale Konfluenz ↷^{Satz 5.2.3 ^{2}} Konfluenz Falls der Algorithmus “True“ ausgibt ↷ so existiert

\xymatrix{ & p \ar[dl] \ar[dr] \\ s \ar[d]_{∗} &  & t \ar[d]^{∗} \\ s′ &  & t′}

d.h. p hat 2 verschiedene Normalformen ↷ R nicht confluent

b) folgt, da CONFLUENCE ein entscheidungsalgorithmus ist □

0Kritische Paar Lemma 0Diamond Lemma

Vervollständigung von Termersetzungssystemen

6.1 grundlegender Vervollständigungsalgorithmus, der anschliessend verbessert wird (6.1) Einsatz für Induktionsbeweise/Programmverifikation (6.3)

6.1 Der grundlegende Vervollständigungsalgorithmus

Beispiel 6.1.1: plus-TES: Durch Richten der Gleichungen entsteht ein terminierendes und konfluentes TES ↷ man bekommt direkt ein Verfahren, um Aussagen über plus zu beweise/widerlegen

Beispiel 6.1.2: Gruppen-TES: Durch Richten der Gleichungen entsteht ein terminierendes TES, das nicht konfluent ist.

Grund: Ein kritisches Paar ⟨\underbrace{f(f(x, y), i(y))}_{f(f(x,y),i(y))}, \underbrace{f(x, e)}_{x}⟩ ist nicht zusammenführ-

bar. Idee: Bei nicht zusammengeführten kritischen Paaren ⟨s, t⟩, wobei s die Normalform s’, t die Normalform t’ hat, ergänze das TES um die Regel s′ → t′ oder t′ → s′ (neues TES soll weiterhin terminieren) R_{0} = {(G1), (G2), (G3)} wird vervollständigt zu:

R_{0} = \{(G1), (G2), (G3), \underbrace{f(f(x, y), i(y)) → x}_{(G4)}\}

R_{1} ist adäquat für Gruppenaxiome (E ⊆↔_{R_{0}}^{∗}⊆↔_{R_{1}}^{∗})

82KAPITEL 6. VERVOLLSTÄNDIGUNG VON TERMERSETZUNGSSYSTEMEN

R_{1} ist korrekt für Gruppenaxiome (R_{1} ⊆↔_{E}^{∗}. Wir wissen: R_{0} ⊆↔_{E}^{∗}. f(f(x, y)i(y) \underbrace{←_{R_{0}}^{∗} … →_{R_{0}}^{∗}}_{↔_{R_{0}}^{∗}} x)

R_{1} terminiert, denn l ≻_{lpos} r für alle l → r ∈ R_{0} und auch für (G4). Die kritischen Paare aus CP (R_{0}) sind mit R_{1} alle zusammenführbar. R_{1} ist trotzdem nicht konfluent, da sich durch die neue Regel (G4) neue kritische Paare ergeben: z.B.:

\xymatrix{ & f(f(x, e), i(e)) \ar[dl]_{(G4)} \ar[dr]^{(G2)} \\ x &  & f(x, i(e))}

neues kritisches Paar, das nicht zusammenführbar ist. Insgesamt entstehen für R_{1} 5 kritische Paare, von denen 4 nicht zusammenführbar sind. ↷ erzeuge daraus 4 neue Regeln (G5)-(G8) (eine davon ist f(x, i(e)) → x). R_{2} = {(G1) − (G8)} etc.

3 Möglichkeiten für das Verhalten dieses Vervollständigungsalgorithmusses: Erfolg, Fehlschlag, Nicht-Terminierung Erfolg: nach endlich vielen Schritten erreicht man ein konfluentes TES Fehlschlag: Bei jeder neue erzeugten Regel s′ → t′ bzw t′ → s′ muss überprüft werden, ob das TES immer noch terminiert. Wenn die bisherigen Regeln mit der Reduktionsordnung ≻ terminierten, dann überprüfe, ob s′ ≻ t′ bzw t′ ≻ s′ ist. Abbruch, falls s′ ≡ t′ mit der bisherigen Reduktionsordnung nicht orientiert werden kann. gegebenenfalls Neustart mit neuer Reduktionsordnung. Verbesserung: Lasse ≻ so unbestimmt wie möglich und lege sie nur dann weiter fest, wenn es zur Orientierung von s′ ≡ t′ nötig ist. Nicht-Terminierung: Scheitern wird “nicht bemerkt“ ⇒ Algorithmus BASIC_COMPLETITION Schritt (1) Richten der Gleichungen in E +2 Schritt (4) Vervollständigungsschritt Danach sind alle kritischen Paare von R_{i} zusammenführbar Schritt (5) Erfolgsfall Alle kritischen Paare von R_{i} waren schon in R_{i} zusammenführbar ↷ R_{i} konfluent 3 Beispiele für Erfolg / Fehlschlag / Nichttterminierung von BASIC_COMPLETITION

Beispiel 6.1.3: Erfolg E = {f(f(x, y), f(y, z)) ≡ y} Zentrales Gruppoid ≻ z.B. rpos Alle kritischen Paare von R_{1} sind zusammenführbar ↷ R_{2} = R_{1}. ↷ Erfolg: R_{1} ist konvergent und äquivalent zu E.

Beispiel 6.1.4: Fehlschlag E = {f(x, g(y, z)) ≡ g(f(x, y), f(x, z)), f(g(x, y), z) = g(f(x, z), f(y, z))} f ist links- und rechtsdistributiv über g Wähle ≻=≻_{rpos} mit f]g 6.1. DER GRUNDLEGENDE VERVOLLSTÄNDIGUNGSALGORITHMUS83

E = {f(x, g(y, z)) → g(f(x, y), f(x, z)), f(g(x, y), z) = g(f(x, z), f(y, z))}

\xymatrix{ & f(g(x, y), g(y′, z′)) \ar[dl]_{(1)} \ar[dr]^{(2)} \\ g(f(g(x, y), y′), f(g(x, y), z′)) &  & g(f(x, g(y′, z′)), f(y, g(y′, z′)) \\ g(g(f(x, y′)f(y, y′)), g(f(x, z′), f(y, z′))) &  & g(g(f(x, z′), f(x, z′)), g(f(y, y′), f(y, z′)))}

Hieraus lässt sich keine terminierende Regel gewinnen, da beide Terme gleich sind, wenn alle Terme gleich instantiiert werden ⇒ Fehlschlag

[20.07.04]

Vervollständigung: Finde ein konvergentes und zu E äquivalentes TES

Beispiel 6.1.5: Nichtterminierung E = {f(g(f(x))) ≡ g(f(x))} “Man darf das äussere f weglassen, wenn ein g zwischen zwei f’s steht“ R_{0} = {f(g(f(x))) → g(f(x))} (≻ beliebiige Simplifikatonsordnung)

\xymatrix{ & f(g(f(g(f(x))))) \ar[dl] \ar[dr] \\ g(f(g(f(x)))) \ar[d] &  & f(g(g(f(x)))) \\ g(g(f(x)))}

R_{1} = {f(g(f(x))) →^{(1)} g(f(x))f(g(g(f)))) →^{(2)} g(g(f(x)))} “Man darf das äussere f weglassen, wenn ein oder zwei g’s zwischen zwei f’s stehen“

\xymatrix{ & f(g(f(g(g(f(x)))))) \ar[dl] \ar[dr] \\ g(f(g(g(f(x))))) \ar[d]_{(1)} &  & f(g(g(g((f(x)))))_{(2)} \\ g(g(g(f(x))))}

f(g(g(f(g(f(x)))))) führt zur selben neuen Regel

\xymatrix{ & f(g(g(f(g(g(f(x))))))) \ar[dl] \ar[dr] \\ g(g(f(g(g(f(x)))))) \ar[d]_{(2)} &  & f(g(g(g(g((f(x))))))_{(2)} \\ g(g(g(g(f(x)))))}

R_{2} = {f(g^{i}(f(x))) → g^{i}(f(x))|1 ≤ i ≤ 4} Vervollständigung kann unendlich oft wiederholt werden ↷ erzeugt eine unendliche Menge von Regeln R_{∞} = {f(g^{i}(f(x))) → g^{i}(f(x))|1 ≤ i}

Selbst wenn der Vervollständigungsalgorithmus nicht terminiert, entsteht ein unendliches, aber konvergentes TES R_{∞}, das äquivalent zu E ist ⇒ Man kann den Vervollständigungsalgorithmus dann immer noch als Semi-Entscheidungsverfahren für das Wortproblem benutzen: Um s ≡_{E} t zu zeigen, kann man wie folgt vorgehen: s ≡_{E} t gdw.

\xymatrix{s \ar[dr]^{∗}_{R_{∞}} &  & t \ar[dl]_{∗}^{R_{∞}} \\  & •}

gdw ein n existiert, so dass

\xymatrix{s \ar[dr]^{∗}_{R_{n}} &  & t \ar[dl]_{∗}^{R_{n}} \\  & •}

Semi-Entscheidungsverfahren: Untersuche, ob s ↓_{R_{0}} t. Wenn ja, gilt s ≡_{E} t. Wenn nein, untersuche s ↓_{R_{1}} t etc

Satz 6.1.6: Sei E ein (endliches) Gleichungssystem, sei ≻ eine Reduktionsordnung.

a) Falls BASIC_COMPLETITION(E, ≻) terminiert und R_{n} als Resultat liefert, dann ist R_{n} ein (endliches) konvergentes TES, das äquivalent zu E ist.

b) Falls BASIC_COMPLETITION(E, ≻) nicht terminiert, dann ist R_{∞} = ∪_{i≥0}R_{i} ein unendliches konvergentes TES, das äquivalent zu E ist

6.2. EIN VERNESSERTER VERVOLLSTÄNDIGUNGSALGORITHMUS 85

(Fall (a): Wir erhalten ein Entscheidungsverfahren für das Wortproblem von E Fall (b): Wir erhalten ein Semi-Entscheidungsverfahren für das Wortproblem von E) Beweis: (Kurzfassung) a) R_{n}endlich: in jedem Schleifendurchlauf kommen nur endlich viele Regeln

dazu

R_{n} terminiert: l > r gilt für alle Regeln

R_{n} konfluent: alle kritischen Paare von R_{n} zusammenführbar (kritische Paar Lemma, Diamond Lemma)

R − n äquivalent zu E: alle kritischen Paare sind „korrekt“ bezüglich E

b) R_{∞} unendlich: in jedem Schleifendurchlauf kommen neue Regeln dazu

R_{∞} konfluent: jedes ⟨s, t⟩ ∈ CP (R_{∞}) ist kritisches Paar von einem R_{n} ↷ in R_{n+1} zusammenführbar.

R_{∞} terminiert: wie (a)

R_{∞} äquivalent zu E: wie (a)

□

Nachteil von BASIC_COMPLETION: Regeln, die man einmal gebildet hat (in einem R_{i}) kann man nicht mehr verändern bzw. löschen ↷ man muss kritische Paare mit all diesen Regeln bilden. → zu aufwendig (und zu schwach) für realistischen Einsatz.

6.2 Ein vernesserter Vervollständigungsalgorithmus

Ziel ist: Wenn man neue Regeln erzeugt, dann sollte man alte Regeln mit Hilfe der neuen Regeln vereinfachen bzw. löschen.

Beispiel 6.2.1: Gruppenbeispiel [Folie]

\begin{matrix}(G5) ein Spezialfall der Tatsache, dassi(e) ≡ e \\ (G6) ein Spezialfall der Tatsache, dassi(e) ≡ e \\ (G7) ist die Erkenntnisi(e) ≡ e \end{matrix}\}

Man kann mit neuen Regeln (G7) alte Regeln vereinfachen

\xymatrix{f(x, i(e)) → x(G5) \ar[d]_{(G7)} \\ f(x, e) \ar[d]_{(G2)} \\ x}

Es entsteht: x ≡ x Triviale Aussagen kann man löschen Vervollständigungsalgorithmus: Sammlung von 6 Transformationsregeln auf Paaren (E, R). E: endliches Gleichungssystem R. endliches TES Transformation beginnt mit (E, ∅) \underbrace{⊢_{c}}_{Überführung durch Anwendern von Transformationsregeln(E,R)⊢_{c}(E′,R′)} … ⊢_{c}

(∅, R). Dann ist R das konvergente, zu E äquivalente TES (unter besonderen Bedingungen) Bei (E, R) ⊢_{c} (E′, R′) ändert sich die Menge der wahren Gleichungen nicht, d.h. ↔_{E∪R}^{∗}=↔_{E′∪R′}^{∗} Intuition: E enthält die Gleichungen, die noch nicht gerichtet wurden R enthält die Gleichungen, die schon nicht gerichtet wurden (als Regeln)

Definition 6.2.2: Transformationsregeln für Vervollständiung Sei E ein Gleichungssystem, R ein TES, ≻ eine Reduktionsordnung. Dann definieren wir folgende Transformationsregeln auf Paaren (E, R) [Folie] (Die ersten 4 Transformationsregeln „entsprechen“ dem grundlegenden Vervollständigungsalgorithmus) (Reduziere-Rechts ist unkritisch für Terminierung: Wenn man mit (E, ∅) startet, dann gilt l ≻ r für alle Regeln l → r ∈ R. D.h.: s ≻ t, t ≻ v ↷ s ≻ v ⇒ Terminierung belibt erhalten. Bei Reduziere-links: u ≻ t ist nicht sichergestellt ↷ anstelle der Regel u → t erzeugt man eine Gelichung u ≡ t, die dann noch orientiert werden muss. Grund für die Einschränkung, dass l nicht mit s → t reduziert werden kann → später Wir schreiben (E, R) ⊢_{c} (E′, R′) falls (E, R) durch eine der Transformationsregeln in (E′, R′) Überführt werden kann.

Beispiel 6.2.3: E = {h(x, y) ≡ f(x), h(x, y) ≡ f(y), g(x, y) ≡ h(x, y), g(x, y) ≡ a}.

(ϵ, R) \underbrace{⊢_{c}^{∗}}_{orientieren} (∅, \{h(x, y) →^{(1)} f(x), h(x, y) →^{(2)} f(y), g(x, y) →^{(3)} h(x, y), g(x, y) →^{(4)} a\})

Generieren: erzeugt f(x) ≡ f(y) aus (1) und (2) (\{f(x) \underbrace{≡}_{kann man nicht zu terminierender Regel orientieren↷BASIC_COMPLETITION scheitert} f(y), h(x, y) ≡

a\}, \underbrace{…}_{wie oben}

Orientieren. überführe h(x, y) ≡ a in h(x, y) → a

Reduziere-rechts ({f(x) ≡ f(y), a ≡^{(1)} f(x), a ≡^{(2)} f(y)} Reduziere-links {g(x, y) → a, h(x, y) → a}) Orientieren: ({f(x) ≡ f(y)}, {f(x)′a, q(x, y) → a, a ≡ f(y), h(x, y) → a}) Lösung: {f(x) → a, q(x, y) → a, h(x, y) → a}. Reduktionsgleichung und Löschen: (∅, {f(x) → a, q(x, y) → a, h(x, y) → a})

[27.07.04] Verbersserte Vervollständigung:

• arbeitet auf Paaren (E, R)

• Start mit (E)

• Erfolg mit (∅, R), R konvergent und äquivalent zu E

Lemma 6.2.4: Sei ≻ die bei der Vervollständigung benutzte Reduktionsordnung. Falls l ≻ r für alle l → r ∈ R und (E, R) ⊢_{c} (E′, R′), dann gilt l′ ≻ r′ für alle l′ → r′ ∈ R′. Beweis: offensichtlich, bei „Reduziere-rechts“ wegen Transitivität von ≻ □

Lemma 6.2.5: Aus (E, R) ⊢_{c} (E′, R′) folgt lras_{E∪R} = lras_{E′∪R′} (Bei (E, ∅) ⊢_{c}^{∗} (∅, R) gilt ↔_{E}^{∗}=↔_{R}^{∗}, d.h. R ist äquivalent zu E) Beweis: einfach

Bei (E, ∅) ⊢_{c}^{∗} (∅, R) ist R nicht unbedingt konfluent:

E = \{a ≡ b, a ≡ c\} (E, ∅) ⊢_{c}^{2}^{orientieren} (∅, \underbrace{\{a¯,a → c\}}_{nicht konfluent})

↷ Transformation führt nur dann zu konfluenten TES, wenn „alle“ kritischen Paare gebildet werden. Mann muss nur vor den Regeln kritische Paare bilden, die irgendwann gebildet werden, und nicht wieder gelöscht werden → „Persistente Regeln“. Definieren dies für endliche und unendliche Transformationsfolgen:

Definition 6.2.6: Persistente Gleichungen und Regeln

• Für eine endliche Folge (E_{0}, R_{0}) ⊢_{c} (E_{1}, R_{1}) ⊢_{c} … ⊢_{c} (E_{n}, R_{n}) definieren wir die persistenten Gleichungen E_{ω} = ϵ_{n} und die persistenten Regeln R_{ω} = R_{n}.

• Für eine unendliche Folge (E_{0}, R_{0}) ⊢_{c} (E_{1}, R_{1}) ⊢_{c} … definieren wir die persistenten Gleichungen E_{ω} = ∪_{i≥0} ∩_{j≥i} E_{j} (die Gleichungen, die in E_{j} mit j ≥ i auftreten) und die persistenten Regeln R_{ω} = ∪_{i≥0} ∩_{j≥i} R_{j}.

Definition 6.2.7: Erfolg und Korrektheit von Vervollständigungsprozeduren

• Eine (endliche oder unendliche) Transformationsfolge ist erfolgreich ((E_{0}, R_{0}) ⊢_{c} (E_{1}, R_{1}) ⊢_{c} …) gdw. E_{ω} = ∅ und R_{ω} ein konvergentes zu E_{0}äquivalentes TES ist.

• Eine Transformationsfolge

Vervollständigungsprozeduren unterscheiden sich in der Strategie zur Anwendung der Transformationsregeln (→ beeinflusst Mächtigkeit und Effizienz).

Aber: Korrektheit sollte garantiert sein.

Definition 6.2.8: Fairness Eine (endliche oder unendliche) Transformationsfolge ist fair ((E_{0}, R_{0}) ⊢_{c} (E_{1}, R_{1}) ⊢_{c} …) gdw. CP (R_{ω}) ⊆ ∪_{i≥0}E_{i}. (d.h. jedes kritische Paar der persistenten Regeln trat mal als Gleichung auf)

Satz 6.2.9: Vervollständigungssatz Jede Vervollständigungsprozedur, bei der jede nicht-fehlschlagende Transformationsfolge fair ist, ist korrekt.

Beispiel 6.2.10: illustiert warum bei Reduziere-Links “s → t“nur dann in “u ≡ t“ überführt werden darf, wenn s →^{l→r} u und l ist mit s → t nicht reduzierbar. Durch kritische-Paar-Bildung entstehen die Regeln: fgf(x) → fg(x) (fgf(x) → fg^{2^{n}}(x) für alle n ≥ 0) fgf(x) → fg^{2}(x) fgf(x) → fg^{4}(x) fgf(x) → fg^{8}(x)

⋮ Zweite Regel kann linke Seite der ersten Regel reduzieren. Erste Regel kann linke Seite der zweiten Regel reduzieren. Ohne Einschränkung bei „Reduziere-links“ könnte man die erste Regel löschen und die zweite behalten. Später: Lösche dritte Regel mit der vierten, lösche vierte Regel mit der fünften, … ⇒ einzige persistente Regel, keine persistenten Gleichungen: g^{2}(x) → g(x). Transformationsfolge ist fair. Aber: Ergebnis (persistente Regeln) ist nicht äquivalent zum ursprünglichen Gleichungssystem.

6.3 Implizite Induktion

Ziel: Verwende den Vervollständingungsalgorithmus für automatische Induktionsbeweise. Motiv: in der Programmverifkation ist man meist nicht daran interessiert, ob E ⊨ s ≡ t gilt (s ≡ t gilt in allen Modellen von E), sondern man möchte nur Gültigkeit von s ≡ t in einem speziellen Modell von E untersuchen.

Beispiel 6.3.1: E-plus-Gleichungen. Untersuche, ob plus(x, s(y)) ≡ s(plus(x, y)) Algebra A = (ℕ, α) mit α_{0} = 0, α_{s}(n) = n + 1, α_{plus}(n, m) = n + m: A ⊨ E, A ⊨ plus(x, s(y)) ≡ s(plus(x, y)) Aber: E ⊭ plus(x, s(y)) ≡ s(plus(x, y)), denn es existieren Modelle B von E mit B ⊭ plus(x, s(y)) ≡ s(plus(x, y)). z.B. B = (ℕ ∪ {□, ♢}, α′) mit α′_{0} = 0, α′_{s}(n) =

\begin{cases}n + 1, & falls n ∈ ℕ \\ ♢, & falls n ∈ \{□, ♢\} \end{cases}

α′_{plus}(n, m) =

\begin{cases}n + m & n, m ∈ ℕ \\ n & n ∈ \{□, ♢\} \\ m & n = 0, m ∈ \{□, ♢\} \\ ♢ & n > 0, m ∈ \{□, ♢\} \end{cases}

B ⊨ E (Übung) B ⊭ plus(x, s(y)) ≡ s(plus(x, y)) Bei Variablenbelegung B mit B(x) = 0

\begin{aligned}I = ℕ ∪ \{□, ♢\}, α′, B) : & I(plus(x, s(y))) = α′_{plus}(□, α′_{s}(0)) = □ \\ & I(s(plus(x, y))) = α′_{s}(\underbrace{α′_{plus}(□, 0)}_{□}) = ♢ \end{aligned}

Programmverifikation: Gilt eine Aussage s ≡ t für alle Belegungen der Variablen mit Datenonjekten (z.B. mit natürlichen Zahlen) Ziel: Untersuche, ob eine Aussage für alle Instatiierungen der Variablen mit Datenobjekten/Grundtermen.

Definition 6.3.2: Induktive Gültigkeit Sei E ein Gleichungssystem über Σ, V und s, t ∈ T (Σ, V), Die Gleichung s ≡ t ist induktiv gültig in E(E ⊨_{I} s ≡ t) gdw. E ⊨ sσ ≡ tσ für alle Substitutionen σ mit σ(x) ∈ T (Σ, V) für alle x ∈ V(s) ∪ V(t).

Beispiel 6.3.3: E-plus-Gleichungen. E ⊨_{I} plus(x, s(y)) ≡ s(plus(x, y)) Beweis: Zeige für alle grundterme t_{1}, t_{2} E ⊨ plus(t_{1}, s(t_{2})) ≡ s(plus(t_{1}, t_{2}))

Leichter Beweis durch strukturelle Induktion über t_{1}. “Explizite“ Induktion: Induktionsrelation, Induktionshypothese, etc. werden explizit gebildet und angewendet. (Automatisierung der expliziten Induktion: APV) Alternative: implizite Induktion: keine direkte Bildung von Induktionshypothese und Induktionsrelation

[30.07.04]

Satz 6.3.4: Konsistenzbeweismethode Sei E ein Gleichungssystem über Σ, V, s, t ∈ T (Σ, V). Dann gilt E ⊨_{I} s ≡ t gdw. für alle Grundterme u, v ∈ T (Σ) mit E ⊭ u ≡ v auch E ∪ {s ≡ t} ⊭ u ≡ v gilt. (d.h. falls E ∪ {s ≡ t} ⊨ u ≡ v dann auch E ⊨ u ≡ v) Beweis: “⇒“ E ⊨_{I} s ≡ t E ∪ {s ≡ t} ⊨ u ≡ v

↷^{Birkhoff} u = u_{0} ↔_{E∪{s≡t}} u_{1} ↔_{E∪{s≡t}} … ↔_{E∪{s≡t}} u_{n} = v

↷^{Ersetze alle Variablen der u_{i} durch Grundterme, ↔_{E∪{s≡t}} stabil} u = uδ = u_{0}δ ↔_{E∪{s≡t}} u_{1}δ ↔_{E∪{s≡t}} … ↔_{E∪{s≡t}} u_{n}δ = vδ = v

↷^{da alle u_{i}δ Grundterme sind} u = uδ = u_{0}δ ↔_{E∪{sσ≡tσ|xσ∈T (Σ für alle x∈V(s)∪V(t)}}

u_{1}δ ↔_{E∪{sσ≡tσ|xσ∈T (Σ für alle x∈V(s)∪V(t)}} u_{2}δ ↔_{E∪{sσ≡tσ|xσ∈T (Σ für alle x∈V(s)∪V(t)}} … ↔_{E∪{sσ≡tσ|xσ∈T (Σ für alle x∈V(s)∪V(t)}} u_{n}δ = v

↷^{Birkhoff} E ∪ {sσ ≡ tσ|xσ ∈ T (Σ für alle x ∈ V(s) ∪ V(t)} ⊨ u ≡ v

↷^{E⊨_{I}s≡t} E ⊨ u ≡ v

“⇐“ E ∪ {s ≡ t} ⊨ u ≡ v ↷ E ⊨ u ≡ v E ⊨_{I} s ≡ t Es gilt: E ∪ {s ≡ t} ⊨ sσ ≡ tσ für alle σ, insbesondere für σ, die Variablen aus s, t mit Grundtermen instatiieren ↷^{Var} E ⊨ sσ ≡ tσ für alle Grundsubstitutionen σ ↷ E ⊨_{I} s ≡ t □

Um Satz 6.3.4 zu automatisieren: Generiere ein konvergentes, zu E äquivalentes TES R. Dann muss man Satz 6.3.4 nicht mehr für alle Grundterme u, v überprüfen, sondern nur für Grundnormalformen von RR NF (R) = {q ↓_{R} |q ∈ T (Σ)} Im plus-Beispiel: NF (R) = {O, s(O), s^{2}(O), …} Satz 6.3.5: Konsistentbeweismethode mit konvergenten TESen Sei E ein Gleichungssystem über Σ, V, sei R ein zu E äquivalentes konvergentes TES, s, t ∈ T (Σ, V). Dann gilt: E ⊨_{I} s ≡ t gdw. für alle q_{1}, q_{2} ∈ NF (R) mit q_{1} ≠ q_{2} auch E ∪ {s ≡ t} ⊭ q_{1} ≡ q_{2} gilt. Beweis: “⇒“ Vorraussetzung: E ⊨_{I} s ≡ t. z.Z.: E ∪ {s ≡ t} ⊭ q_{1} ≡ q_{2} falls q_{1}, q_{2} ∈ NF (R) und q_{1} ≠ q_{2} E ∪ {s ≡ t} ⊨ q_{1} ≡ q_{2} für q_{1}, q_{2} ∈ NF (R)

↷^{Satz 6.3.4} E ⊨ q_{1} ≡ q_{2}

↷^{Rkonvergent und äquivalent zu E} q_{1} ↓_{R} q_{2} (q_{1}, q_{2} sind mit R zusammenführbar) ↷^{q_{1}, q_{2} Normalformen} q_{1} = q_{2} “⇐“ Vorraussetzung: für alle q_{1} ≠ q_{2} ∈ NF (R) gilt E ∪ {s ≡ t} ⊭ q_{1} ≡ q_{2}. z.Z. E ⊨_{I} s ≡ t Annahme: E ⊭_{I} s ≡ t ↷^{Satz 6.3.4} es existieren Grundterme u, v mit E ∪ {s ≡ t} ⊨ u ≡ v, E ⊭ u ≡ v Zeige nun, dass es dann statt u, v auch entsprechende Grundnormalformen q_{1}, q_{2} gibt mit

a) q_{1} ≠ q_{2}

b) E ∪ {s ≡ t} ⊨ q_{1} ≡ q_{2}

Wähle q_{1} = u ↓_{R}, q_{2} = v ↓_{R} (existiert, denn R ist konvergent)

a) q_{1} ≠ q_{2}, sonst u ↓_{R} v ↷ E ⊨ u ≡ v → ⚡ zu (1) b)

\begin{matrix}E ∪ \{s ≡ t\} ⊨ q_{1} ≡ u \\ E ∪ \{s ≡ t\} ⊨ q_{1} ≡ u \end{matrix}\} da R äquivalent zu E wegen (2): E∪\{s ≡ t\} ⊨ q_{1} ≡ q_{2}

□

Problem: Wie erkennt man NF (R)? Lösung: Einschränkung auf TES R bestimmter Gestalt. Vorgehen: Teile Σ in zwei disjunkte Teilmengen auf: Σ^{c}: Konstruktoren, dienen zum Aufbau von Datenstrukturen z.B. O, succ Konstruktorgrundterme ˆ= Datenobjekte Σ^{d}: definierte Funktionssymbole, entsprechen den Algorithmen, z.B. plus Definition 6.3.6: Definitionsprinzip

Sei Σ^{c} ⊆ Σ mit Σ_{0}^{c} ≠ ∅ und |σ^{c}| ≥ 2,

Sei Σ^{d} = Σ\Σ^{c}. Ein TES R über Σ, V genügt dem Definitionsprinzip gdw.

a) für alle l → r ∈ R giltl ∉ T (Σ^{c}, V) (l muss ein def. Funktionssymbol enthalten)

b) für alle f ∈ Σ^{d} und alle t_{1}, t_{2} ∈ T (Σ^{c}) existiert eine Regel l → r ∈ R, so dass l den Term f(t_{1}, …, t_{n}) matcht (d.h. f ist vollständig)

Beispiel 6.3.7:

plus-Beispiel erfüllt Definitions-prinzip für Σ^{c} = {O, succ}, Σ^{d} = {plus}.

Satz 6.3.8: Grundnormalformen bei Definitions-prinzip

Sei R ein TES, das dem Definitionsprinzip genügt. Dann gilt NF (R) = T (Σ^{c})

Beweis: NF (R) ⊆ T (Σ^{c}):

Annahme: q ∈ NF (R), q enthält definiertes Funktionssysmbol

Dann existiert π ∈ Occ(q) mit q|_{π} = f(t_{1}, …, t_{n}) für f ∈ Σ^{d}, t_{1}, …, t_{n} ∈ T (Σ^{c})

Dann ist q|_{π} und damit q keine Normalform wegen Definition 6.3.6 (b)

T (Σ^{c}) ⊆ NF (R): folgt aus Definition 6.3.6 (a)

□

Ziel: überprüfe ob E ∪ {s ≡ t} ⊨ q_{1} ≡ q_{2} für verschiedene Konstruktorgrundterme q_{1}, q_{2} gilt. Falls ja: E ⊭_{I} s ≡ t Falls nein: E ⊨_{I} s ≡ t

Dazu benutze Vervollständigungsalgorithmus und modifiziere ihn so, dass er mit “False“ abbricht, sobald Gleichungen entstehen, aus denen q_{1} ≡ q_{2} für verschiedene Konstruktorgrundterme folgt. Wenn er mit Erfolg terminiert, dann existiert ein zu E ∪{s ≡ t} äquivalentes, konvergentes TES, aus dem q_{1} ≡ q_{2} nicht folgt. Starte hierbei nicht mit (E ∪ {s ≡ t}, ∅), sondern mit (\{s ≡ t\}, \underbrace{R}_{Konvergentes, zu E äquivalentes TES, dass das Definitionsprinzip erfüllt})

Änderungen:

– Orientieren nur noch dann, wenn die entstehende neue Regel links aussen ein definiertes Funktionssysbol hat (⇒ Definitionsprinzip Teil (a) soll erhalten beleiben)

– Zwei neue Transformationsregeln um Inkonsistenzen zu erkennen ∗ Inkonsistenz: c_{1}(…) ≡ c_{2}(…) ↷ verschiedene Konstruktorgrund-

terme wären dann “gleich“ bezüglich E ∪ {s ≡ t}

c(…) ≡ x da es Konstruktoren c′ ≠ c gibt, folgt daraus c(…) ≡ c′(…).

∗ Injektivität: “Orientieren“ behandelt nur noch Gleichungen, bei denen aussen ein definiertes Funktionssymbol steht Injektivität behandelt Fall, dass links und rechts der gleiche Konstruktor steht.

Beispiel 6.3.9:

Starte Induktionsbeweiskalkül mit ({plus(x, s(y)) ≡ s(plus(x, y))}, R)

Da Vervollständigung mit einem konvergenten TES endet und keine Inkonsistenz entdeckt wird: E ⊨_{I} p(…) ≡ s(plus(x, y))

Satz 6.3.10:

Sei E ein Gleichungssystem über Σ, V, R ein zu E äquivalentes, konvergentes TES, dass das Definitionsprinzip erfüllt, s, t ∈ T (Σ, V), Reduktionsordnung ≻. Sei ({s ≡ t}, R) ⊢_{I} … eine faire Transformationsfolgemit dem Induktionsbeweiskalkül. Falls die Ableitung mit “False“ abbricht, gilt E ⊭_{I} s ≡ t. Terminiert die Ableitung mit (∅, R_{ω}), dann gilt E ⊨_{I} s ≡ t.