SS2018 Klausur Aufgabe1 Konfluenz und Terminierung

kritische Paare finden

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

SS2018 Klausur Aufgabe1 Konfluenz und Terminierung
https://prntscr.com/ml7k3p


Zur besseren Lesbarkeit:
Gegeben sei eine ternäre Relation [] , und eine unäre Relation _ . Es sei folgende Signatur gegeben:

1.1. [x,y,z] → [x,z,y]
1.2. [x,y,z] → [ x, y, z ]

Meine Gedanken:
Kritische Paare gibt es hier nicht - nur triviale Substitutionen sind möglich, damit ist es auch lokal konfluent.

Meine Gedanken:
Bzgl.: Polynomordnungen wähle man zb.: P_[] (x,y,z) =x+y+z und P_ (x) = x*x +1 auf der Domäne N_>0 und beweise terminierend.
Terminierend und lokal konfluent bedeutet, das System ist konfluent.

EDIT: Es gibt doch ein kritisches Paar, man kann die linken Seiten von 1.1. in 1.2 einsetzen: Man habe: [x,y,z] und [x’,y’,z’] und substiuiere: x’-> x, y’->y, z’->z.
Auf den neuen Term lassen sich dann die Regeln 1.1 bzw. 1.2 anwenden, liefern aber Terme, die sich nicht zusammenführen lassen. Ergebnis: System immernoch nicht konfluent.


deshalb ist meine Lösung richtig? kannst du anschauen? Danke