Konfluenz mit Variable sowohl in Kontext, als auch Substitution

Bachelor Theorie der Programmierung
1

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.

2

Konfluenz mit Variable sowohl in Kontext, als auch Substitution
Hey zusammen,

wenn ich Konfluenz zeigen/widerlegen will und eine Regel der Form

x + (x + y) -> y + x

habe, sprich x sowohl Teil des Kontextes, als auch der Substitution ist, ist das folgende Vorgehen korrekt?

C = x + (.)
Sigma = [a/x, (a+b)/y]

     x + (x + y)  -- ursprüngliche linke Seite
     a + (a + b)  -- Variablen umbenannt
x + (x +    y   ) -- äußere linke Seite
a + (a + (a + b)) -- Sigma auf alle(?) Variablen anwenden

Ist das so richtig? Muss der Kontext dabei zu C = a + (.) substituiert werden - wenn ja, nur bei der Beschreibung der Ersetzungsvorschrift unten oder auch beim Ineinandereinsetzen der zwei linken Seiten oben?

C = a + (.) a + (a + (a + b)) -> a + (b + a) -> keine weitere Regelanwendung möglich, da a != b

C = (.) a + (a + (a + b)) -> (a + b) + a -> keine weitere Regelanwendung möglich

Die Regel/das Termersetzungssystem ist nicht konfluent.

3

Der Kontext bleibt C(.) = x + (.). Laut Definition 2.52 des kritischen Paars im Skript muss gelten, dass l_1 = C(t), sodass t und l_2 unifizierbar. Insbesondere ist bei l_1 = C(t) keine Erwähnung einer Substitution vorhanden, d. h. die Regel muss synktatisch exakt wieder so da stehen.

Die Idee ist, dass du einen Subterm so „verändern“ willst, dass er auf eine andere Regel matcht. Dieses „Verändern“ ist jedoch nur eine Substitution, sodass gleichzeitig auch noch die alte Regel greift. Der Kontext fängt dir ein, wo genau der Subterm in der alten originalen Regel steht. Natürlich musst du die Substitution dann auf C(t) komplett anwenden, sonst wäre nicht gewährleistet, dass die alte Regel noch greift, denn: C(t sigma) → ???, aber C(t) sigma → r_1 sigma per kontextabgeschlosser und stabiler Relation ->.

l_1 sigma = C(t) sigma = C(l_2) sigma -> C(r_2) sigma | v r_1 sigma

Das ist korrekt, die Herleitung wäre C(t) sigma = (x + (x + y)) [a/x, (a+b)/y] = a + (a + (a + b)).