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.
Übungsblatt 4, Übung 1
Hallo, ich bin gerade am Übungen wiederholen, und iwie blick ich trotz Übungsmitschrift und Skript nicht wie ich die Krit Paare bestimmen soll.
https://imgur.com/a/sgXL4Ej meine Mitschrift der Aufgabe
In der Übung haben wir die 4 Regeln Umgeschrieben, dass die Variablen Global unique sind, d.h. x kommt nur in Regel 1 vor in Regel 2 heißt es dann y in R3 dann z usw…
Dann haben wir eine Regel gesucht “die auf Context matched” und haben dann verglichen:
C(t) = Ax “Nein” (Quasi C(t) = Regel 1)
C(t) = C(Dy) (C(t) = Regel 2)
C(t) = B(zw) (R4)
dann wird auf letzeres eingegangen:
C(.) = (.)
t = B(zw) = B(Bu) = L4
sigma = [B/7, u/w]
c(t) = B(Bu)
->(3) A(DB)
->(4) Du
Diese beiden sind dann das kritische Paar
Dann wird noch eine Rechnung C(.) = B*(.) angefangen
Kritischen Paare sind dann L1 → r1 und L2 → r2
Ich blick nicht die Vorgehensweise nicht ganz, Woran erkenne ich denn ob eine Regel “Auf Context Matched”?
Habe auch schon bei Folien von anderen Unis geschaut aber die machen es wieder anders (zumidest soweit ich es meine zu verstehen)
Hat jemand vlt in seiner Übung eine simplere/Verständliche Strategie zum Bestimmen Kritischer Paare gezeigt bekommen?
Oder kann jemand das für mich nochmal für dumme erklären?
Würde mich über eine Antwort freuen
Ich lerne das gerade auch und bin mir daher noch nicht ganz sicher. Ich denke mir auch “Context Matchen” ist gemeint, dass du durch Substitution aus dem Term einer Regel, den Term der anderen Regel erzeugen kannst ( linker Term der Ersetzung ist hier relevant ). Hierbei darf aber die Substitution nicht einen ganzen Term ersetzen, d.h. du darfst eine Variable nicht durch den ganzen linksseitigen Term ersetzen.
In der Aufgabe sähe das mMn. so aus (Notation könnte falsch sein):
Vgl. Regel 1 mit Regel 1: Substitution nicht möglich
Vgl. Regel 1 mit Regel 2: Substitution nicht möglich
Vgl. Regel 1 mit Regel 3: Substitution nicht möglich
Vgl. Regel 1 mit Regel 4: Substitution nicht möglich
Vgl. Regel 2 mit Regel 3: Substitution nicht möglich
Vgl. Regel 2 mit Regel 4: Substitution nicht möglich
Vgl. Regel 3 mit Regel 4: Substitution möglich: Term 3 → Term 4 mit o = [x → B , y → x]
Im Endeffekt ist der Sinn der Aufgabe nur zu lernen, wie man kritische Paare findet und einen allgemeinen Unifikator angibt.
Eine simplere Art welche zu finden, ist zu Raten. Dabei sollte man natürlich ein paar Tricks haben, z.b. nach gleicher Klammerung und nach gleichen Konstanten ausschau halten. Kritische Paare zu sich selbst findet man oft bei Verschachtelten Termen, die man dann einfach ein bisschen weiter Verschachtelt, indem man eine Variable durch eine Funktion ersetzt. Einziges Problem beim Raten: Du kannst dir nicht sicher sein, ob du alle kritischen Paare gefunden hast.
Edit:
die ersten paar nicht möglich substitutionen hab ich deiner Aussage entnommen, dass nur 3 und 4 substitutionen sind. Ich habe dies nicht weiter geprüft
1 „Gefällt mir“