Beweis: while true terminiert nicht (-> neue Übungsaufgabe)

typ
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 5. Nov 2016 19:06

Beweis: while true terminiert nicht (-> neue Übungsaufgabe)

Beitrag von typ » 7. Mär 2017 17:21

Hallo,
per Widerspruchsbeweis wird in den Folien gesagt, dass "while true do skip od" nicht terminiert, da der Zustand nach einem Schleifendurchlauf wieder der selbe ist. Wie würde man Beweisen, dass "while true do c od" nie terminiert? Man kann dann nicht sagen, dass o=o', wodurch man den Widerspruchsbeweis nicht nutzen kann.
Gruß
Zuletzt geändert von typ am 7. Mär 2017 18:31, insgesamt 1-mal geändert.

save_jeff
Neuling
Neuling
Beiträge: 8
Registriert: 24. Nov 2016 10:50

Re: Beweis: while true terminiert nicht

Beitrag von save_jeff » 7. Mär 2017 17:29

- ist H die kürzeste Herleitung für while true do c od
- dann kann der letzte herleitungsschritt nur rwht sein.
- in der prämisse kommt wieder while true do c od vor.
- das ist ein wiederspruch da ja eig H die kürzeste herleitung sein soll

-> daraus folgen wir, dass while true do c od, zustand wertet aus zu zustand' nicht herleitbar ist

typ
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 5. Nov 2016 19:06

Re: Beweis: while true terminiert nicht

Beitrag von typ » 7. Mär 2017 17:41

save_jeff hat geschrieben:- ist H die kürzeste Herleitung für while true do c od
- dann kann der letzte herleitungsschritt nur rwht sein.
- in der prämisse kommt wieder while true do c od vor.
- das ist ein wiederspruch da ja eig H die kürzeste herleitung sein soll

-> daraus folgen wir, dass while true do c od, zustand wertet aus zu zustand' nicht herleitbar ist
Hallo,
reicht das so? Bei dem Schritt ist man auf der Folie "Nichtterminierung (1)" auch gewesen. Danach wurde aber noch sichergestellt, dass o=o'', sodass man dann den gleichen Ausdruck und Zustand in der Prämisse hat. In dem Fall "X:=0;while (X eq 0) do Y:=(Y+1) od" kann man schlecht per widerspruch zeigen, dass c den Zustand nicht so ändert, dass das Programm Terminiert, da man in jedem Schleifen durchlauf einen neuen Zustand hat

save_jeff
Neuling
Neuling
Beiträge: 8
Registriert: 24. Nov 2016 10:50

Re: Beweis: while true terminiert nicht

Beitrag von save_jeff » 7. Mär 2017 17:45

ich kann dir schwer sagen ob das so reicht oder nicht.
aber nicht terminierung muss man denke ich nur für programme beweisen die auch herleitbar sind

typ
Windoof-User
Windoof-User
Beiträge: 32
Registriert: 5. Nov 2016 19:06

Re: Beweis: while true terminiert nicht

Beitrag von typ » 7. Mär 2017 18:25

So ists in den Folien:
BildBild
Wir haben in der Konklusion das gleiche wie in der Prämisse stehen -> Widerspruch, da Wiederholung.

Wir können soweit auswerten:
Bild
Wie man Hinteressiernicht zu true auswertet ist trivial. H1 wird von zustand o zu o'' auswerten mit o!=o'', da r:= von o zu o'' ableitet. Somit haben wir in der Konklusion und Prämisse H2 nicht das gleiche stehen da der while-ausdruck im zustand o so ableitet wir wie es stehen haben aber der while-ausdruck im zustand o'' anders ableiten könnte (rwhf). Es müsste also irgendwie bewiesen werden, dass o[X] = o''[X]. Noch komplizierter scheint es wenn wir "X:=X*1" als c haben :D

wintermute
Erstie
Erstie
Beiträge: 15
Registriert: 6. Jul 2016 13:07

Re: Beweis: while true terminiert nicht

Beitrag von wintermute » 7. Mär 2017 18:38

typ hat geschrieben:Hallo,
per Widerspruchsbeweis wird in den Folien gesagt, dass "while true do skip od" nicht terminiert, da der Zustand nach einem Schleifendurchlauf wieder der selbe ist. Wie würde man Beweisen, dass "while true do c od" nie terminiert? Man kann dann nicht sagen, dass o=o', wodurch man den Widerspruchsbeweis nicht nutzen kann.
Gruß
Hier benötigt man das stärkste Beweismittel, welches wir kennengelernt haben, die Induktion über Herleitungen. Wir wollen zeigen: \(\forall \mathcal{H} \in DER_{\mathcal{C}}:\forall c \in Com: \forall \sigma , \sigma' \in \Sigma: \neg (\mathcal{H} \in DER_{\mathcal{C}}(\langle \text{while true do c od}, \sigma \rangle \rightarrow \sigma'))\)

Den exakten Beweis spare ich mir. Von der Idee her sind die Fälle für alle Regeln außer rwht klar, da diese in einer Herleitung von \(\langle \text{while true do c od}, \sigma \rangle \rightarrow \sigma')\) nicht die letzte Regelanwendung darstellen können. Es bleibt der Fall für rwht. Hier wendet man die Induktionsvoraussetzung auf die Teilherleitung an.

Antworten

Zurück zu „Archiv“