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.
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.
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