algorithm - logica - ¿Qué es un bucle invariante?
invariante logica (15)
Estoy leyendo "Introducción al algoritmo" por CLRS. En el capítulo 2, los autores mencionan "invariantes de bucle". ¿Qué es un bucle invariante?
Además de todas las buenas respuestas, creo que un gran ejemplo de How to Think About Algorithms, de Jeff Edmonds, puede ilustrar muy bien el concepto:
EJEMPLO 1.2.1 "El algoritmo de búsqueda de dos dedos máximo"
1) Especificaciones: una instancia de entrada consta de una lista L (1..n) de elementos. La salida consiste en un índice i tal que L (i) tiene un valor máximo. Si hay varias entradas con este mismo valor, se devuelve cualquiera de ellas.
2) Pasos básicos: usted decide sobre el método de dos dedos. Tu dedo derecho recorre la lista.
3) Medida de progreso: la medida de progreso es la distancia a lo largo de la lista en la que se encuentra su dedo derecho.
4) El bucle invariante: el bucle invariante indica que su dedo izquierdo apunta a una de las entradas más grandes encontradas hasta ahora por su dedo derecho.
5) Pasos principales: En cada iteración, mueves el dedo derecho hacia abajo una entrada en la lista. Si su dedo derecho ahora apunta a una entrada que es más grande que la entrada del dedo izquierdo, mueva el dedo izquierdo para estar con el dedo derecho.
6) Progreso: progresarás porque tu dedo derecho mueve una entrada.
7) Mantener invariante de bucle: Usted sabe que el invariante de bucle se ha mantenido de la siguiente manera. Para cada paso, el nuevo elemento del dedo izquierdo es Max (antiguo elemento del dedo izquierdo, nuevo elemento). Por el bucle invariante, esto es Max (Max (lista más corta), nuevo elemento). Matemáticamente, este es Max (lista más larga).
8) Establecimiento del invariante de bucle: Inicialmente, el invariante del bucle se establece apuntando ambos dedos al primer elemento.
9) Condición de salida: ha terminado cuando su dedo derecho ha terminado de recorrer la lista.
10) Finalización: al final, sabemos que el problema se resuelve de la siguiente manera. Por la condición de salida, su dedo derecho ha encontrado todas las entradas. Por el bucle invariante, su dedo izquierdo apunta al máximo de estos. Devuelve esta entrada.
11) Terminación y tiempo de ejecución: el tiempo requerido es una cantidad constante de veces la longitud de la lista.
12) Casos especiales: verifique qué sucede cuando hay varias entradas con el mismo valor o cuando n = 0 o n = 1.
13) Detalles de codificación e implementación: ...
14) Prueba formal: la corrección del algoritmo se sigue de los pasos anteriores.
Cabe señalar que un Loar invariante puede ayudar en el diseño de algoritmos iterativos cuando se considera una aserción que expresa relaciones importantes entre las variables que deben ser verdaderas al comienzo de cada iteración y cuando el bucle termina. Si esto se mantiene, el cálculo está en el camino hacia la efectividad. Si es falso, entonces el algoritmo ha fallado.
El significado de invariante nunca es cambio.
Aquí, el invariante de bucle significa "El cambio que ocurre con la variable en el bucle (incremento o decremento) no está cambiando la condición del bucle, es decir, la condición es satisfactoria", por lo que el concepto invariante de bucle ha llegado.
En la búsqueda lineal (según el ejercicio dado en el libro), necesitamos encontrar el valor V en una matriz dada.
Es simple como escanear la matriz de 0 <= k <de longitud y comparar cada elemento. Si se encuentra V, o si el escaneo alcanza la longitud de la matriz, simplemente finalice el ciclo.
Según mi entendimiento en el problema anterior
Invariantes de bucle (inicialización): V no se encuentra en la iteración k - 1. Primera iteración, esto sería -1, por lo que podemos decir que V no se encuentra en la posición -1
Mantenimiento: en la siguiente iteración, V no encontrada en k-1 es válida
Terminación: si V se encuentra en la posición k o k alcanza la longitud de la matriz, finalice el bucle.
En palabras simples, es una condición LOOP que se cumple en cada iteración de bucle:
for(int i=0; i<10; i++)
{ }
En esto podemos decir que el estado de i es i<10 and i>=0
Es difícil hacer un seguimiento de lo que está sucediendo con los bucles. Los bucles que no terminan o terminan sin lograr su comportamiento objetivo es un problema común en la programación de computadoras. Ayuda invariantes de bucle. Un bucle invariante es una declaración formal sobre la relación entre las variables en su programa que se mantiene verdadera justo antes de que se ejecute el bucle (estableciendo el invariante) y es verdadera nuevamente en la parte inferior del bucle, cada vez que pasa por el bucle ). Aquí está el patrón general del uso de invariantes de bucle en su código:
... // el Loar Invariante debe ser verdadero aquí
while (TEST CONDITION) {
// parte superior del bucle
...
// parte inferior del bucle
// el Loar Invariante debe ser verdadero aquí
}
// Terminación + Loar invariante = Objetivo
...
Entre la parte superior e inferior del bucle, es probable que se avance hacia el logro del objetivo del bucle. Esto podría perturbar (hacer falso) lo invariante. El punto de las invariantes de bucles es la promesa de que el invariante se restaurará antes de repetir el cuerpo del bucle cada vez. Hay dos ventajas a esto:
El trabajo no se lleva a la siguiente pasada de manera complicada y dependiente de los datos. Cada paso a través del bucle es independiente de todos los demás, y el invariante sirve para unir los pasos en un todo funcional. El razonamiento de que su bucle funciona se reduce a razonar que el bucle invariable se restaura con cada paso a través del bucle. Esto rompe el complicado comportamiento general del bucle en pequeños pasos simples, cada uno de los cuales puede considerarse por separado. La condición de prueba del bucle no es parte del invariante. Es lo que hace que el bucle termine. Considera por separado dos cosas: por qué el bucle debería terminar alguna vez, y por qué el bucle logra su objetivo cuando termina. El bucle terminará si cada vez que atraviesa el bucle se acerca a la condición de terminación. A menudo es fácil asegurar esto: p. Ej., Escalonar una variable de contador en uno hasta que alcance un límite superior fijo. A veces el razonamiento detrás de la terminación es más difícil.
El bucle invariante debe crearse de modo que cuando se alcance la condición de terminación, y el invariante sea verdadero, se alcance el objetivo:
invariante + terminación => objetivo
Se necesita práctica para crear invariantes que sean simples y se relacionen y que capturen todo el logro de la meta, excepto la terminación. Es mejor usar símbolos matemáticos para expresar invariantes de bucle, pero cuando esto lleva a situaciones demasiado complicadas, confiamos en una prosa clara y sentido común.
Hay una cosa que muchas personas no se dan cuenta de inmediato cuando se trata de bucles e invariantes. Se confunden entre el bucle invariante y el bucle condicional (la condición que controla la terminación del bucle).
Como señala la gente, el bucle invariante debe ser verdadero
- antes de que comience el bucle
- antes de cada iteración del bucle
- después de que el bucle termina
(aunque puede ser temporalmente falso durante el cuerpo del bucle). Por otro lado, el condicional del bucle debe ser falso después de que el bucle termina, de lo contrario, el bucle nunca terminaría.
Por lo tanto, el bucle invariante y el bucle condicional deben ser condiciones diferentes.
Un buen ejemplo de un bucle complejo invariante es la búsqueda binaria.
bsearch(type A[], type a) {
start = 1, end = length(A)
while ( start <= end ) {
mid = floor(start + end / 2)
if ( A[mid] == a ) return mid
if ( A[mid] > a ) end = mid - 1
if ( A[mid] < a ) start = mid + 1
}
return -1
}
Por lo tanto, el condicional del bucle parece bastante sencillo: cuando comienza> termina, el bucle termina. Pero ¿por qué es correcto el bucle? ¿Qué es el invariante de bucle que prueba que es correcto?
El invariante es el enunciado lógico:
if ( A[mid] == a ) then ( start <= mid <= end )
Esta afirmación es una tautología lógica: siempre es cierta en el contexto del bucle / algoritmo específico que intentamos demostrar . Y proporciona información útil sobre la corrección del bucle una vez que termina.
Si regresamos porque encontramos el elemento en la matriz, entonces la declaración es claramente verdadera, ya que si A[mid] == a entonces a está en la matriz y mid debe estar entre el inicio y el final. Y si el bucle termina porque start > end , no puede haber un número tal que start <= mid y mid <= end y, por lo tanto, sabemos que la declaración A[mid] == a debe ser falsa. Sin embargo, como resultado, la declaración lógica general sigue siendo cierta en el sentido nulo. (En lógica, la afirmación if (false) entonces (algo) siempre es verdadera).
Ahora, ¿qué hay de lo que dije sobre que el condicional del bucle es necesariamente falso cuando el bucle termina? Parece que cuando el elemento se encuentra en la matriz, ¿el condicional del bucle es verdadero cuando el bucle termina? En realidad no lo es, porque el condicional implícito del bucle es en realidad while ( A[mid] != a && start <= end ) pero acortamos la prueba real ya que la primera parte está implícita. Este condicional es claramente falso después del bucle, independientemente de cómo termine el bucle.
Invariante en este caso significa una condición que debe ser cierta en un cierto punto en cada iteración de bucle.
En la programación de contratos, un invariante es una condición que debe ser cierta (por contrato) antes y después de que se llame a cualquier método público.
La propiedad invariante del bucle es una condición que se cumple para cada paso de la ejecución de un bucle (es decir, para bucles, bucles, etc.)
Esto es esencial para una Prueba invariante de bucle, donde se puede demostrar que un algoritmo se ejecuta correctamente si en cada paso de su ejecución se cumple esta propiedad invariante de bucle.
Para que un algoritmo sea correcto, el invariante de bucle debe mantenerse en:
Inicialización (el principio)
Mantenimiento (cada paso después)
Terminación (cuando está terminado)
Esto se usa para evaluar un montón de cosas, pero el mejor ejemplo son los algoritmos codiciosos para el recorrido ponderado de gráficos. Para que un algoritmo codicioso produzca una solución óptima (una ruta a través del gráfico), debe alcanzar la conexión de todos los nodos en la ruta de menor peso posible.
Por lo tanto, la propiedad invariable del bucle es que la ruta tomada tiene el menor peso. Al principio no hemos agregado bordes, por lo que esta propiedad es verdadera (no es falsa, en este caso). En cada paso , seguimos el borde de menor peso (el paso codicioso), por lo que nuevamente estamos tomando el camino de menor peso. Al final , hemos encontrado la ruta ponderada más baja, por lo que nuestra propiedad también es cierta.
Si un algoritmo no hace esto, podemos probar que no es óptimo.
Las respuestas anteriores han definido un Loar Invariante de una manera muy buena.
Ahora permítanme tratar de explicar cómo los autores de CLRS usaron Invariantes de bucles para probar la corrección de la Inserción.
Algoritmo de clasificación de inserción (como se indica en el libro):
INSERTION-SORT(A)
for j ← 2 to length[A]
do key ← A[j]
// Insert A[j] into the sorted sequence A[1..j-1].
i ← j - 1
while i > 0 and A[i] > key
do A[i + 1] ← A[i]
i ← i - 1
A[i + 1] ← key
Loar invariante en este caso (Fuente: libro de CLRS): La subarregla [1 a j-1] siempre se ordena.
Ahora comprobemos esto y probemos que el algoritmo es correcto.
Inicialización : Antes de la primera iteración j = 2. Por lo tanto, Subarray [1: 1] es la matriz que se va a probar. Como solo tiene un elemento, está ordenado. Así se satisface Invariante.
Mantenimiento : esto se puede verificar fácilmente verificando el invariante después de cada iteración. En este caso, se cumple.
Terminación : Este es el paso donde probaremos la corrección del algoritmo.
Cuando el bucle termina, el valor de j = n + 1. De nuevo, se cumple la invariante de bucle. Esto significa que se debe clasificar el subarreglo [1 a n].
Esto es lo que queremos hacer con nuestro algoritmo. Por lo tanto, nuestro algoritmo es correcto.
Loar invariante es una fórmula matemática como (x=y+1) . En ese ejemplo, y representan dos variables en un bucle. Teniendo en cuenta el comportamiento cambiante de esas variables a lo largo de la ejecución del código, es casi imposible probar todos los valores posibles de x e y ver si producen algún error. Digamos que x es un número entero. El entero puede contener espacio de 32 bits en la memoria. Si ese número supera, se produce un desbordamiento de búfer. Por lo tanto, debemos asegurarnos de que, durante la ejecución del código, nunca supere ese espacio. para eso, necesitamos entender una fórmula general que muestre la relación entre las variables. Después de todo, solo tratamos de entender el comportamiento del programa.
Me gusta esta definición muy simple: ( here )
Un bucle invariante es una condición [entre variables de programa] que es necesariamente cierta inmediatamente antes e inmediatamente después de cada iteración de un bucle. (Tenga en cuenta que esto no dice nada acerca de su verdad o falsedad en parte a través de una iteración).
Por sí mismo, un bucle invariante no hace mucho. Sin embargo, dado un invariante apropiado, puede usarse para ayudar a probar la exactitud de un algoritmo. El ejemplo simple en CLRS probablemente tiene que ver con la clasificación. Por ejemplo, deje que su invariante de bucle sea algo como, al comienzo del bucle, las primeras i entradas de esta matriz están ordenadas. Si puede probar que esto es realmente un bucle invariante (es decir, que se mantiene antes y después de cada iteración del bucle), puede usar esto para probar la corrección de un algoritmo de clasificación: al final del bucle, el bucle invariante aún se cumple. , y el contador i es la longitud de la matriz. Por lo tanto, las primeras entradas i están ordenadas significa que toda la matriz está ordenada.
Un ejemplo aún más simple: invariantes de bucles, corrección y derivación de programas .
La forma en que entiendo un bucle invariante es como una herramienta sistemática y formal para razonar acerca de los programas. Hacemos una sola declaración en la que nos centramos en demostrar que somos verdaderos, y lo llamamos el bucle invariante. Esto organiza nuestra lógica. Si bien también podemos argumentar informalmente sobre la corrección de algún algoritmo, el uso de un bucle invariante nos obliga a pensar con mucho cuidado y garantiza que nuestro razonamiento sea hermético.
Un bucle invariante es una afirmación que es verdadera antes y después de la ejecución del bucle.
Lo siento, no tengo permiso para comentar.
@Tomas Petricek como has mencionado
Un invariante más débil que también es cierto es que i> = 0 && i <10 (¡porque esta es la condición de continuación!) "
¿Cómo es un bucle invariante?
Espero no estar equivocado, por lo que entiendo [1] , la invariante del bucle será verdadera al comienzo del bucle (Inicialización), será verdadera antes y después de cada iteración (Mantenimiento) y también será cierta después La terminación del bucle (Terminación) . Pero después de la última iteración, i se convierte en 10. Por lo tanto, la condición i> = 0 && i <10 se vuelve falsa y termina el ciclo. Viola la tercera propiedad (Terminación) del bucle invariante.
[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html
En palabras simples, un bucle invariante es un predicado (condición) que se mantiene para cada iteración del bucle. Por ejemplo, veamos un bucle for simple que se ve así:
int j = 9;
for(int i=0; i<10; i++)
j--;
En este ejemplo, es cierto (para cada iteración) que i + j == 9 . Un invariante más débil que también es cierto es que i >= 0 && i <= 10 .