Correção Total e Terminação

• Distinguir com precisão correção parcial de correção total e enunciar a correção total como a conjunção das duas.
• Definir uma variante (função de ranking) e explicar por que ela precisa ser ao mesmo tempo não negativa e estritamente decrescente.
• Explicar por que é a boa fundação (well-foundedness), e não a mera diminuição, que de fato exclui a descida infinita.
• Ligar a impossibilidade de um verificador universal de terminação ao Problema da Parada já provado em Computabilidade e Complexidade.
• Provar a correção total de um laço pequeno combinando uma prova de correção parcial com uma variante explícita.

Cada prova em lógica de Hoare construída até aqui nesta disciplina (as regras de atribuição e sequência, a regra do while com seu invariante de laço) provou correção parcial: se o comando terminar, a pós-condição vale. Esse "se" vem fazendo um trabalho silencioso e importante o tempo todo, de forma mais visível na observação de the-hoare-triple de que um comando que não termina torna trivialmente verdadeira qualquer tripla de correção parcial sobre ele. A correção total é o que remove o "se", provando a terminação como uma obrigação separada e adicional, de modo que a garantia final se torna incondicional: o comando termina, e, quando termina, a pós-condição vale.

O motivo de este conceito ficar aqui, depois dos invariantes de laço, em vez de embutido neles, é que a terminação é um tipo de afirmação genuinamente diferente, que exige uma técnica de prova genuinamente diferente: um invariante de laço, por mais cuidadosamente escolhido, não diz nada por si só sobre quantas iterações ainda faltam, só que as iterações que acontecerem preservam um certo fato. Provar a terminação exige medir o progresso em direção ao fim do laço, uma ideia nova, e não um refinamento da ideia de invariante.

E o Problema da Parada, provado por completo em Computabilidade e Complexidade, não é uma abstração distante aqui: é exatamente o motivo de provas de correção total não poderem ser produzidas por um procedimento totalmente automático e universalmente aplicável. Nenhum algoritmo consegue decidir, para todo programa e toda entrada, se aquele programa para; por consequência, não se pode contar com nenhum algoritmo para sempre encontrar (ou mesmo sempre verificar) um argumento de terminação para um laço arbitrário. Este conceito torna essa fronteira da computabilidade concreta dentro da peça de sintaxe mais comum desta disciplina (o laço while), em vez de deixá-la como um fato sobre máquinas de Turing que parece morar em outro lugar.

Correção parcial versus total

A correção parcial, exatamente como the-hoare-triple a definiu, afirma: se C terminar quando iniciado em um estado que satisfaz P, o estado resultante satisfaz Q. A terminação, considerada como propriedade própria e separada, afirma: C não consegue rodar para sempre quando iniciado a partir de um estado que satisfaz P; toda execução a partir de um estado assim acaba chegando a um estado final, ponto, sem nenhum "se". A correção total é definida como a conjunção das duas: C, iniciado a partir de P, tem garantia tanto de terminar quanto de satisfazer Q quando terminar. É uma afirmação genuinamente mais forte que a correção parcial sozinha, e a distância entre elas não é acadêmica; uma prova de apenas correção parcial para um laço de controle crítico para a segurança, por exemplo, deixaria aberta a possibilidade de o laço simplesmente nunca devolver o controle, o que muitas vezes é uma falha tão séria quanto devolver a resposta errada.

Variantes

Uma variante (às vezes chamada de função de ranking, tratada como a mesma ideia abaixo) é uma medida numérica calculada a partir do estado do programa, que precisa satisfazer duas propriedades ao mesmo tempo: ela precisa ser limitada inferiormente por algum valor fixo (por convenção, não negativa, ou seja, limitada inferiormente por zero) e precisa diminuir estritamente a cada execução do corpo do laço. Para laços sobre inteiros, uma escolha natural e extremamente comum de variante é uma expressão como n - i, que diminui exatamente em um a cada iteração de um laço guiado por contador e chega a zero exatamente quando a condição natural de parada do laço é atingida. O limite inferior não é uma nota de rodapé técnica menor; é o que faz "estritamente decrescente" de fato forçar a terminação, em vez de só forçar mudança; um valor que diminui para sempre sem nunca bater em um piso (números negativos arbitrariamente grandes, por exemplo) poderia em princípio diminuir a cada passo de uma execução infinitamente longa, o que não provaria nada sobre a terminação.

Funções de ranking

Enunciando de forma mais geral, uma função de ranking mapeia estados de programa em uma ordem bem fundada: uma ordem em que não existe nenhuma cadeia infinita estritamente decrescente de elementos. Os números naturais com sua ordem usual são o exemplo paradigmático de uma ordem bem fundada: partindo de qualquer número natural e diminuindo repetidamente, a sequência precisa chegar a zero e parar depois de finitos passos, porque não existe cadeia infinita decrescente de números naturais pela qual descer para sempre. Cada transição pelo laço precisa diminuir estritamente o valor da função de ranking e, como a ordem subjacente é bem fundada, uma sequência infinita dessas diminuições estritas é matematicamente impossível; e é exatamente esse o argumento que força o laço a terminar depois de apenas finitas iterações. É o motivo preciso de a boa fundação, e não apenas "diminuir", ser a propriedade que faz o trabalho de verdade: muitas ordens (os inteiros sem limite inferior, por exemplo, ou os números racionais entre 0 e 1 com a subtração comum) permitem sequências infinitas estritamente decrescentes, e uma função de ranking para uma ordem assim não provaria nada sobre a terminação, por mais convincentemente que parecesse "diminuir".

A fronteira da indecidibilidade

Alguns laços terminam por motivos genuinamente sutis, e não obviamente aritméticos: uma variante pode precisar ser uma combinação não trivial de várias variáveis do programa, ou pode depender de fatos que são eles próprios resultados de teoria dos números conquistados com dificuldade, e não aritmética elementar (a famosa iteração "3n+1" da conjectura de Collatz é a ilustração padrão de um laço cuja terminação para todo valor inicial, no momento em que isto é escrito, nem se sabe se é verdadeira, quanto mais demonstrável por alguma variante conhecida). Isso não é uma curiosidade nas margens da teoria; é uma instância direta e concreta da fronteira geral de indecidibilidade já estabelecida: nenhum algoritmo geral consegue sempre decidir a terminação para programas arbitrários e entradas arbitrárias, porque um algoritmo assim resolveria o Problema da Parada, que está provado impossível. Todo verificador prático de terminação, portanto, trabalha dentro de algum fragmento restrito e decidível, aceitando automaticamente padrões sintáticos simples de diminuição e recorrendo a uma variante fornecida por um humano (exatamente a mesma divisão de trabalho que weakest-preconditions já estabeleceu para invariantes de laço) sempre que o padrão cai fora do que o fragmento automatizado cobre.

Laço de contagem regressiva

Considere o laço while x > 0 do x := x - 1, com a precondição x ≥ 0. Tome como variante o próprio x. Cada iteração do laço começa, pela guarda, com x > 0, então x é um inteiro positivo no início de toda iteração que de fato roda; o corpo então o diminui exatamente em um. Como x continua sendo um inteiro não negativo o tempo todo (começa não negativo pela precondição e só é diminuído enquanto é estritamente positivo, nunca podendo ficar negativo, porque a própria guarda interrompe o laço quando x chega a zero), a sequência de valores que x assume é uma sequência estritamente decrescente de números naturais. Os números naturais com sua ordem usual são bem fundados, então nenhuma sequência assim pode continuar para sempre; o laço precisa terminar depois de exatamente tantas iterações quanto o valor inicial de x.

Uma armadilha de correção parcial

Considere while true do skip, com a pós-condição x = x (uma tautologia, escolhida de propósito para deixar o ponto bem nítido). A correção parcial vale trivialmente, e por um motivo um tanto inquietante: como a guarda true nunca fica falsa, não há execução que termina a partir de nenhuma precondição, e a afirmação universalmente quantificada "toda execução que termina satisfaz a pós-condição" é trivialmente verdadeira justamente porque seu domínio de quantificação (o conjunto das execuções que terminam) é vazio. A correção total, ao contrário, falha de vez, e pelo motivo mais direto possível: o laço comprovadamente nunca termina a partir de nenhum estado inicial, então a metade de terminação da conjunção da correção total é simplesmente falsa, por mais trivialmente verdadeira que a pós-condição teria sido se o laço algum dia terminasse. Este exemplo existe especificamente para deixar vívido por que a terminação não é um detalhe menor a ser deixado de lado: um programa "parcialmente correto" nesse sentido trivial não dá nenhuma garantia real sobre nada que importe a quem o chama de verdade.

Descida no estilo de Euclides

Algoritmos que substituem repetidamente um par de valores por um par menor (o algoritmo de Euclides para o máximo divisor comum é o exemplo canônico, substituindo (a, b) por (b, a mod b) a cada passo) normalmente admitem uma variante construída a partir de uma combinação dos argumentos, e não de um deles sozinho, como o segundo argumento ou a soma dos dois, dependendo exatamente de como a recorrência é estruturada. Provar a terminação de um laço assim exige duas coisas, e as duas são genuinamente necessárias, e não só dois jeitos de enunciar o mesmo fato: primeiro, que a medida escolhida diminua estritamente a cada iteração (não só em média, ou em algum momento: a cada iteração, sem exceção) e, segundo, que a medida nunca saia do domínio bem fundado em que se presumiu que ela vive (continuando um inteiro não negativo o tempo todo, por exemplo, em vez de ficar momentaneamente negativa ou não inteira no meio de algum caso de borda). Omitir qualquer uma das metades deixa uma lacuna genuína: uma medida que diminui, mas de vez em quando sai do domínio bem fundado, ainda poderia, em princípio, permitir uma sequência decrescente infinita em alguma outra parte da sua faixa.

• Presumir, sem checar, que uma variável que parece diminuir é sempre não negativa. Uma quantidade que diminui um valor fixo a cada iteração, mas nunca é checada contra um limite inferior, pode, depois de iterações suficientes, cruzar para o território negativo (ou sair de outro modo do domínio bem fundado presumido); nesse ponto, "ela diminui" deixa de implicar "ela precisa chegar a um piso fixo e parar", porque o domínio mudou em silêncio por baixo do argumento.
• Provar a pós-condição e esquecer totalmente a terminação. É exatamente a armadilha que o exemplo while true do skip foi construído para expor: uma prova de correção parcial sintaticamente válida, e até fácil, pode coexistir com um laço que nunca termina, e nada em uma prova de correção parcial, por si só, exclui isso; a correção total exige o argumento separado da variante por cima.
• Usar uma variante que às vezes fica igual em vez de diminuir estritamente. Uma medida apenas não crescente (que pode ficar estável em algumas iterações) não exclui por si só um laço infinito que mantém a medida no mesmo valor para sempre; a variante precisa diminuir estritamente em toda iteração do corpo do laço, sem exceções, para que o argumento da boa fundação de fato force a terminação.
• Esperar que ferramentas automatizadas descubram argumentos de terminação para laços arbitrários. Como a fronteira da indecidibilidade torna preciso, não se pode contar que nenhuma ferramenta encontre (ou mesmo verifique, em total generalidade) um argumento de terminação para todo laço possível; ferramentas práticas tratam padrões sintáticos comuns automaticamente e, fora disso, pedem que um humano forneça a variante, espelhando exatamente como os invariantes de laço são tratados para a correção parcial.

A correção total fortalece a correção parcial acrescentando uma prova independente de terminação, mais comumente estabelecida exibindo uma variante (uma medida em uma ordem bem fundada, limitada inferiormente e estritamente decrescente a cada iteração), o que exclui a execução infinita, porque nenhuma cadeia infinita estritamente decrescente pode existir em um domínio bem fundado. Os exemplos do laço de contagem regressiva e da descida de Euclides mostraram esse argumento feito de forma concreta, enquanto o exemplo while true do skip mostrou exatamente como a correção parcial sozinha pode enganar, valendo trivialmente até para um laço que nunca termina. Como nenhum algoritmo consegue decidir a terminação para programas arbitrários (uma consequência direta do Problema da Parada já provado em Computabilidade e Complexidade), as variantes, como os invariantes de laço antes delas, continuam sendo um lugar em que as ferramentas automatizadas pedem a percepção humana, em vez de prometer fornecê-la automaticamente.