Wohlfundierte Relation auf Herleitungen

dawit
Neuling
Neuling
Beiträge: 5
Registriert: 17. Sep 2015 13:04

Wohlfundierte Relation auf Herleitungen

Beitrag von dawit » 6. Mär 2017 17:58

Hallo,

ich verstehe nicht ganz, warum die in Modul 7, Folie 11 definierte Relation für Com wohlfundiert ist. Existiert hier nicht ein ähnliches Problem wie bei der Strukturellen Induktion, nämlich, dass es bei der while-Schleife nicht unbedingt ein "kleinstes" Element gibt, denn die rwht-Regel könnte ja immer eine direkte Teilherleitung sein, oder?

Viele Grüße
David

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

Re: Wohlfundierte Relation auf Herleitungen

Beitrag von typ » 6. Mär 2017 20:22

Hi,
auf der Folie "Deterministische Berechnung (8)" steht unten etwas dazu, was eventuell helfen könnte
Gruß

dawit
Neuling
Neuling
Beiträge: 5
Registriert: 17. Sep 2015 13:04

Re: Wohlfundierte Relation auf Herleitungen

Beitrag von dawit » 7. Mär 2017 10:41

Aber das sagt doch auch nur, dass es mit der strukturellen Induktion Probleme gibt, aber nicht, warum die Relation auf Herleitungen wohlfundiert ist. Oder übersehe ich was?

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

Re: Wohlfundierte Relation auf Herleitungen

Beitrag von wintermute » 7. Mär 2017 14:21

dawit hat geschrieben:Hallo,

ich verstehe nicht ganz, warum die in Modul 7, Folie 11 definierte Relation für Com wohlfundiert ist. Existiert hier nicht ein ähnliches Problem wie bei der Strukturellen Induktion, nämlich, dass es bei der while-Schleife nicht unbedingt ein "kleinstes" Element gibt, denn die rwht-Regel könnte ja immer eine direkte Teilherleitung sein, oder?

Viele Grüße
David
Das funktioniert, da jede Herleitung nur endlich lang ist. Somit ist die Existenz eines kleinsten Elements garantiert.

dawit
Neuling
Neuling
Beiträge: 5
Registriert: 17. Sep 2015 13:04

Re: Wohlfundierte Relation auf Herleitungen

Beitrag von dawit » 7. Mär 2017 14:47

Ich glaube, mein Problem ist, dass ich nicht verstehe, wieso die Herleitung von while true do skip od endlich ist. Ich kann doch bis in alle Ewigkeit rwht anwenden, oder nicht?

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

Re: Wohlfundierte Relation auf Herleitungen

Beitrag von wintermute » 7. Mär 2017 15:07

dawit hat geschrieben:Ich glaube, mein Problem ist, dass ich nicht verstehe, wieso die Herleitung von while true do skip od endlich ist. Ich kann doch bis in alle Ewigkeit rwht anwenden, oder nicht?
Natürlich ist das möglich, dennoch ist jede Herleitung selbst endlich lang. Um es hoffentlich etwas klarer zu machen: Es lassen sich beliebig lange Herleitungen konstruieren, das heißt für jede natürliche Zahl gibt es eine Herleitung dieser Länge. Dennoch hat jede dieser Herleitungen nur endliche viele Teilherleitungen, genau so wie jede natürliche Zahl auch nur endlich viele Vorgänger hat. Wichtig ist der Unterschied zwischen beliebig lang und unendlich lang.

dawit
Neuling
Neuling
Beiträge: 5
Registriert: 17. Sep 2015 13:04

Re: Wohlfundierte Relation auf Herleitungen

Beitrag von dawit » 7. Mär 2017 15:30

Okay, ich glaube, ich habs begriffen (werde noch ein bisschen drüber nachdenken). Auf jeden Fall Danke!

Antworten

Zurück zu „Archiv“