Informatik: Fixpunkte und eine Semantik für Rekursion
Released by matroid on Di. 25. Mai 2004 14:50:58 [Statistics]
Written by lochi - 5398 x read [Outline] Printable version Printer-friendly version -  Choose language   
Informatik

\(\begingroup\)

Fixpunkte und eine Semantik für Rekursion




In diesem Artikel geht es um ein paar Grundlagen der Fixpunkttheorie für vollständigen Halbordnungen, mit deren Hilfe rekursiven Definitionen eine Semantik gegeben werden kann. Zentrales Konzept ist dabei die Fixpunktiteration.

Eine rekursive Definition braucht dabei dann nicht mehr - wie etwa folgende Definition für die Fakultät - für natürliche Zahlen zu erfolgen.
fac:\IN->\IN\, n->\fdef(1,n=0;n*fac(n-1),n>0)




Inhaltsverzeichnis




Ordnungen, Monotonie und Stetigkeit


Bevor wir richtig loslegen können, brauchen wir eine ganze Menge an
Definitionen, um uns unser Handwerkszeug zu verschaffen:


define(bot,\void\senkrechtauf)
\big\ Definition: Ordnung, kleinstes Element
Eine array(geordnete Menge)__ (M\,<=||) ist eine nichtleere Menge M zusammen mit einer binären Relation <=\ \subseteq\ M\ \cross\ \M, so dass für alle
x\,y\,z\in\ M gilt:
\- Reflexiv:__ x<=x
\- Antisymmetrisch:__ x<=y\and\ y<=x=>x=y
\- Transitiv:__ x<=y\and\ y<=z=>x<=z
<= heißt dann (Halb\-)Ordnung__.

Eine Halbordnung <= ist eine array(totale Ordnung)__, wenn zusätzlich für alle x\,y\in\ M gilt:
\- Konnex__: x<=y\or\ y<=x

Falls ein Element \bot\in\ M (sprich: bottom) existiert, so dass \bot<=x für alle x\in\ M gilt, dann heißt \bot array(kleinstes Element)__ von (M,<=\ ).


In einer totalen Ordnung kann man also jedes Element mit jedem vergleichen, was in einer Halbordnung nicht der Fall sein muss.


\big\ Definition: Kette, kleinste obere Schranke
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Eine nichtleere Teilmenge K\subseteq\ M einer geordneten Menge (M\,<=||) heißt Kette__ von (M\,<=||), falls (K\,<=\ \cut\ K\cross\ K) eine total Ordnung ist.

fix(<=,K))\in\ M heißt array(kleinste obere Schranke)__ von K, wenn gilt:
\- \forall\ k\in\ K:k<=fix(<=,K) und
\- \forall\ s'\in\ M:(\forall\ k\in\ K:k<=s')=>fix(<=,K)<=s'


Eine Kette ist also nichts anderes als eine geordnete Menge, in der jedes Element mit jedem vergleichbar ist. Jede endliche Kette lässt ich als Ungleichungskette darstellen:
k_1<=k_2<=k_3<=...<=k_n|mit|K=menge(k_1\,k_2\,k_3\,...\,k_n)
Die kleinste obere Schranke von K ist dann k_n.

So weit sind diese Begriffe noch wie gewohnt aus anderen Bereichen der Mathematik.


\big\ Definition: vollständige Halbordnung (CPO)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Eine Ordnung (M,<=||) heißt vollständig__ (complete partial order, CPO), wenn jede Kette K von (M,<=||) eine kleinste obere Schranke fix(<=,K)\in\ M besitzt.


Wichtig ist hier, dass diese Vollständigkeit etwas ganz anderes als die gewohnte Vollständigkeit in metrischen Räumen ist, denn:


\big\ Beispiel 1: \IR
Sei M=\IR und <= die gewöhnliche Ordnung auf \IR. Dann ist (\IR\,<=\ ) eine totale Ordnung. Damit ist auch jede Teilmenge K\subseteq\IK eine Kette, also insbesondere zum Beispiel 2|\IN=menge(0\,2\,4\,...)\subset\IR^\inf, die keine obere Schranke besitzt, also insbesondere keine kleinste.
Damit ist (\IR,<=\ ) also nicht vollständig.

Fügen wir aber ein größtes Element \inf\notin\IR hinzu, dann ist \IR^\inf=menge(\inf)\union\IR zusammen mit <=\ ^\inf=\ <=\ \union\ (\IR^\inf\cross menge(\inf)) eine vollständig Totalordnung.

\IR^\inf hat aber kein kleinstes Element.




\big\ Beispiel 2: \calP(A)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Sei A eine beliebige Menge und \calP(A) die Potenzmenge von A. Dann ist (\calP(A),\subseteq\ ) eine geordnete Menge, die nicht total ist. Außerdem hat jede Kette K=menge(k_i\subseteq\ A|i\in\ I)\subseteq\calP(A) von (\calP(A),\subseteq\ ) eine kleinste obere Schranke, nämlich fix(\subseteq,K)=union(k_i,i\in\ I,).
Also ist (\calP(A),\subseteq\ ) vollständig. Außerdem ist die leere Menge \0 das kleinste Element von (\calP(A),\subseteq\ ).
\geo

e(400,200)
xachse(0.13,0.6)
yachse(0.18,0.52)
param(alpha,0,45,1,deg2rad)
param(beta,-45,45,1,deg2rad)
param(gamma,-45,0,1,deg2rad)
kurve(0.1*cos(alpha)+0.1,0.1*sin(alpha)+0.2)
kurve(0.1*(2-cos(alpha))+0.1,0.1*sin(alpha)+0.2)
kurve(0.1*(1.41412-cos(beta))+0.1,0.1*(sin(beta)+1.41412)+0.2)
kurve(0.1*(2-1.41412+cos(beta))+0.1,0.1*(sin(beta)+1.41412)+0.2)
kurve(0.1*cos(gamma)+0.1,0.1*(sin(gamma)+2*1.41412)+0.2)
kurve(0.1*(2-cos(gamma))+0.1,0.1*(sin(gamma)+2*1.41412)+0.2)
print(\0,0.205,0.2)
print(A,0.205,0.50284)

print(\0,0.42,0.2)
print(menge(a),0.31,0.3)
print(menge(b),0.405,0.3)
print(menge(c),0.51,0.3)
print(menge(a\,b),0.295,0.4)
print(menge(a\,c),0.395,0.4)
print(menge(b\,c),0.495,0.4)
print(menge(a\,b\,c),0.38,0.5)
nolabel()
p(0.41,0.21,bot1,hide)
p(0.425,0.21,bot2,hide)
p(0.44,0.21,bot3,hide)
p(0.35,0.27,au,hide)
p(0.425,0.27,bu,hide)
p(0.51,0.27,cu,hide)
p(0.33,0.305,a1,hide)
p(0.35,0.305,a2,hide)
p(0.41,0.305,b1,hide)
p(0.44,0.305,b2,hide)
p(0.51,0.305,c1,hide)
p(0.53,0.305,c2,hide)
p(0.33,0.37,abu1,hide)
p(0.35,0.37,abu2,hide)
p(0.41,0.37,acu1,hide)
p(0.44,0.37,acu2,hide)
p(0.51,0.37,bcu1,hide)
p(0.53,0.37,bcu2,hide)
p(0.35,0.405,ab,hide)
p(0.425,0.405,ac,hide)
p(0.51,0.405,bc,hide)
p(0.41,0.47,abc1,hide)
p(0.425,0.47,abc2,hide)
p(0.44,0.47,abc3,hide)
strecke(bot1,au)
strecke(bot2,bu)
strecke(bot3,cu)
strecke(a1,abu1)
strecke(a2,acu1)
strecke(b1,abu2)
strecke(b2,bcu1)
strecke(c1,acu2)
strecke(c2,bcu2)
strecke(ab,abc1)
strecke(ac,abc2)
strecke(bc,abc3)
\geooff
Anschaulich sieht diese Ordnung so aus, kleinere Elemente sind weiter unten, vergleichbare Elemente liegen auf einem Pfad von oben nach unten.
geoprint()



\big\ Beispiel 3: "Un-Ordnung"
Jede Menge A ist zusammen mit der Identität id_A auf A geordnet. Da Ketten höchstens einelementig sein können, ist id_A vollständig. Wenn A mehr als ein Element hat, dann hat (A,id_A) kein kleinstes Element.




define(bot,\void\senkrechtauf)
\big\ Beispiel 4: Diskrete Ordnung
Eine Ordung (M\,<=\ ) mit kleinstem Element \bot\in\ M ist diskret__, wenn für alle x\,y\in\ M gilt:
x<=y=>x=\void\bot\or\ x=y
Anschaulich sieht eine diskrete Ordung wie im Bild unten aus, wobei
vergleichbare Elemente wieder durch Linien verbunden sind und dabei das größere oben steht.
\geo
ebene(300,100)
xachse(0.18,0.8)
yachse(0.15,0.35)
color(black)
nolabel()
p(0.24,0.29,m1,hide)
p(0.34,0.29,m2,hide)
p(0.43,0.28,m3,hide)
p(0.6,0.3,mn,hide)
p(0.4,0.21,bot1,hide)
p(0.42,0.22,bot2,hide)
p(0.44,0.22,bot3,hide)
p(0.48,0.21,botn,hide)
print(m_1,0.2,0.34)
print(m_2,0.3,0.34)
print(m_3,0.4,0.34)
print(...,0.5,0.34)
print(m_n,0.6,0.34)
print(...,0.7,0.34)
strecke(m1,bot1)
strecke(m2,bot2)
strecke(m3,bot3)
strecke(mn,botn)
print(\bot,0.43,0.21)
\geooff
geoprint()

Eine Kette ist dann eine Teilmenge von M, so dass jedes Element mit jedem verbunden ist. Da so aber nur Ketten mit höchstens zwei Elementen möglich sind, ist jede Kette endlich, d.h., sie hat ein größtes Element und damit auch eine kleinste obere Schranke. Damit ist also jede diskrete Ordnung vollständig.




\big\ Definition: monoton und kettenstetig
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Seien (X,<=\ ) und (Y,\subseteq\ ) geordnete Mengen. Eine Funktion
f:X->Y heißt monoton__, wenn für alle x_1\,x_2\in\ X mit x_1<=x_2 gilt, dass f(x_1)\subseteq\ f(x_2).

Sind (X,<=\ ) und (Y,\subseteq\ ) vollständig und f:X->Y monoton, dann ist f kettenstetig__, falls f(fix(<=,K))=fix(\subseteq,f(K)) gilt.


Intuitiv ist eine Funktion kettenstetig, wenn wir Funktionsanwendung und Supremum (= kleinste obere Schranke der Kette) vertauschen können. Damit die Definition von Kettenstetigkeit aber so überhaupt Sinn macht, muss f(K) eine Kette in Y sein:

Behauptung:__ f(K) ist eine Kette in (Y,\subseteq\ ), falls f:(X,<=\ )->(Y,\subseteq\ ) monoton ist und K eine Kette in X.

Beweis:__
Zu jedem y_1 und y_2\in\ f(K) gibt es x_1 und x_2\in\ K, so dass f(x_1)=y_1 und f(x_2)=y_2. Da K eine Kette ist, gilt x_1<=x_2 oder x_2<=x_1. Damit folgt, dass y_1\subseteq\ y_2 oder y_2\subseteq\ y_1, weil f monoton ist. Damit ist aber f(K) eine Kette.


Zur Veranschaulichung wieder ein paar Beispiele:

\big\ Beispiel 1 (Fortsetzung): \IR^\inf
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Wir betrachten wieder (\IR^\inf,<=^\inf) und nehmen als Funktion
f:\IR^\inf->\IR^\inf\, x->\fdef(floor(x),x\in\IR;\inf,x=\inf)

Es ist leicht zu sehen, dass f monoton ist. Allerdings ist f nicht
kettenstetig: Nehmen wir das rechts offene Intervall I=[0,1), das eine Kette in \IR^\inf ist. Dann ist f(fix(<=,I))=f(1)=1, aber
f(I)=menge(0), also fix(<=,menge(0))=0!=1.

Schauen wir aber eine andere Funktion, zum Beispiel
g:\IR^\inf->\IR^\inf\, x->\fdef(x^3+x+4,x\in\IR;\inf,x=\inf)
dann ist g ebenfalls monoton (da g'(x)=3|x^2+1>0), aber auch
kettenstetig.



define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
\big\ Beispiel 4 (Fortsetzung): Diskrete Ordnung
Wenn (X,<=\ ) diskret ist, dann hat jede Kette höchstens zwei Elemente. Betrachten wir jetzt eine monotone Funktion f:(X,<=\ )->(Y,\subseteq\ ), dann ist f automatisch kettenstetig, denn für einelementige Ketten ist die Bedingung trivialerweise erfüllt und für K={a,b}\subseteq X mit a<=b gilt f(a)\subseteq\ f(b) und damit fix(\subseteq,menge(f(a)\,f(b)))=f(b)=f(fix(<=,K)).

Wenn (Y,<=\ ) auch noch diskret ist, dann ist f genau dann monoton, wenn f das kleinste Element von X auf das kleinste Element von Y abbildet.



\big\ Definition: induzierte Ordnung
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Sind (X,<=\ ) und (Y,\subseteq\ ) CPOs und bezeichne ccm(X,Y) die Menge aller
monotonen und kettenstetigen Funktionen von (X,<=\ ) nach (Y,\subseteq\ ),
dann ist (ccm(X,Y),\sqsubseteq\ ) die von <= und \subseteq\void array(induzierte Halbordnung)__ auf ccm(X,Y) gegeben durch
f\sqsubseteq\ g <=>\forall\ x\in\ X:f(x)\subseteq\ g(x)


\big\ Satz:__ Induzierte Ordnungen sind vollständige Halbordnungen.
Beweis:__
define(mfl,menge(f_\l(x)|\l\in\L))
Es ist leicht nachzurechnen, dass \sqsubseteq eine Ordnung auf ccm(X,Y) ist.

Sei also K=menge(f_i|i\in\ I) eine Kette in (ccm(X,Y),\sqsubseteq). Für x\in\ X sei K(x)=menge(f_i\.(x)|i\in\ I) die Menge der Funktionswerte der Elemente der Kette am Punkt x.

Behauptung:__ K(x) ist eine Kette in (Y,\subseteq\ ).
Für y,z\in\ K(x) gibt es i,j\in\ I mit f_i\.(x)=y und f_j\.(x)=z. Da K eine Kette ist, gilt f_i\sqsubseteq\ f_j oder f_j\sqsubseteq\ f_i, und damit y=f_i\.(x)\subseteq\ f_j\.(x)=z oder z=f_j\.(x)\subseteq\ f_i\.(x)=y.

Setzen wir f:X->Y\, x->fix(\subseteq,K(x)).
Behauptung:__ f ist monoton.
Für x,y\in\ X mit x<=y ist für alle i\in\ I f_i(x)\subseteq\ f_i(y)\subseteq fix(\subseteq,K(y)) und damit ist fix(\subseteq,K(y)) eine obere Schranke von K(x) und
folglich f(x)=fix(\subseteq,K(x))\subseteq fix(\subseteq,K(y))=f(y).


Sei L eine Kette in (X,<=\ ) und L(i)=f_i\.(L) für i\in\ I. Dann ist L(i) eine Kette in (Y,\subseteq\ ) (vgl. oben) und fix(\subseteq,L(i))) existiert mit f_i\.(l)\subseteq fix(\subseteq,L(i))) für alle i\in\ I und l\in\ L.

Behauptung:__ S:=menge(fix(\subseteq,L(i))|i\in\ I) ist eine Kette in (Y,\subseteq\ ).
Sei i,j\in I. Dann gilt f_i\sqsubseteq\ f_j oder f_j\sqsubseteq\ f_i. Nehmen wir den ersten Fall an. Dann ist fix(\subseteq,L(j)) eine obere Schranke von L(i) (da f_i\.(l)\subseteq\ f_j\.(l)\subseteq fix(\subseteq,L(j))) und damit fix(\subseteq,L(i))\subseteq fix(\subseteq,L(j)).


makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Behauptung:__ f ist kettenstetig.
Da S eine Kette ist, wissen wir, dass f_i(l)\subseteq fix(\subseteq,L(i))\subseteq fix(\subseteq,menge(fix(\subseteq,L(i))|i\in\ I))=fix(\subseteq,S) und damit ist fix(\subseteq,S\ ) eine obere Schranke von K(l) für alle l\in\ L, folglich
f(l)=fix(\subseteq,K(l))\subseteq fix(\subseteq,S) und damit ist fix(\subseteq,S) auch eine obere Schranke von f(L). f(L) ist aber wieder eine Kette, da f monoton ist, und damit gilt fix(\subseteq,f(L))\subseteq fix(\subseteq,S).
Analog erhalten wir, dass fix(\subseteq,S)\subseteq fix(\subseteq,f(L)), also folgt
f(fix(\subseteq,L))=fix(\subseteq,f(L)).

Damit ist also f\in ccm(X,Y).

Behauptung:__ f=fix(\sqsubseteq,K)
Es gilt, dass f_i\sqsubseteq\ f für alle i\in\ I, da f_i\.(x)\subseteq fix(\subseteq,K(x)))=f(x) für alle x\in\ X. Sei also g\in ccm(X,Y) mit f_i\sqsubseteq\ g für alle i\in\ I eine obere Schranke von K. Dann gilt f_i\.(x)\subseteq\ g(x) für alle x\in\ X, also f(x)=fix(\subseteq,K(x))\subseteq\ g(x) und damit f\sqsubseteq\ g.



\define(bot,\void\senkrechtauf)
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
Bemerkung:__ Wenn Y ein kleinstes Element \bot_Y hat, dann hat auch ccm(X,Y) ein kleinstes Element \bot:X->Y, x->\bot_Y.



Neben diesem Weg zur Schaffung neuer vollständiger Ordnungen aus alten kann man auch auf Produkten von geordneten Mengen eine Produktordnung über die Komponenten definieren, was aber im Folgenden nicht gebraucht und deshalb übersprungen wird. Dagegen werden wir brauchen, dass alle betrachteten geordneten Mengen ein kleinstes Element haben. Um jeder Ordnung ein kleinstes Element "unterzuschieben", gibt es den Trick des Liftings.


define(bot,\void\senkrechtauf)
\big\ Definition: Lifting
Sei (M,<=\ ) eine geordnete Menge mit \bot\notin\ M. Dann ist (M^\bot\,\void\sqsubseteq ) gegeben durch M^\bot=M\union menge(\bot) und \void\sqsubseteq\ =\ <=\ \union(menge(\bot)\cross\ M^\bot).

Dann ist (M^\bot\,\void\sqsubseteq\ ) eine Halbordnung mit kleinstem Element \bot und, falls (M,<=\ ) vollständig ist, vollständig.



Zur Veranschaulichung wieder ein paar Beispiele:

define(bot,\void\senkrechtauf)
\big\ Beispiel 3 und 4 (Fortsetzung)
Jede Menge A kann zusammen mit der "Un-Ordnung" Identität von Beispiel 3 zu einer diskret geordneten A^\bot erweitert werden - Beispiel 4.
Da (A,id_A\ ) vollständig ist, ist auch A^\bot vollständig.



define(bot,\void\senkrechtauf)
\big\ Beispiel 2 (Fortsetzung): \calP(A)
Aber auch einer geordneten Menge, die schon ein kleinstes Element besitzt, kann ein neues kleinstes Element untergeschoben werden:
(\calP(A),\subseteq) wird zu (\calP(A)^\bot\,\void\sqsubseteq), anschaulich für A=menge(a\,b\,c):
\geo
e(200,200)
xachse(0.25,0.6)
yachse(0.08,0.52)

print(\void\senkrechtauf,0.42,0.1)
print(\0,0.42,0.2)
print(menge(a),0.31,0.3)
print(menge(b),0.405,0.3)
print(menge(c),0.51,0.3)
print(menge(a\,b),0.295,0.4)
print(menge(a\,c),0.395,0.4)
print(menge(b\,c),0.495,0.4)
print(menge(a\,b\,c),0.38,0.5)
nolabel()
p(0.425,0.105,bot,hide)
p(0.425,0.17,botu,hide)
p(0.41,0.21,bot1,hide)
p(0.425,0.21,bot2,hide)
p(0.44,0.21,bot3,hide)
p(0.35,0.27,au,hide)
p(0.425,0.27,bu,hide)
p(0.51,0.27,cu,hide)
p(0.33,0.305,a1,hide)
p(0.35,0.305,a2,hide)
p(0.41,0.305,b1,hide)
p(0.44,0.305,b2,hide)
p(0.51,0.305,c1,hide)
p(0.53,0.305,c2,hide)
p(0.33,0.37,abu1,hide)
p(0.35,0.37,abu2,hide)
p(0.41,0.37,acu1,hide)
p(0.44,0.37,acu2,hide)
p(0.51,0.37,bcu1,hide)
p(0.53,0.37,bcu2,hide)
p(0.35,0.405,ab,hide)
p(0.425,0.405,ac,hide)
p(0.51,0.405,bc,hide)
p(0.41,0.47,abc1,hide)
p(0.425,0.47,abc2,hide)
p(0.44,0.47,abc3,hide)
strecke(bot,botu)
strecke(bot1,au)
strecke(bot2,bu)
strecke(bot3,cu)
strecke(a1,abu1)
strecke(a2,acu1)
strecke(b1,abu2)
strecke(b2,bcu1)
strecke(c1,acu2)
strecke(c2,bcu2)
strecke(ab,abc1)
strecke(ac,abc2)
strecke(bc,abc3)
\geooff
geoprint()



\big\ Beispiel 1 (Fortsetzung): \IR
Vergessen wir die vorgegebene Ordnung <= auf \IR und liften (\IR,id_\IR), dann erhalten wir eine vollständige Ordnung auf \IR mit kleinstem Element, die statt vollständig diskret ist.


Fixpunktiteration


Jetzt endlich haben wir das wesentliche Handwerkszeug beisammen, um das Thema Rekursion anzugehen.


define(bot,\void\senkrechtauf)
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
makro(FixO,Fix_(\ %1)(%2))
\big\ Satz:__ Fixpunktsatz von Tarski
Sei (M,<=\ ) eine vollständig geordnete Menge mit kleinstem Element \bot sowie f\in ccm(M,M) eine monotone und kettenstetige Funktion von M nach M. Dann hat f einen kleinsten Fixpunkt FixO(\sqsubseteq,f)=fix(<=,menge(f^n\.(\bot)|n\in\IN)), wobei
f^n\.(\bot) die n-malige Funktionsanwendung von f auf \bot ist (mit f^0=id_M).

Beweis:__
Seien (M,\sqsubseteq\ ), \bot und f wie oben.
Behauptung:__ FixO(\sqsubseteq,f) ist wohldefiniert.
Wir zeigen mittels Induktion über n\in\IN, dass f^n\.(\bot)<=f^(n+1)\.(\bot).
array(n=0:)__ f^0(\bot)=\bot<=f^1(\bot), da \bot das kleinste Element von M ist.
array(n->n+1:)__ Angenommen, f^n(\bot)<=f^(n+1)\.(\bot) für festes n\in\IN. Dann gilt: f^(n+1)(\bot)=f(f^n(\bot)). Da f monoton ist, folgt mit der Annahme, dass f(f^n(\bot))<=f(f^(n+1)(\bot))=f^(n+2)(\bot).
Aus der Transitivität von <= folgt, dass menge(f^n\.(\bot)|n\in\IN) eine Kette in (M,\sqsubseteq\ ) ist.

Behauptung:__ FixO(\sqsubseteq,f) ist ein Fixpunkt von f.
\mixoff\align
f(FixO(\sqsubseteq,f))=f(fix(<=,menge(f^n\.(\bot)|n\in\IN)))=
da|f|kettenstetig|ist
=fix(<=,f(menge(f^n\.(\bot)|n\in\IN)))=
=fix(<=,menge(f^(n+1)\.(\bot)|n\in\IN))=
da|f^0(\bot)=\bot|und|\bot<=f(\bot)
=fix(<=,menge(f^n\.(\bot)|n\in\IN))=FixO(\sqsubseteq,f)


Behauptung:__ FixO(\sqsubseteq,f) ist kleinster Fixpunkt von f.
Sei x\in\ M ein Fixpunkt von f. Dann gilt f(x)=x und \bot<=x, und damit folgt wegen der Monotonie von f: f^n(\bot)<=f(x)=x für alle n\in\IN. x ist also eine obere Schranke von menge(f^n\.(\bot)|n\in\IN) und damit FixO(\sqsubseteq,f)=fix(<=,menge(f^n\.(\bot)|n\in\IN))\sqsubseteq x.



define(bot,\void\senkrechtauf)
array(Bemerkung 1:)__ Die wiederholte Anwendung von f auf \bot bezeichnet man als vec(Fixpunktiteration). Wenn wir einen Fixpunkt von f berechnen wollen, genügt es, f so lange auf \bot anzuwenden, bis f^n\.(\bot)=f^(n-1)\.(\bot) gilt.

array(Bemerkung 2:)__ Für die Existenz eines kleinsten Fixpunkts von f reicht bereits die Monotonie von f aus, zur Konstruktion mittels der Fixpunkt-
iteration ist aber die Kettenstetigkeit notwendig.


Doch was hat das alles mit Rekursionen zu tun? Angenommen, wir haben eine rekursive Definition à la
x=f(x)#,
wobei wir wissen, dass x aus einer bestimmten Menge X ist. Es ist gut möglich, dass viele verschiedene x die Rekursionsgleichung erfüllen. Wenn zum Beispiel f(x)=x gilt, dann haben wir x=x, was immer wahr ist.
Welches x sollen wir also wählen?
Hier können wir jetzt x als Parameter auffassen und eine Funktion
F:X->X\, x->f(x)
definieren, deren Fixpunkte genau die Lösungen der rekursiven Definition sind. Dasjenige x, das der kleinste Fixpunkt von F ist, soll dann mit der Definition x=f(x) gemeint sein. Damit dieser jedoch existiert, muss F monoton und kettenstetig sein.

Zuerst mal wieder zwei Beispiele:

define(bot,\void\senkrechtauf)
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
makro(FixO,Fix_(\ %1)(%2))
\big\ Beispiel 5: Fakultät
Sei f: ccm(\IN^\bot,\IN^\bot), n->fdef(\bot,n=\bot;1,n=0;n*f(n-1),sonst) mit n*\bot:=\bot.

Das Funktional F ist dann gegeben durch:
F: ccm(\IN^\bot,\IN^\bot)->ccm(\IN^\bot,\IN^\bot),f->(n->fdef(\bot,n=\bot;1,n=0;n*f(n-1),sonst))
In Worten gesagt ist F diejenige Funktion, die eine monotone und
kettenstetige Funktion f aus ccm(\IN^\bot,\IN^\bot) auf die Funktion abbildet, die
das Argument \bot auf \bot, 0 auf 1 und alle anderen n auf das n-fache von dem, auf das n-1 abgebildet wird, abbildet.

Der Einfachheit halber bezeichne \bot auch das kleinste Element von ccm(\IN^\bot,\IN^\bot). Dann ergibt sich folgende Iteration:
\mixoff\align
F^0(\bot)=\bot
F^1(\bot)=F(\bot)=n->fdef(\bot,n=\bot;1,n=0;n*\bot(n-1),sonst)=n->fdef(1,n=0;\bot,sonst)
F^2(\bot)=F(F(\bot))=n->fdef(\bot,n=\bot;1,n=0;n*F(\bot)(n-1),sonst)=
=n->fdef(\bot,n=\bot;1,n=0;n*fdef(1,n-1=0;\bot,n-1!=0),sonst)=n->fdef(1,n=0;1,n=1;\bot,sonst)
F^3(\bot)=F(F^2(\bot))=n->fdef(\bot,n=\bot;1,n=0;n*F^2(\bot)(n-1),sonst)=
=n->fdef(\bot,n=\bot;1,n=0;n*fdef(1,n-1=0;1,n-1=1;\bot,sonst),sonst)=n->fdef(1,n=0;1,n=1;2,n=2;\bot,sonst)
#Allgemein erkennen wir:
F^i(\bot)=F(F^(i-1)(\bot))=n->fdef(\bot,n=\bot;1,n=0;n*F^(i-1)(n-1),sonst)=n->fdef(n!,n#Im Grenzwert:
F^\inf\.(\bot)=n->n!



define(bot,\void\senkrechtauf)
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
makro(FixO,Fix_(\ %1)(%2))
\big\ Beispiel 6: Ulam-Funktion
Die Ulam-Funktion, auch als 3n+1-Funktion oder Collatz-Problem bekannt, lässt sich so auch exakt definieren:
ulam:\IN^\bot->\IN^\bot\,n->fdef(\bot,n=\bot;ulam(n/2),2|\||n;ulam(3|n+1),2\teiltnicht\ n)
Damit ist also der kleinste Fixpunkt von
U: ccm(\IN^\bot,\IN^\bot)->ccm(\IN^\bot,\IN^\bot)\,u->fdef(\bot,n=\bot;u(n/2),2|\||n;u(3|n+1),2\teiltnicht\ n)
gemeint.

Allgemein wird vermutet, dass
FixO(\sqsubseteq,U)=n->fdef(\bot,n=\bot;1,sonst),
aber bewiesen wurde es bis heute noch nicht.



define(bot,\void\senkrechtauf)
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
makro(FixO,Fix_(\ %1)(%2))
\big\ Satz:__ Fix ist monoton und kettenstetig.
Sei (X,<=\ ) eine vollständig geordnete Menge mit kleinstem Element \bot. Dann ist der Fixpunktoperator__ Fix: ccm(X,X)->X\,f->FixO(\sqsubseteq,f) monoton und kettenstetig auf (ccm(X,X),\sqsubseteq\ ).

Beweis:__ Seien f\,g\in\ (ccm(X,X)\,\void\sqsubseteq\ ) mit f\sqsubseteq\ g. Es ist per Induktion über n\in\IN leicht zu zeigen, das für alle n\in\IN gilt: f^n(\bot)<=g^n(\bot). Damit ist fix(<=,menge(g^i(\bot)|i\in\IN)) eine obere Schranke für menge(f^i(\bot)|i\in\IN) und folglich
\mixoff\align
FixO(\sqsubseteq,f)><=fix(<=,menge(f^i(\bot)|i\in\IN))<=
><<=fix(<=,menge(g^i(\bot)|i\in\IN))=FixO(\sqsubseteq,g).
\stopalign
Fix ist also monoton.

Sei K eine Kette in ccm(X,X). Dann gilt:
\mixoff\align\breakalign
FixO(\sqsubseteq,fix(\sqsubseteq,K))><=FixO(\sqsubseteq,fix(\sqsubseteq,menge(f|f\in\ K)))=
><=fix(<=,menge((fix(\sqsubseteq,menge(f|f\in\ K)))^n(\bot)|n\in\IN))
und
fix(<=,FixO(\sqsubseteq,K))><=fix(<=,menge(FixO(\sqsubseteq,f)|f\in\ K))=
><=fix(<=,menge(fix(<=,menge(f^n(\bot)|n\in\IN))|f\in\ K))
\stopalign

FixO(\sqsubseteq,fix(\sqsubseteq,K)) ist dann eine obere Schranke für menge(fix(<=,menge(f^n(\bot)|n\in\IN))|f\in\ K) und damit fix(<=,FixO(\sqsubseteq,K))<=FixO(\sqsubseteq,fix(\sqsubseteq,K)). Entsprechend ist auch fix(<=,FixO(\sqsubseteq,K)) eine obere Schranke für menge((fix(\sqsubseteq,menge(f|f\in\ K)))^n(\bot)|n\in\IN), woraus fix(<=,FixO(\sqsubseteq,K))<=FixO(\sqsubseteq,fix(\sqsubseteq,K)) und damit Gleichheit folgt. Fix ist also auch kettenstetig. Damit ist Fix\in ccm(ccm(X,X),X).


Anwendungsbeispiel


Um zu sehen, dass diese Theorie nicht nur für einfache Beispiele wie die Fakultät funktioniert, will ich hier ein größeres Beispiel angehen. Dabei lasse ich die Mehrzahl der Beweise weg, um die Sache übersichtlich zu halten. Zuerst brauche ich eine neue vollständig geordnete Menge, nämlich die unendlichen Folgen über einem Alphabet.


define(bot,\void\senkrechtauf)
makro(ccm,array(%1->%2)^-)
define(Sup,sup)
makro(fix,\Sup_(\ %1)(%2))
makro(FixO,Fix_(\ %1)(%2))
define(cons,\+)
Wenn \S unser nichtleeres Alphabet ist, dann ist eine Folge in \S eine Abbildung f:\IN^\bot->\S^\bot, wobei f(\bot)=\bot und f(n) das n-te Symbol der Folge darstellt. Die Menge der Folgen in \S ist also ccm(\IN^\bot,\S^\bot).
Auf der Menge aller Folgen können wir das Vorne-Anfügen eines Buchstabens durch \cons und \cons_f definieren: \cons: ccm(\IN^\bot,\S^\bot)->ccm(\S^\bot,ccm(\IN^\bot,\S^\bot)) mit \cons(f)=\cons_f
und \cons_f : \S^\bot->ccm(\IN^\bot,\S^\bot)\, \cons_f(\s)=n->fdef(\bot,n=\bot;\s,n=0;f(n-1),n>0)

Das ganze könnte man zwar auch direkter als eine Funktion von ccm(\IN^\bot,\S^\bot)\cross\S^\bot nach ccm(\IN^\bot,\S^\bot) definieren, aber dafür bräuchten wir die Produktordung, die ich im ersten Abschnitt nur erwähnt habe.

Ebenso können wir die Folge konstruieren, die ohne das erste Folgenglied auskommt, also
tail: ccm(\IN^\bot,\S^\bot)->ccm(\IN^\bot,\S^\bot)\,tail(f)=n->fdef(\bot,n=\bot;f(n+1),n\in\IN).


Eine Funktion g:\S_1^\bot->\S_2^\bot wollen wir jetzt mittels der Funktion map auf alle Elemente einer Liste anwenden. Also:
map: ccm(\S_1^\bot,\S_2^\bot)->ccm(ccm(\IN^\bot,\S_1^\bot),ccm(\IN^\bot,\S_2^\bot)) mit map(g)=map_g und
map_g: ccm(\IN^\bot,\S_1^\bot)->ccm(\IN^\bot,\S_2^\bot)\,
map_g(f)=(\cons(map_g(tail(f))))(g(f(0)))

Die einzige rekursive Definition ist hierbei die von map_g. Betrachten wir also das Funktional MapG von map_g:
MapG: ccm(ccm(\IN^\bot,\S_1^\bot),ccm(\IN^\bot,\S_2^\bot))->ccm(ccm(\IN^\bot,\S_1^\bot),ccm(\IN^\bot,\S_2^\bot))\,
h->(\cons(h(tail(f))))(g(f(0)))


Mit obiger Definition von map_g ist also der kleinste Fixpunkt von MapG gemeint. Schauen wir uns als nächstes die ersten Iterationen an:
\mixoff\breakalign\align
MapG^0(\bot)=\bot
MapG^1(\bot)><=f->(\cons(\bot(tail(f))))(g(f(0)))=
><=f->(\cons(\bot))(g(f(0)))=
><=f->\cons_\bot\.(g(f(0)))=
><=f->(n->fdef(\bot,n=\bot;g(f(0)),n=0;\bot(n-1),n>0))=
><=f->(n->\fdef(\bot,n!=0;g(f(0)),n=0))
MapG^2(\bot)><=f->(\cons(MapG^1(tail(f))))(g(f(0)))=
><=f->(\cons(n->fdef(\bot,n!=0;g(tail(f)(0)),n=0)))(g(f(0)))=
><=f->(n->fdef(\bot,n=\bot;g(f(0)),n=0;(m->fdef(\bot,m!=0;g(tail(f)(0)),m=0))(n+1),n>0))=
><=f->(n->fdef(\bot,n=\bot;g(f(0)),n=0;\bot,n+1!=0;g(tail(f)(0)),n+1=0))=
><=f->(n->fdef(g(f(0)),n=0;g(f(1)),n=1;\bot,sonst))
\stopalign
Weitere Iterationen spare ich mir jetzt hier, da das allgemeine Schema bereits erkennbar ist:
MapG^k(\bot)=f->(n->fdef(g(f(n)),nwas sich auch per Induktion beweisen lässt.


Ausblick


Schön und gut, was soll das ganze jetzt? Eine wichtige Anwendung dieser ganzen Theorie sind moderne funktionale Programmiersprachen wie ML oder Haskell, für die es eine formale Definition der Semantik von Programmkonstrukten (und damit auch von jedem Programm) gibt. Eine mögliche Definition arbeitet dabei genau mit diesen Begriffen von CPO und Fixpunktiteration. Hat man es einmal geschafft, einer Programmiersprache so eine Semantik überzustülpen, werden formale Programmkorrektheitsbeweise möglich. Doch für heute lasse ich es hiermit bewenden, sonst wird die ganze Sache noch undurchdringlicher.

Ein netter Nebeneffekt des ganzen ist, dass mit diesem Werkzeug ein Beweis für die Nichtentscheidbarkeit des Halteproblems geführt werden kann, der nicht auf dem üblichen Diagonalisierungsverfahren aufbaut. Aber auch das sei auf die Zukunft verschoben.

Lochi
\(\endgroup\)
Get link to this article Get link to this article  Printable version Printer-friendly version -  Choose language     Kommentare zeigen Comments  
pdfFür diesen Artikel gibt es keine pdf-Datei


Arbeitsgruppe Alexandria Dieser Artikel ist im Verzeichnis der Arbeitsgruppe Alexandria eingetragen:
: Interessierte Studenten :: Informatik :: Theoretische Informatik :: Fixpunkte :
Fixpunkte und eine Semantik für Rekursion [von lochi]  
Grundlagen der Fixpunkttheorie für vollständige Halbordnungen
[Die Arbeitsgruppe Alexandria katalogisiert die Artikel auf dem Matheplaneten]

 
 
Aufrufzähler 5398
 
Aufrufstatistik des Artikels
Insgesamt 362 externe Seitenaufrufe zwischen 2012.01 und 2021.09 [Anzeigen]
DomainAnzahlProz
http://google.de29180.4%80.4 %
https://google.com298%8 %
http://google.sk71.9%1.9 %
http://google.it61.7%1.7 %
https://www.ecosia.org30.8%0.8 %
https://www.bing.com30.8%0.8 %
https://google.de30.8%0.8 %
http://google.at41.1%1.1 %
https://duckduckgo.com30.8%0.8 %
http://www.bing.com71.9%1.9 %
http://google.com20.6%0.6 %
http://adguard.com10.3%0.3 %
http://search.sweetim.com10.3%0.3 %
https://www.qwant.com10.3%0.3 %
http://search.conduit.com10.3%0.3 %

Häufige Aufrufer in früheren Monaten
Insgesamt 317 häufige Aufrufer [Anzeigen]
DatumAufrufer-URL
2013-2018 (93x)http://google.de/url?sa=t&rct=j&q=
2012-2017 (42x)http://google.de/url?sa=t&rct=j&q=zusammenhang fixpunkttheorie und rekursion ...
201205-05 (31x)http://google.de/url?sa=t&rct=j&q=lifting von kettenvollständigen halbordn...
2020-2021 (27x)https://google.com/
201305-05 (18x)http://google.de/url?sa=t&rct=j&q=semantik fixpunkt
201201-01 (15x)http://google.de/url?sa=t&rct=j&q=fixpunkt rekursion iteration
201211-11 (15x)http://google.de/url?sa=t&rct=j&q=was ist kleinste fixpunkt
2012-2013 (14x)http://google.de/url?sa=t&rct=j&q=rekursion fixpunkt
201406-06 (9x)http://google.de/url?sa=t&rct=j&q=fixpunkt rekursion
201405-05 (8x)http://google.de/url?sa=t&rct=j&q=fixpunktproblem rekursion beispiel
201306-06 (7x)http://google.de/url?sa=t&rct=j&q=größter fixpunkt array
201212-12 (7x)http://google.de/url?sa=t&rct=j&q=fixpunkte der funktion potenzmenge
201505-05 (7x)http://google.sk/url?sa=t&rct=j&q=
201206-06 (7x)http://google.de/url?sa=t&rct=j&q=haskell minimales elemenet menge
201312-12 (6x)http://google.it/url?sa=t&rct=j&q=
201202-02 (6x)http://google.de/url?sa=t&rct=j&q=rekursion fixpunkt haskell
201207-07 (5x)http://google.de/url?sa=t&rct=j&q=rekursionsgleichung fixpunkt

[Top of page]

"Informatik: Fixpunkte und eine Semantik für Rekursion" | 3 Comments
The authors of the comments are responsible for the content.

Re: Fixpunkte und eine Semantik für Rekursion
von: Lavant am: So. 25. Dezember 2005 15:08:37
\(\begingroup\)Hallo, Ich danke dir für diesen Artikel aber wozu brauche ich das ganze Zeug hier überhaupt und wo findet es verwendung? mfg Lavant\(\endgroup\)
 

Re: Fixpunkte und eine Semantik für Rekursion
von: Martin_Infinite am: So. 25. Dezember 2005 15:25:03
\(\begingroup\)Hi Lavant, dies hat lochi im letzten Abschnitt "Ausblick" erläutert, oder nicht? Gruß Martin\(\endgroup\)
 

Re: Fixpunkte und eine Semantik für Rekursion
von: Martin_Infinite am: So. 22. Juli 2007 16:59:45
\(\begingroup\) define(bot,\void\senkrechtauf) makro(ccm,array(%1->%2)^-) auf die monotonie kann man m.E. explizit in der definition von kettenstetigkeit verzichten, weil sie sich implizit mit 2\-elementigen ketten ergibt. ich habe zwei fragen. du wendest den satz von tarski anscheinend auf ccm(\IN^\bot,\IN^\bot) an, aber dies ist doch gar keine vollständige ordnung, jedenfalls wenn man \IN die natürliche ordnung gibt. mit welcher ordnung wird das alphabet \Sigma versehen? \(\endgroup\)
 

 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2021 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]