Variante de bucle - Loop variant

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 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 de computadora por descendencia bien fundada . 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:

{\ Displaystyle {\ frac {\ {I \ land C \} \; S \; \ {I \}} {\ {I \} \; {\ mathtt {mientras}} \; C \; {\ mathtt { hacer}} \; S \; \ {I \ land \ lnot C \}}},}

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:

{\ Displaystyle {\ frac {<{\ text {está bien fundamentado}}, \; [I \ land C \ land V = z] \; S \; [I \ land V <z]} {[I] \; {\ mathtt {mientras}} \; C \; {\ mathtt {hacer}} \; S \; [I \ land \ lnot C]}},}

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

{\ Displaystyle {\ mathtt {mientras}} \; C \; {\ mathtt {hacer}} \; S}

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

{\ Displaystyle [I \ land C] \; S \; [I].}

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 $σ$ .

Observamos que, de lo contrario, el bucle no terminaría. ${\ Displaystyle \ sigma '\ neq \ sigma,}$

A continuación, considérese el cierre transitivo y reflexivo de la relación "sucesora". Llame a esta iteración : decimos que un estado $σ '$ es una iteración de $σ$ si existe una cadena finita tal que y es un "sucesor" de 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 nuevamente, de lo contrario, el ciclo no terminaría. 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 estados $Σ$ , ya que es estricta (irreflexiva) y está contenida en la relación de "iteración". 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 ω ₁ , 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 desde una entrada finita es infinitamente numerable, y ω ₁ 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, 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.

/** condition-variable, which is changed in procedure S() **/
bool C;
/** function, which computes a loop iteration bound without side effects **/
inline unsigned int getBound();

/** body of loop must not alter V **/ 
inline void S(); 

int main() {
    unsigned int V = getBound(); /* set variant equal to bound */
    assert(I); /* loop invariant */
    while (C) {
        assert(V > 0); /* this assertion is the variant's raison d'être (reason of existence) */
        S(); /* call the body */
        V = min(getBound(), V - 1); /* variant must decrease by at least one */
    };
    assert(I && !C); /* invariant is still true and condition is false */

    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.

Languages

In other projects

Variante de bucle - Loop variant

Contenido

Regla de inferencia para la corrección total

Cada bucle que termina tiene una variante

Consideraciones prácticas

Ejemplo

¿Por qué incluso considerar una variante no entera?

Ver también

Referencias