kann mir jemand den Sinn der Fixpunkttheorie am Beispiel der While-Schleifenabwicklung erklären?
ist das irgendwie ein eigenständiger Teil der Frage zu etwas von Seite 23?
dazu hab ich noch ne Frage:
wieso ist F dort stetig?
Wieso werden durch die Fixpunkttheorie die Probleme (S. 16 "Die Lösung hat folgende Nachteile…") der Schleifenabwicklung gelöst?
dafür müsste man erst mal verstehen, was denn die Probleme von S. 16 sind,
den ersten Nachteil (rechte Seite hängt von sigma ab) sehe ich nicht ein,
da steht doch nicht mehr von sigma als etwa bei der Denotation von 'if b then c_0 else c_1'
der zweite Nachteil scheint mir auch merkwürdig,
wie ist es möglich, dass in Beispiel 1.4 sigma', das ja beliebig sein soll, zum Beispiel x=-4 entspricht?
für mich ist durch die Definition festgelegt, das entweder das richtige Ergebnis rauskommt oder
(in diesem Falle bei sigma', sigma'') eine verkappte Endlosschleife,
die man dummerweise nicht als bottom identifizieren kann (sondern man musss wohl ewig weiterrechnen..),
-> dieses Problem wird durch den Fixpunktsatz gelöst,
hier kommt als Ergebnis dann tatsächlich bottom raus,
wenn man denn den Fixpunkt der Funktion ausrechnet (z.B. per Induktion in Beispiel 1.18)
bei der ursprünglichen Notation von Seite 16 ist ein solches Ausrechnen wohl nicht definiert..
was sagt eigentlich Beispiel 1.5 aus?
Wieso ist im Beispiel 1.18 in der Tabelle so vieles zu Bottom geworden und ist das das Ziel?
bei der oberen Tabelle ist die Funktion die naive ohne Fixpunkt,
links sind die Anfangswerte x_0,y_0 und nach rechts hin stehen in einer Zeile alle Zwischenergebnisse bei
i-maligen anwenden der rekursiven Funktion
unten verwendet man nun die Ergebnisse aus der Fixpunkttheorie,
zwar nicht die tatsächliche Fixpunktfunktion, aber die Kette der Funktionen dahin,
beginnend bei F(bottom) in der Spalte neben den Eingabewerten
(entspricht in etwa 1-malige Anwendung der rekursiven Funktion in obiger Tabelle),
danach F^2(bottom) usw.,
dass dadurch so viele Felder zu Bottom werden liegt an der Definition der Funktionen F^i(bottom)
(auf Seite 24 unten zum Beispiel für F(bottom) genau erklärt)
die Tabelle soll veranschaulichen wieso es möglich ist zu behaupte, dass die tatsächliche while-Denotation
(also die Fixpunktfunktion, der Grenzwert von F^i(bottom) )
für sigma mit x<0 bottom als Funktionswert ausgibt,
das ist das Ziel ;)
der Beweis (durch Induktion) dafür steht schon auf der Seite 25, die Tabelle verdeutlicht dies
(für alle F^i(bottom) ist für sigma mit x<0 das Ergebnis bottom -> auch für den Grenzwert)
