Variante de bucle

En informática , una variante de bucle es una función matemática definida en el espacio de estados de un programa informático cuyo valor disminuye monótonamente con respecto a una relación bien fundada (estricta) mediante la iteración de un bucle while bajo ciertas condiciones invariantes , lo que garantiza su terminación . Una variante de bucle cuyo rango está restringido a los números enteros no negativos también se conoce como función límite , porque en este caso proporciona un límite superior trivial en el número de iteraciones de un bucle antes de que finalice. Sin embargo, una variante de bucle puede ser transfinita y, por lo tanto, no está necesariamente restringida a valores enteros.

Una relación bien fundada se caracteriza por la existencia de un elemento mínimo de cada subconjunto no vacío de su dominio. La existencia de una variante prueba la terminación de un bucle while en un programa informático mediante una descendencia bien fundada . ^[1] Una propiedad básica de una relación bien fundada es que no tiene cadenas descendentes infinitas . Por lo tanto, un bucle que posee una variante terminará después de un número finito de iteraciones, siempre que su cuerpo termine cada vez.

Se dice que un bucle while , o, más generalmente, un programa de computadora que puede contener bucles while, es totalmente correcto si es parcialmente correcto y finaliza.

Regla de inferencia para la corrección total

Para enunciar formalmente la regla de inferencia para la terminación de un bucle while que hemos demostrado anteriormente, recordemos que en la lógica Floyd-Hoare , la regla para expresar la corrección parcial de un bucle while es:

${\displaystyle {\frac {\{I\land C\}\;S\;\{I\}}{\{I\}\;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;\{I\land \lnot C\}}},}$

donde I es el invariante , C es la condición y S es el cuerpo del bucle. Para expresar la corrección total, escribimos en cambio:

${\displaystyle {\frac {<{\text{ is well-founded}},\;[I\land C\land V=z]\;S\;[I\land V<z]}{[I]\;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;[I\land \lnot C]}},}$

donde, además, V es la variante , y por convención se toma que el símbolo no ligado z está cuantificado universalmente .

Cada bucle que termina tiene una variante

La existencia de una variante implica que un bucle while termina. Puede parecer sorprendente, pero lo inverso también es cierto, siempre que asumamos el axioma de elección : todo bucle while que termina (dado su invariante) tiene una variante. Para demostrarlo, supongamos que el bucle

${\displaystyle {\mathtt {while}}\;C\;{\mathtt {do}}\;S}$

termina dado el invariante I donde tenemos la afirmación de corrección total

${\displaystyle [I\land C]\;S\;[I].}$

Consideremos la relación "sucesor" en el espacio de estados Σ inducida por la ejecución de la declaración S desde un estado que satisface tanto el invariante I como la condición C . Es decir, decimos que un estado σ′ es un "sucesor" de σ si y sólo si

• I y C son ambas verdaderas en el estado σ , y
• σ′ es el estado que resulta de la ejecución de la sentencia S en el estado σ .

Notamos que de lo contrario el bucle no lograría finalizar. ${\displaystyle \sigma '\neq \sigma ,}$

Consideremos a continuación el cierre reflexivo y transitivo de la relación "sucesor". Llamemos a esto iteración : decimos que un estado σ′ es un iterado de σ si o bien hay una cadena finita tal que y es un "sucesor" de ⁠ ⁠ para todo I , ${\displaystyle \sigma '=\sigma ,}$ ${\displaystyle \sigma _{0},\sigma _{1},\,\dots \,,\sigma _{n}}$ ${\displaystyle \sigma _{0}=\sigma ,}$ ${\displaystyle \sigma _{n}=\sigma '}$ ${\displaystyle \sigma _{i+1}}$ ${\displaystyle \sigma _{i};}$ ${\displaystyle 0\leq i<n.}$

Observamos que si σ y σ′ son dos estados distintos, y σ′ es una iteración de σ , entonces σ no puede ser una iteración de σ′, porque de lo contrario el bucle no terminaría. En otras palabras, la iteración es antisimétrica y, por lo tanto, de orden parcial .

Ahora bien, dado que el bucle while termina después de un número finito de pasos dado el invariante I , y ningún estado tiene un sucesor a menos que I sea verdadero en ese estado, concluimos que cada estado tiene solo un número finito de iteraciones, cada cadena descendente con respecto a la iteración tiene solo un número finito de valores distintos y, por lo tanto, no hay una cadena descendente infinita , es decir, la iteración del bucle satisface la condición de cadena descendente .

Por lo tanto, suponiendo el axioma de elección , la relación "sucesor" que definimos originalmente para el bucle está bien fundada en el espacio de estados Σ , ya que es estricta (irreflexiva) y está contenida en la relación "iterar". Por lo tanto, la función identidad en este espacio de estados es una variante para el bucle while, ya que hemos demostrado que el estado debe decrecer estrictamente (como un "sucesor" y un "iterar") cada vez que se ejecuta el cuerpo S dado el invariante I y la condición C .

Además, podemos demostrar mediante un argumento de conteo que la existencia de cualquier variante implica la existencia de una variante en ω ₁ , el primer ordinal incontable , es decir,

${\displaystyle V:\Sigma \rightarrow \omega _{1}.}$

Esto se debe a que la colección de todos los estados alcanzables por un programa de computadora finito en un número finito de pasos a partir de una entrada finita es contablemente infinita, y ω ₁ es la enumeración de todos los tipos bien ordenados en conjuntos contables.

Consideraciones prácticas

En la práctica, las variantes de bucle se toman a menudo como números enteros no negativos , o incluso se requiere que lo sean, ^[2] pero el requisito de que cada bucle tenga una variante entera elimina el poder expresivo de la iteración ilimitada de un lenguaje de programación. A menos que un lenguaje de este tipo (verificado formalmente) permita una prueba transfinita de terminación para alguna otra construcción igualmente poderosa como una llamada de función recursiva , ya no es capaz de una μ-recursión completa , sino solo de una recursión primitiva . La función de Ackermann es el ejemplo canónico de una función recursiva que no se puede calcular en un bucle con una variante entera .

Sin embargo, en términos de su complejidad computacional , las funciones que no son recursivas primitivas se encuentran mucho más allá del ámbito de lo que generalmente se considera manejable . Considerando incluso el caso simple de la exponenciación como una función recursiva primitiva, y que la composición de las funciones recursivas primitivas es recursiva primitiva, uno puede comenzar a ver cuán rápidamente puede crecer una función recursiva primitiva. Y cualquier función que pueda ser calculada por una máquina de Turing en un tiempo de ejecución limitado por una función recursiva primitiva es en sí misma recursiva primitiva. Por lo tanto, es difícil imaginar un uso práctico para la μ -recursión completa donde la recursión primitiva no funcione, especialmente porque la primera puede ser simulada por la segunda hasta tiempos de ejecución extremadamente largos.

En cualquier caso, el primer teorema de incompletitud de Kurt Gödel y el problema de la detención implican que hay bucles while que siempre terminan pero no se puede demostrar que lo hagan; por lo tanto, es inevitable que cualquier requisito para una prueba formal de la terminación debe reducir el poder expresivo de un lenguaje de programación. Si bien hemos demostrado que cada bucle que termina tiene una variante, esto no significa que se pueda demostrar que la iteración del bucle está bien fundada.

Ejemplo

A continuación se muestra un ejemplo, en pseudocódigo similar a C , de una variante entera calculada a partir de un límite superior en el número de iteraciones restantes en un bucle while. Sin embargo, C permite efectos secundarios en la evaluación de expresiones, lo cual es inaceptable desde el punto de vista de la verificación formal de un programa informático.

/** variable de condición, que se cambia en el procedimiento S() **/ bool C ; /** función, que calcula un límite de iteración de bucle sin efectos secundarios **/ inline unsigned int getBound ();    /** el cuerpo del bucle no debe alterar V **/ inline void S ();    int main () { unsigned int V = getBound (); /* establecer la variante igual al límite */ assert ( I ); /* invariante de bucle */ while ( C ) { assert ( V > 0 ); /* esta afirmación es la razón de ser de la variante */ S (); /* llamar al cuerpo */ V = ​​min ( getBound (), V - 1 ); /* la variante debe disminuir en al menos uno */ }; assert ( I && ! C ); /* la invariante sigue siendo verdadera y la condición es falsa */                                devuelve 0 ; }; 

¿Por qué siquiera considerar una variante no entera?

¿Por qué siquiera considerar una variante no entera o transfinita? Esta pregunta se ha planteado porque en todos los casos prácticos en los que queremos demostrar que un programa termina, también queremos demostrar que termina en un tiempo razonable. Hay al menos dos posibilidades:

• Un límite superior en el número de iteraciones de un bucle puede estar condicionado a la prueba de terminación en primer lugar. Puede ser deseable probar por separado (o progresivamente) las tres propiedades de
  • corrección parcial,
  • terminación, y
  • tiempo de ejecución.
• Generalidad: considerar variantes transfinitas permite que todas las posibles pruebas de terminación de un bucle while se vean en términos de la existencia de una variante.

Véase también

• Bucle While
• Invariante de bucle
• Inducción transfinita
• Condición de cadena descendente
• Ordinal contable grande
• Corrección (informática)
• Precondiciones más débiles del bucle While

Referencias

1. Winskel, Glynn (1993). La semántica formal de los lenguajes de programación: una introducción . Instituto Tecnológico de Massachusetts. págs. 32-33, 174-176.
2. Bertrand Meyer, Michael Schweitzer (27 de julio de 1995). "Por qué las variantes de bucle son números enteros". Páginas de soporte de Eiffel . Eiffel Software . Consultado el 23 de febrero de 2012 .