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.
Aufgabe 1.2 der Probeklausur
Sehe ich das richtig das es keine Kritischen Paare gibt, da sich bei dem TES nichts Substituieren lässte egal unter welchen Kontext ? Und folg daraus Konfluenz wenn es keine Kritischen Paare gibt ?
Schonmal danke für die Antworten
Es gibt kritische Paare. Bitte beachten, dass eine Regel auch mit sich selbst kombiniert werden kann!
Beispielsweise in dem Term a ⇑ (b ⇑ (c ⇑ d)) gibt es offensichtlich zwei Möglichkeiten die erste Regel anzuwenden; das Beispiel geht auch mit der zweiten Regel unter Benutzung von ⇓.
Also ich hab mir das mit den kritischen Paaren so gemerkt:Mir muss es gelingen, eine linke Regelseite so zu substituieren, dass sie eine andere komplett beinhaltet. Dabei darf die “andere” auch dieselbe, nur mit umbenannten Variablen, sein.
Konkret würde ich also versuchen, x⇑(y⇑x) in x’⇑(y’⇑x’) unterzubringen. Das geht mittels [x’ → y⇑x, y’ → x]. Bei der 2. Regel verfahre ich ebenso und finde auch genau ein kritisches Paar.
Ist das richtig so, oder gibts noch mehr Möglichkeiten?
Das oben beschriebene Kritische Paar aus ((y⇑x)⇑(x⇑(y⇑x)) und x⇑(y⇑x) kann ich aber nicht zusammenführen. Deswegen ist das System nicht konfluent. Kommt jemand auf gleiche Ergebnis?
Die Definition aus dem Skript finde ich eigentlich recht anschaulich:
Sei l1 → r1, l2 → r2 mit FV(l1) und FV(l2) = ∅.
l1 = C(t) und t ist keine Variable.
o = mgu( t, l2 )
Dann ist ( r1 o, C(r2) o ) ein kritisches Paar.
Die Substitution o = [ x → (y’ ⇑ x’), y → x’] habe ich genauso wie du, allerdings ergibt sich bei mir das kritische Paar
r1 o = (y’ ⇑ x’) ⇑ (x’ ⇓ x’)
C(r2) o = (y’ ⇑ x’) ⇑ ( x’ ⇑ (y’ ⇓ y’) )
Von hier aus führt keine Regel weiter. Also ist das System nicht konfluent.
Wäre cool, wenn jemand überprüfen kann, welches Paar das richtige ist.
Ich habe es so wie du.
Das Gegenbeispiel, das man dann angeben soll, wäre dann also l1o (da man es in zwei unterschiedliche Terme reduzieren kann, die nicht zusammenführbar sind), richtig?
sehe ich genauso wie BreakFast und BTL; als Gegenbeispiel hätte ich halt hingeschrieben l1\sigma, dann 2 Pfeile wie man es unterschiedlich reduzieren kann (am Ende dieser beiden Pfeile stehen dann die beiden Teile des kritischen Paares, also r1\sigma und C(r2)\sigma), und dann andeutungsweise Pfeile mit “hier geht’s nicht weiter”
2 „Gefällt mir“