Punto fijo mínimo

En informática , el enfoque de semántica denotacional utiliza puntos fijos mínimos para obtener a partir de un texto de programa dado una función matemática correspondiente, llamada su semántica. Para ello, se utiliza un objeto matemático artificial,${\displaystyle \bot }$, se introduce, denotando el valor excepcional "indefinido". Dado, por ejemplo, el tipo de datos del programa int, su contraparte matemática se define como${\displaystyle \mathbb {Z} _{\bot }=\mathbb {Z} \cup \{\bot \};}$ Se convierte en un conjunto parcialmente ordenado definiendo${\displaystyle \bot \sqsubset n}$para cada${\displaystyle n\in \mathbb {Z} }$y permitiendo que dos miembros diferentes${\displaystyle n,m\in \mathbb {Z} }$ser incomparable con respecto a${\displaystyle \sqsubset }$, ver imagen.

La semántica de la definición de un programa int f(int n){...}es alguna función matemática.${\displaystyle f:\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }.}$Si la definición del programa fno termina para alguna entrada n, esto se puede expresar matemáticamente como${\displaystyle f(n)=\bot .}$El conjunto de todas las funciones matemáticas se ordena parcialmente definiendo${\displaystyle f\sqsubseteg g}$si, para cada${\displaystyle n,}$la relación${\displaystyle f(n)\sqsubseteteq g(n)}$se sostiene, es decir, si${\displaystyle f(n)}$está menos definido o es igual a${\displaystyle g(n).}$Por ejemplo, la semántica de la expresión x+x/xestá menos definida que la de x+1, ya que la primera, pero no la segunda, asigna${\displaystyle 0}$a${\displaystyle \bot ,}$y ellos opinan lo contrario.

Dado un texto de programa f, su contraparte matemática se obtiene como el punto fijo mínimo de alguna función que mapea funciones a otras funciones y que se puede obtener mediante una "traducción" f. Por ejemplo, la definición en C.

int fact ( int n ) { if ( n == 0 ) return 1 ; else return n * fact ( n -1 ); }

se traduce a un mapeo

${\displaystyle F:(\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot })\to (\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }),}$definido como${\displaystyle (F(f))(n)={\begin{cases}1&{\text{si }}n=0,\\n\cdot f(n-1)&{\text{si }}n\neq \bot {\text{ y }}n\neq 0,\\\bot &{\text{si }}n=\bot .\\\end{cases}}}$

El mapeo${\displaystyle F}$se define de forma no recursiva, aunque factse definió recursivamente. Bajo ciertas restricciones (véase el teorema del punto fijo de Kleene ), que se cumplen en el ejemplo,${\displaystyle F}$necesariamente tiene un punto fijo mínimo,${\displaystyle \operatorname {fact} }$, eso es${\displaystyle (F(\operatorname {fact} ))(n)=\operatorname {fact} (n)}$a pesar de${\displaystyle n\in \mathbb {Z} _ {\bot }}$. ^{[ 1 ]} Es posible demostrar que

${\displaystyle \operatorname {fact} (n)={\begin{cases}n!&{\text{si }}n\geq 0,\\\bot &{\text{si }}n<0{\text{ o }}n=\bot .\end{cases}}}$

Un punto fijo más grande de${\displaystyle F}$es por ejemplo la función${\displaystyle \operatorname {fact} _{0},}$definido por

${\displaystyle \operatorname {fact} _{0}(n)={\begin{cases}n!&{\text{if }}n\geq 0,\\0&{\text{if }}n<0,\\\bot &{\text{if }}n=\bot ,\end{cases}}}$

Sin embargo, esta función no refleja correctamente el comportamiento del texto del programa anterior para valores negativos.${\displaystyle n;}$Por ejemplo, la llamada fact(-1)no terminará en absoluto, y mucho menos devolverá 0. Solo el punto fijo más pequeño ,${\displaystyle \operatorname {fact} ,}$Puede utilizarse razonablemente como semántica de un programa matemático.

Immerman ^{[ 2 ] [ 3 ]} y Vardi ^{[ 4 ]} demostraron independientemente el resultado de complejidad descriptiva de que las propiedades computables en tiempo polinomial de estructuras linealmente ordenadas se pueden definir en FO(LFP) , es decir, en lógica de primer orden con un operador de punto fijo mínimo. Sin embargo, FO(LFP) es demasiado débil para expresar todas las propiedades en tiempo polinomial de estructuras no ordenadas (por ejemplo, que una estructura tenga un tamaño par ).