Not logged in. · Lost password · Register

momo8
Member since May 2015
68 posts
Subject: SS2018 Klausur Aufgabe1 Konfluenz und Terminierung
https://prntscr.com/ml7k3p
Ezekiel15
Ezekiel15
Member since Oct 2015
168 posts
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.
This post was edited 5 times, last on 2019-02-17, 13:27 by Ezekiel15.
momo8
Member since May 2015
68 posts
deshalb ist meine Lösung richtig? kannst du anschauen? Danke
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen