Not logged in. · Lost password · Register

nudelsalat
Avatar
Member since Apr 2014
13 posts
Subject: 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.
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
622 posts
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

a + (a + (a + b)) -- Sigma auf alle(?) Variablen anwenden
Das ist korrekt, die Herleitung wäre C(t) sigma = (x + (x + y)) [a/x, (a+b)/y] = a + (a + (a + b)).
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