Substitution in der Informatik

Question

In der Informatik Vorlesung stand das hier in den Folien ... ich dachte zuhause ergibt das etwas mehr sinn aber da habe ich mich getäuscht. Alles was blau ist verstehe ich nicht wie es zustande kommt, kann mir das jemand erklären?

Substitution

Q sei logischer Ausdruck, v eine int-Variable und t ein int-Ausdruck.

Q[v/t] : Ist v „ungebunden“, so wird es überall durch t ersetzt.

Normalerweise einfache Textersetzung:

Für Q ≡ x > y, v  ≡ x , t  ≡ x+y :

Q[v/t]  ≡ (x > y)[x/x+y]  ≡ x+y > y

Für Q ≡ x > y, v  ≡ x, t  ≡ x*y+y :

Q[v/t]  ≡ (x > y) [x/x*y+y]  ≡ x*y+y > y

Für Q  ≡ ∃k. elem[k]==x+3, v  ≡ x, t  ≡ x*x

Q[v/t]  ≡ (∃ k. elem[k]==x+3)[x/x*x]  ≡ ∃ k. elem[k]==x*x+3

 Durch Quantoren gebundene Variablen werden nicht ersetzt.

Für Q  ≡ ∃ k. elem[k]==x+3, v ≡ k, t ≡ x*x

Q[v/t]  ≡ (∃ k. elem[k]==x+3)[k/x*x] ≡ ∃ k. elem[k]==x+3

Answer 1

> (x > y)[x/x+y]  ≡ x+y > y

Aus dem Term x > y entsteht durch Ersetzung von x durch x+y der Term x+y > y

> Für Q  ≡ ∃k. elem[k]==x+3

Dass blaue ist durch willkürliche Festlegung seitens des Dozenten zustande gekommen.

Comments

Danke für die Hilfe, ich habe aber noch ein paar fragen bei x / x+y

Ist nicht x durch x gleich 1? 

---

> Ist nicht x durch x gleich 1?

Ja, ist es. Alledings wird der Schrägstrich in diesem Zusammenhang nicht als "geteilt durch"-Zeichen verwendet. Stattdessen bedeutet er "wird ersetzt durch".

---

ah danke, das ergibt jetzt auch alles viel mehr Sinn. 

Ich hätte noch eine frage, hat  x+y > y und x*y+y (in der nächsten Zeile) einen Zusammenhang?

Ich verstehe nicht, wie man auf  x*y+y kommt.

Answer 2

Substitution

Q sei logischer Ausdruck, v eine int-Variable und t ein int-Ausdruck.

Q[v/t] : Ist v „ungebunden“, so wird es überall durch t ersetzt.

Normalerweise einfache Textersetzung: Ab hier gehören immer 2 Zeilen zusammen. Die obere beginnt mit "Für" und gibt dir an, wie Q, v und t festgelegt sind. In der unteren wird der Ausdruck Q explizit hingeschrieben und nach dem zweiten ≡ steht erst das 2. Element der eckigen Klammer und dann das erste "ersetzt". 

Für Q ≡ x > y, v  ≡ x , t  ≡ x+y :

Q[v/t]  ≡ (x > y)[x/x+y]  ≡ x+y > y

Für Q ≡ x > y, v  ≡ x, t  ≡ x*y+y :

Q[v/t]  ≡ (x > y) [x/x*y+y]  ≡ x*y+y > y

Ab hier kommen Quantoren ins Spiel. k wird also nicht ersetzt. D.h. dass der Anfang nach dem zweiten ≡ abzuschreiben ist. Dann kommt das zweite Element der eckigen Klammer. Das ist x*x anstelle von x und dann noch das +3.

Für Q  ≡ ∃k. elem[k]==x+3, v  ≡ x, t  ≡ x*x

Q[v/t]  ≡ (∃ k. elem[k]==x+3)[x/x*x]  ≡ ∃ k. elem[k]==x*x+3

Ich würde aber auch vermuten, dass das eine Privatnotation deines Dozenten ist.