O que é um loop invariável?

Estou lendo "Introdução ao algoritmo", do CLRS. No capítulo 2, os autores mencionam "invariantes de loop". O que é um loop invariável?

Em palavras simples, um loop invariável é um predicado (condição) válido para todas as iterações do loop. Por exemplo, vejamos um forloop simples que se parece com isso:

int j = 9;
for(int i=0; i<10; i++)  
  j--;

Neste exemplo, é verdade (para todas as iterações) isso i + j == 9. Um invariante mais fraco que também é verdade é isso i >= 0 && i <= 10.

Eu gosto desta definição muito simples: ( fonte )

Um invariante de loop é uma condição [entre variáveis ​​de programa] que é necessariamente verdadeira imediatamente antes e imediatamente após cada iteração de um loop. (Observe que isso não diz nada sobre sua verdade ou falsidade no meio de uma iteração.)

Por si só, um loop invariável não faz muito. No entanto, dada uma invariável apropriada, ela pode ser usada para ajudar a provar a correção de um algoritmo. O exemplo simples no CLRS provavelmente tem a ver com classificação. Por exemplo, deixe seu loop invariável ser algo como, no início do loop, as primeiras ientradas dessa matriz são classificadas. Se você puder provar que é de fato uma invariante de loop (ou seja, que ela contém antes e depois de cada iteração de loop), você pode usá-lo para provar a correção de um algoritmo de classificação: no término do loop, a invariante de loop ainda é satisfeita. , e o contador ié o comprimento da matriz. Portanto, as primeiras ientradas são classificadas significa que toda a matriz é classificada.

Um exemplo ainda mais simples: loops de invariantes, correção e derivação de programa .

A maneira como entendo um loop invariável é como uma ferramenta sistemática e formal para raciocinar sobre programas. Fazemos uma afirmação única que focamos em provar a verdade e a chamamos de loop invariável. Isso organiza nossa lógica. Embora possamos argumentar informalmente sobre a correção de algum algoritmo, o uso de um loop invariável nos obriga a pensar com muito cuidado e garante que nosso raciocínio seja hermético.

Há uma coisa que muitas pessoas não percebem imediatamente ao lidar com loops e invariantes. Eles ficam confusos entre o loop invariável e o loop condicional (a condição que controla a finalização do loop).

Como as pessoas apontam, o loop invariável deve ser verdadeiro

1. antes do loop começar
2. antes de cada iteração do loop
3. depois que o loop terminar

(embora possa ser temporariamente falso durante o corpo do loop). Por outro lado, o condicional do loop deve ser falso depois que o loop termina, caso contrário, o loop nunca terminaria.

Portanto, o loop invariável e o condicional do loop devem ter condições diferentes.

Um bom exemplo de invariante de loop complexo é para pesquisa binária.

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

}

Portanto, o condicional do loop parece bem direto - quando start> end o loop termina. Mas por que o loop está correto? Qual é o loop invariável que prova sua correção?

O invariante é a afirmação lógica:

if ( A[mid] == a ) then ( start <= mid <= end )

Essa afirmação é uma tautologia lógica - sempre é verdadeira no contexto do loop / algoritmo específico que estamos tentando provar . E fornece informações úteis sobre a correção do loop após o término.

Se retornarmos porque encontramos o elemento na matriz, a declaração será claramente verdadeira, pois se A[mid] == aela aestiver na matriz e middeve estar entre o início e o fim. E se os termina de loop, porque start > endentão não pode haver nenhum número tal que start <= mid e mid <= end e, portanto, sabemos que a declaração A[mid] == adeve ser falsa. No entanto, como resultado, a declaração lógica geral ainda é verdadeira no sentido nulo. (Na lógica, a afirmação if (false) then (something) é sempre verdadeira.)

Agora, o que eu disse sobre o condicional do loop necessariamente ser falso quando o loop termina? Parece que quando o elemento é encontrado na matriz, o condicional do loop é verdadeiro quando o loop termina !? Na verdade, não é, porque o condicional implícito do loop é realmente, while ( A[mid] != a && start <= end )mas reduzimos o teste real, pois a primeira parte está implícita. Essa condicional é claramente falsa após o loop, independentemente de como o loop termina.

As respostas anteriores definiram um loop invariável de uma maneira muito boa.

A seguir, é como os autores do CLRS usaram o invariante de loop para provar a correção do tipo de inserção.

Algoritmo de classificação de inserção (conforme fornecido no livro):

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

Loop invariante neste caso: O sub-array [1 a j-1] é sempre classificado.

Agora vamos verificar isso e provar que o algoritmo está correto.

Inicialização : Antes da primeira iteração j = 2. Portanto, o sub array [1: 1] é o array a ser testado. Como ele possui apenas um elemento, é classificado. Assim, invariável é satisfeito.

Manutenção : Isso pode ser facilmente verificado verificando-se o invariante após cada iteração. Neste caso, está satisfeito.

Rescisão : Este é o passo em que provaremos a correção do algoritmo.

Quando o loop termina, o valor de j = n + 1. Novamente, o invariante do loop é satisfeito. Isso significa que a sub-matriz [1 a n] deve ser classificada.

É isso que queremos fazer com o nosso algoritmo. Assim, nosso algoritmo está correto.

Além de todas as boas respostas, acho que um ótimo exemplo de How to Think About Algorithms, de Jeff Edmonds, pode ilustrar muito bem o conceito:

EXEMPLO 1.2.1 "O algoritmo Find-Max de dois dedos"

1) Especificações: Uma instância de entrada consiste em uma lista L (1..n) de elementos. A saída consiste em um índice i, de modo que L (i) tenha valor máximo. Se houver várias entradas com esse mesmo valor, qualquer uma delas será retornada.

2) Etapas básicas: você decide o método com dois dedos. Seu dedo direito percorre a lista.

3) Medida de progresso: A medida de progresso é o quão longe está o dedo direito da lista.

4) O invariante de loop: O invariante de loop afirma que o dedo esquerdo aponta para uma das maiores entradas encontradas até agora pelo dedo direito.

5) Etapas principais: a cada iteração, você move o dedo direito uma das entradas da lista. Se o seu dedo direito agora está apontando para uma entrada maior que a entrada do dedo esquerdo, mova o dedo esquerdo para ficar com o dedo direito.

6) Progredir: Você progride porque seu dedo direito move uma entrada.

7) Manter invariável do loop: você sabe que o invariante do loop foi mantido da seguinte maneira. Para cada etapa, o novo elemento do dedo esquerdo é Max (elemento antigo do dedo esquerdo, novo elemento). Pelo invariante do loop, é Max (Max (lista mais curta), novo elemento). Matematicamente, esse é Max (lista mais longa).

8) Estabelecendo o invariante do loop: Você inicialmente estabelece o invariante do loop apontando os dois dedos para o primeiro elemento.

9) Condição de Saída: Você termina quando o dedo direito termina de percorrer a lista.

10) Final: No final, sabemos que o problema é resolvido da seguinte forma. Pela condição de saída, seu dedo direito encontrou todas as entradas. Pelo laço invariável, o dedo esquerdo aponta no máximo deles. Retorne esta entrada.

11) Tempo de término e execução: o tempo necessário é algumas vezes constante o comprimento da lista.

12) Casos especiais: verifique o que acontece quando há várias entradas com o mesmo valor ou quando n = 0 ou n = 1.

13) Detalhes de codificação e implementação: ...

14) Prova formal: A correção do algoritmo segue as etapas acima.

Deve-se notar que um Loop Invariável pode ajudar no design de algoritmos iterativos quando considerado uma afirmação que expressa relacionamentos importantes entre as variáveis ​​que devem ser verdadeiras no início de cada iteração e quando o loop termina. Se isso acontecer, o cálculo está no caminho da eficácia. Se falso, o algoritmo falhou.

Invariante, neste caso, significa uma condição que deve ser verdadeira em um determinado ponto em cada iteração de loop.

Na programação de contratos, uma invariável é uma condição que deve ser verdadeira (por contrato) antes e depois de qualquer método público ser chamado.

O significado de invariante nunca muda

Aqui, o invariante do loop significa "A mudança que ocorre na variável do loop (incremento ou decremento) não está alterando a condição do loop, ou seja, a condição é satisfatória", de modo que o conceito de invariável do loop chegou

A Propriedade Invariável do Loop é uma condição que vale para cada etapa da execução de um loop (por exemplo, para loops, enquanto loops, etc.)

Isso é essencial para uma prova invariável de loop, na qual é possível mostrar que um algoritmo é executado corretamente se a cada passo de sua execução essa propriedade invariante de loop é mantida.

Para que um algoritmo esteja correto, o Loop Invariant deve manter em:

Inicialização (o começo)

Manutenção (cada passo depois)

Rescisão (quando terminar)

Isso é usado para avaliar várias coisas, mas o melhor exemplo são algoritmos gananciosos para a travessia ponderada de gráficos. Para que um algoritmo ganancioso produza uma solução ideal (um caminho no gráfico), ele deve conectar todos os nós no caminho de menor peso possível.

Assim, a propriedade invariável do loop é que o caminho percorrido tem o menor peso. No início , não adicionamos nenhuma aresta; portanto, essa propriedade é verdadeira (não é falsa, neste caso). Em cada etapa , seguimos a borda do menor peso (a etapa gananciosa), e, novamente, seguimos o caminho do menor peso. No final , encontramos o caminho ponderado mais baixo, portanto nossa propriedade também é verdadeira.

Se um algoritmo não fizer isso, podemos provar que não é o ideal.

É difícil acompanhar o que está acontecendo com os loops. Loops que não terminam ou terminam sem atingir o comportamento do objetivo é um problema comum na programação de computadores. Invariantes de loop ajudam. Um invariante de loop é uma declaração formal sobre o relacionamento entre variáveis ​​em seu programa, verdadeiro antes do loop ser executado (estabelecendo o invariante) e verdadeiro novamente na parte inferior do loop, sempre no loop (mantendo o invariante). ) Aqui está o padrão geral do uso de Loop Invariants no seu código:

... // o loop invariante deve ser verdadeiro aqui
enquanto (TEST CONDITION) {
// parte superior do loop
...
// parte inferior do loop
// o loop invariante deve ser verdadeiro aqui
}
// Terminação + loop invariante = Objetivo
...
Entre a parte superior e inferior do loop, presumivelmente está sendo feito progresso para atingir o objetivo do loop. Isso pode perturbar (tornar falso) o invariante. O objetivo dos Invariantes de Loop é a promessa de que os invariantes serão restaurados antes de repetir o corpo do loop a cada vez. Há duas vantagens nisso:

O trabalho não é transportado para a próxima passagem de maneira complicada e dependente de dados. Cada passagem pelo loop é independente de todas as outras, com o invariante servindo para unir as passagens em um todo que funciona. O raciocínio de que seu loop funciona é reduzido ao raciocínio de que o invariante do loop é restaurado a cada passagem pelo loop. Isso divide o comportamento geral complicado do loop em pequenas etapas simples, cada uma das quais pode ser considerada separadamente. A condição de teste do loop não faz parte da invariante. É o que faz o loop terminar. Você considera separadamente duas coisas: por que o loop deve terminar e por que o loop atinge seu objetivo quando ele termina. O loop será encerrado se a cada vez que você se aproximar de satisfazer a condição de encerramento. Muitas vezes, é fácil garantir isso: por exemplo passo uma variável do contador em um até atingir um limite superior fixo. Às vezes, o raciocínio por trás da rescisão é mais difícil.

O invariante de loop deve ser criado para que, quando a condição de término for atingida e o invariante for verdadeiro, o objetivo seja alcançado:

invariante + terminação => objetivo
É necessário criar invariantes simples e relacionados que capturam toda a consecução do objetivo, exceto o término. É melhor usar símbolos matemáticos para expressar invariantes de loop, mas quando isso leva a situações complicadas demais, contamos com prosa clara e bom senso.

Desculpe, não tenho permissão para comentar.

@Tomas Petricek como você mencionou

Uma invariante mais fraca que também é verdadeira é que i> = 0 && i <10 (porque esta é a condição de continuação!) "

Como é um loop invariável?

Espero não estar errado, tanto quanto eu entendo ^[1] , o loop invariável será verdadeiro no início do loop (Inicialização), será verdadeiro antes e depois de cada iteração (Manutenção) e também será verdadeiro após o término do loop (término) . Porém, após a última iteração, i se torna 10. Portanto, a condição i> = 0 && i <10 se torna falsa e finaliza o loop. Ele viola a terceira propriedade (terminação) do loop invariável.

[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html

Invariante de loop é uma fórmula matemática como (x=y+1). Nesse exemplo, xe yrepresenta duas variáveis ​​em um loop. Considerando a mudança de comportamento dessas variáveis ao longo da execução do código, é quase impossível testar todos os possíveis para xe yvalores e ver se eles produzem qualquer bug. Vamos dizer que xé um número inteiro. Inteiro pode conter 32 bits de espaço na memória. Se esse número exceder, ocorrerá um estouro de buffer. Portanto, precisamos ter certeza de que, durante a execução do código, nunca exceda esse espaço. para isso, precisamos entender uma fórmula geral que mostre a relação entre variáveis. Afinal, apenas tentamos entender o comportamento do programa.

Em palavras simples, é uma condição LOOP que é verdadeira em todas as iterações de loop:

for(int i=0; i<10; i++)
{ }

Neste podemos dizer estado de i é i<10 and i>=0

Uma invariante de loop é uma afirmação verdadeira antes e depois da execução do loop.

Na Pesquisa Linear (conforme o exercício indicado no livro), precisamos encontrar o valor V em um determinado array.

É simples como varrer a matriz de 0 <= k <comprimento e comparar cada elemento. Se V for encontrado, ou se a varredura atingir o comprimento da matriz, basta finalizar o loop.

De acordo com o meu entendimento no problema acima

Invariantes de loop (inicialização): V não é encontrado na iteração k-1. Primeira iteração, isso seria -1, portanto, podemos dizer que V não foi encontrado na posição -1

Manutenção: Na próxima iteração, V não encontrado em k-1 é verdadeiro

Terminação: Se V encontrado na posição k ou k atingir o comprimento da matriz, encerre o loop.