Aufgaben

1. Folie Matrix-Interpretationen: das Verifikations-Problem für das Beispiel.

   Beschreiben Sie möglichst genau die Komponenten des Vektors [w](0, 0, 1)^T für w∈{a, b}^* (Beispiele, allgemein)

   Für Rechnungen mit Matrizen z.B. maxima verwenden.

2. Wenn
   • A = (D_A, > _A,[⋅]_A) eine wfmA kompatibel mit R und schwach kompatibel mit S,
   • und B = (D_B, > _B,[⋅]_B) eine wfmA kompatibel mit S:
   konstruieren Sie eine wfmA mit Universum D_A×D_B, die kompatibel mit R∪S ist.

   Lösungsplan:

   • Operationen: komponentenweise. [f](x, y) = ([f]_A(x),[f]_B(y))
   • Ordnung auf dem Universum angeben (unter welchem Namen kennen Sie diese?),
   • Monotonie und Kompatibilität nachweisen.
3. Für A, B, R, S wie in voriger Aufgabe:

   wenn A und B durch Gewichtsfunktionen g_A, g_B definiert sind, dann gibt es eine Gewichtsfunktion g, die mit R∪S kompatibel ist.

   (also eine kompatible wfmA auf $\mathbb {N}$. Nach voriger Aufgabe gibt es eine solche auf $\mathbb {N}$².)

   Anwenden auf R = {bab→aaba}, S = {a³→b}, g_A = {a $\mapsto$ 1, b $\mapsto$ 3}, g_B = {a $\mapsto$ 1, b $\mapsto$ 0}

4. durch Beispiele illustrieren: wenn SN(→₁) und SN(→₂) und (→₁∪→₂) transitiv, dann SN(→₁∪→₂).

   Beweis ist wohl schwierig

5. (von Hand, evtl. autotool) bestimme wfmAs für
   • {aa→bbb, bb→a}
   • Peano-Multiplikation (Variante A: ohne Additionsregeln, B: mit)
   • {p∧(q₁∨q₂)→(p∧q₁)∨(p∧q₂), (p₁∨p₂)∧q→(p₁∧q)∨(p₂∧q)}.
   Hinweis: Dershowitz: 33 examples.

6. Termination des TRS zur Booleschen Auswertung (vorige Woche)
7. Familien von langen Ableitungen und Terminationsbeweis für die SRS
   • R₁ = {ba→acb, bc→abb}
   • R₂ = {ba→acb, bc→cbb}
   • R₃ = {ba→aab, bc→cbb}
   Hinweis: eines hat doppelt exponentielle Ableitungslängen, eines mehrfach exponentielle, eines ist nichtterminierend.

   Beispiel: einfach exponentielle Ableitungslängen für ba→aab: ∀k : ba^k→^*a^2kb, ∀k : b^ka→^*a^2kb^k.

   Hinweis: jede Regelanwendung verlängert um 1, deswegen u→^kv$\implies$k = | v| - | u|, man muß also die Schritte nicht zählen, sondern nur die Wortlängen vergleichen.

8. Geben Sie ein längen-erhaltendes terminierendes SRS mit exponentiellen Ableitungslängen an. Hinweis: Binärzähler.

   Alphabet und Regelanzahl beliebig. Das SRS möglichst kurz (Summe aller Längen aller Regelseiten)

   (Mit einer Regel geht das nicht. Wenn die terminiert, sind die Ableitungslängen höchstens quadratisch.)

9. für alle o.g. Aufgaben u. die restlichen von voriger Woche

   verwenden Sie die Terminationsbeweiser: AProVE (RWTH Aachen), TTT2 (U Innsbruck), Matchbox https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox. Selbst kompilieren/installieren oder Web-Oberfläche.