Teorema del punto fijo de Kleene

En las áreas matemáticas del orden y la teoría de la red, el teorema del punto fijo de Kleene, que lleva el nombre del matemático estadounidense Stephen Cole Kleene, establece lo siguiente:

Kleene Fixed-Point Theorem. Suppose ()L,⊑ ⊑){displaystyle (L,sqsubseteq)} es un orden parcial completo (dcpo) dirigido con un elemento menos, y dejar f:L→ → L{displaystyle f:Lto L} ser una función Scott-continuous (y por lo tanto monotone). Entonces... f{displaystyle f} tiene un punto menos fijo, que es el supremum de la cadena ascendente de Kleene f.{displaystyle f.}

El ascendente Kleene chain de f es la cadena

⊥ ⊥ ⊑ ⊑ f()⊥ ⊥)⊑ ⊑ f()f()⊥ ⊥))⊑ ⊑ ⋯ ⋯ ⊑ ⊑ fn()⊥ ⊥)⊑ ⊑ ⋯ ⋯ {displaystyle bot sqsubseteq f(bot)sqsubseteq f(bot)sqsubseteq cdots sqsubseteq f^{n}(bot)sqsubseteq cdots }

obtenido iterando f en el elemento menor ⊥ de L. Expresado en una fórmula, el teorema establece que

lfp()f)=Sup(){}fn()⊥ ⊥)▪ ▪ n▪ ▪ N}){displaystyle {textrm {lfp}(f)=supleft{f^{n}(bot)mid nin mathbb {N}right}right)}

Donde lfp{displaystyle {textrm {lfp}} denota el punto menos fijo.

Aunque el teorema del punto fijo de Tarski no considera cómo se pueden calcular los puntos fijos iterando f a partir de alguna semilla (además, pertenece a funciones monótonas en redes completas), este resultado a menudo se atribuye a Alfred Tarski, quien lo demuestra para funciones aditivas., El teorema del punto fijo de Kleene se puede extender a funciones monótonas utilizando iteraciones transfinitas.

Prueba

Primero tenemos que demostrar que la cadena ascendente de Kleene f{displaystyle f} existe en L{displaystyle L.. Para demostrarlo, demostramos lo siguiente:

Lemma. Si L{displaystyle L. es un dcpo con un elemento menos, y f:L→ → L{displaystyle f:Lto L} es Scott-continuous, entonces fn()⊥ ⊥)⊑ ⊑ fn+1()⊥ ⊥),n▪ ▪ N0{displaystyle f^{n}(bot)sqsubseteq f^{n+1}(bot),nin mathbb {N}

Prueba. Utilizamos la inducción:

• Assume n = 0. f0()⊥ ⊥)=⊥ ⊥ ⊑ ⊑ f1()⊥ ⊥),{displaystyle f^{0}(bot)=bot sqsubseteq f^{1}(bot),} desde entonces ⊥ ⊥ {displaystyle bot } es el elemento menos.
• Assume n ' Entonces tenemos que mostrar eso fn()⊥ ⊥)⊑ ⊑ fn+1()⊥ ⊥){displaystyle f^{n}(bot)sqsubseteq f^{n+1}(bot)}. Reorganizando lo que tenemos f()fn− − 1()⊥ ⊥))⊑ ⊑ f()fn()⊥ ⊥)){displaystyle f(f^{n-1}(bot)sqsubseteq f(f^{n}(bot)}. Por suposición inductiva, sabemos que fn− − 1()⊥ ⊥)⊑ ⊑ fn()⊥ ⊥){displaystyle f^{n-1}(bot)sqsubseteq f^{n}(bot)} sostiene, y debido a que f es monotone (propiedad de funciones continuas de Scott), el resultado también tiene.

Como corolario de la Lemma tenemos la siguiente cadena dirigida:

M={}⊥ ⊥,f()⊥ ⊥),f()f()⊥ ⊥)),...... }.{displaystyle mathbb {M} ={botf(bot),f(bot)),ldots }.}

De la definición de un dcpo sigue que M{displaystyle mathbb {M} tiene un supremum, llámalo m.{displaystyle m.} Lo que queda ahora es demostrar que m{displaystyle m} es el punto menos fijo.

Primero, mostramos que m{displaystyle m} es un punto fijo, es decir, eso f()m)=m{displaystyle f(m)=m}. Porque... f{displaystyle f} es Scott-continuous, f()Sup()M))=Sup()f()M)){displaystyle f(sup(mathbb {M})=sup(f(mathbb {M})}, eso es f()m)=Sup()f()M)){displaystyle f(m)=sup(f(mathbb {M})}. También, desde M=f()M)∪ ∪ {}⊥ ⊥ }{displaystyle mathbb {M} =f(mathbb {M})cup {bot } y porque ⊥ ⊥ {displaystyle bot } no tiene influencia en la determinación del supremum que tenemos: Sup()f()M))=Sup()M){displaystyle sup(f(mathbb {M})=sup(mathbb {M})}. De ello se desprende que f()m)=m{displaystyle f(m)=m}, haciendo m{displaystyle m} un punto fijo f{displaystyle f}.

La prueba de que m{displaystyle m} es de hecho mínimo punto fijo se puede hacer mostrando que cualquier elemento en M{displaystyle mathbb {M} es más pequeño que cualquier punto fijo de f{displaystyle f} (porque por propiedad de supremum, si todos los elementos de un conjunto D⊆ ⊆ L{displaystyle Dsubseteq L. son más pequeños que un elemento L{displaystyle L. entonces también Sup()D){displaystyle sup(D)} es más pequeño que ese mismo elemento L{displaystyle L.). Esto se hace por inducción: Assume k{displaystyle k} es un punto fijo f{displaystyle f}. Ahora demostramos por inducción sobre i{displaystyle i} que О О i▪ ▪ N:fi()⊥ ⊥)⊑ ⊑ k{displaystyle forall iin mathbb {N}:f^{i}(bot)sqsubseteq k}. La base de la inducción ()i=0){displaystyle (i=0)} Obviamente sostiene: f0()⊥ ⊥)=⊥ ⊥ ⊑ ⊑ k,{displaystyle f^{0}(bot)=bot sqsubseteq k,} desde entonces ⊥ ⊥ {displaystyle bot } es el elemento menos importante L{displaystyle L.. Como hipótesis de inducción, podemos asumir que fi()⊥ ⊥)⊑ ⊑ k{displaystyle f^{i}(bot)sqsubseteq k}. Ahora hacemos el paso de inducción: De la hipótesis de inducción y la monotónica f{displaystyle f} (de nuevo, implicado por la continuidad de Scott f{displaystyle f}), podemos concluir lo siguiente: fi()⊥ ⊥)⊑ ⊑ k⟹ ⟹ fi+1()⊥ ⊥)⊑ ⊑ f()k).{displaystyle f^{i}(bot)sqsubseteq k~implies ~f^{i+1}(bot)sqsubseteq f(k).} Ahora, por supuesto que k{displaystyle k} es un punto fijo f,{displaystyle f,} sabemos que f()k)=k,{displaystyle f(k)=k,} y de eso obtenemos fi+1()⊥ ⊥)⊑ ⊑ k.{displaystyle f^{i+1}(bot)sqsubseteq k.}