En informática , una variante de bucle es una función matemática definida en el espacio de estado de un programa informático cuyo valor disminuye monótonamente con respecto a una relación (estricta) bien fundada mediante la iteración de un bucle while en algunas condiciones invariantes , lo que garantiza su terminación . Una variante de bucle cuyo rango está restringido a los enteros no negativos también se conoce como función ligada , porque en este caso proporciona un límite superior trivial en el número de iteraciones de un bucle antes de que termine. Sin embargo, una variante de bucle puede ser transfinitay, por lo tanto, no está necesariamente restringido 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 de computadora por 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 posea una variante terminará después de un número finito de iteraciones, siempre que su cuerpo termine cada vez.
Un bucle while , o, más generalmente, un programa de computadora que puede contener bucles while, se dice que es totalmente correcto si es parcialmente correcto y termina.
Regla de inferencia para la corrección total
Para establecer formalmente la regla de inferencia para la terminación de un ciclo while que hemos demostrado anteriormente, recuerde que en la lógica de Floyd-Hoare , la regla para expresar la corrección parcial de un ciclo while es:
donde I es el invariante , C es la condición y S es el cuerpo del bucle. Para expresar una corrección total, escribimos en su lugar:
donde, además, V es la variante y, por convención, el símbolo libre z se considera cuantificado universalmente .
Cada bucle que termina tiene una variante
La existencia de una variante implica que termina un ciclo while. Puede parecer sorprendente, pero lo contrario también es cierto, siempre que asumamos el axioma de elección : cada ciclo while que termina (dado su invariante) tiene una variante. Para probar esto, suponga que el bucle
termina dado el invariante I donde tenemos la afirmación de corrección total
Considere la relación "sucesor" en el espacio de estados inducida por la ejecución de la instrucción S de un estado que satisface tanto el invariante I y la condición C . Es decir, decimos que un estado es un "sucesor" de si y solo si
- I y C son ambos verdaderos en el estado y
- es el estado que resulta de la ejecución del enunciado S en el estado
Notamos eso porque de lo contrario el bucle no terminaría.
A continuación, considérese el cierre transitivo y reflexivo de la relación "sucesora". Llame a esta iteración : decimos que un estadoes una iteración de si alguno o hay una cadena finita tal que y es un "sucesor" de por todo yo ,
Notamos que si y son dos estados distintos, y es una iteración de , luego no puede ser una iteración de de nuevo, de lo contrario, el bucle no podría terminar. En otras palabras, la iteración es antisimétrica y, por lo tanto, un orden parcial .
Ahora, dado que el ciclo 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 la cadena descendente .
Por lo tanto, asumiendo el axioma de elección , la relación de "sucesor" que definimos originalmente para el bucle está bien fundada en el espacio de estadosya que es estricto (irreflexivo) y está contenido en la relación "iterar". Por lo tanto, la función de identidad en este espacio de estados es una variante del ciclo while, como hemos demostrado que el estado debe disminuir estrictamente, como "sucesor" y "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 ω 1 , el primer ordinal incontable , es decir,
Esto se debe a que la colección de todos los estados alcanzables por un programa informático finito en un número finito de pasos desde una entrada finita es infinita numerable, y ω 1 es la enumeración de todos los tipos de orden de pozo en conjuntos numerables.
Consideraciones prácticas
En la práctica, las variantes de bucle a menudo se toman como enteros no negativos , o incluso se requiere que lo sean, [2] pero el requisito de que cada bucle tenga una variante de entero elimina el poder expresivo de la iteración ilimitada de un lenguaje de programación. A menos que tal lenguaje (formalmente verificado) 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 recursión μ completa , sino solo recursividad 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 . Si se considera incluso el caso simple de exponenciación como una función recursiva primitiva, y que la composición de las funciones recursivas primitivas es recursiva primitiva, se puede empezar a ver qué tan rápido 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 funcionará, especialmente porque la primera puede ser simulada por la última hasta tiempos de ejecución excesivamente largos.
Y 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 probar que lo hagan; por lo tanto, es inevitable que cualquier requisito de una prueba formal de terminación deba 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 probar la buena base de la iteración del bucle.
Ejemplo
Aquí hay un ejemplo, en un pseudocódigo similar a C , de una variante entera calculada a partir de algún límite superior en el número de iteraciones restantes en un ciclo 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-condición, que se cambia en el procedimiento S () ** / bool C ; / ** función, que calcula un enlace 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 (); / * establece la variante igual al límite * / assert ( I ); / * ciclo invariante * / while ( C ) { aseverar ( V > 0 ); / * esta afirmación es la razón de ser de la variante (razón de existencia) * / S (); / * llamar al cuerpo * / V = min ( getBound (), V - 1 ); / * la variante debe disminuir en al menos un * / }; afirmar ( I && ! C ); / * invariante sigue siendo verdadero y la condición es falsa * / return 0 ; };
¿Por qué incluso considerar una variante no entera?
¿Por qué incluso considerar una variante no entera o transfinita? Esta pregunta se ha planteado porque en todos los casos prácticos en los que queremos probar que un programa finaliza, también queremos demostrar que finaliza en un período de tiempo razonable. Hay al menos dos posibilidades:
- Un límite superior en el número de iteraciones de un bucle puede estar condicionado a probar la 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 ver todas las posibles pruebas de terminación para un ciclo temporal en términos de la existencia de una variante.
Ver también
- Mientras bucle
- Invariable de bucle
- Inducción transfinita
- Condición de cadena descendente
- Ordinal contable grande
- Corrección (informática)
- Condiciones previas más débiles del ciclo While
Referencias
- ^ Winskel, Glynn (1993). La semántica formal de los lenguajes de programación: una introducción . Instituto de Tecnología de Massachusetts. págs. 32–33, 174–176.
- ^ Bertrand Meyer, Michael Schweitzer (27 de julio de 1995). "Por qué las variantes de bucle son enteros" . Las páginas de soporte de Eiffel . Software Eiffel . Consultado el 23 de febrero de 2012 .