Resumo

  • Em Edinburgh LCF, uma tática propunha subobjetivos e devolvia uma validação. Só quando essa validação recombinava teoremas aceitos por meio das regras primitivas surgia um teorema para o objetivo original.
  • O tipo abstrato thm reduzia o código com autoridade direta para construir teoremas, mas não provava a consistência da lógica, a fidelidade da especificação nem a correção do compilador, do runtime e do hardware.
  • A história é coletiva: a lógica veio de Dana Scott; Stanford LCF antecedeu Edinburgh LCF; Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey e uma comunidade mais ampla participaram do sistema e de ML.

A busca termina antes da aceitação

Uma prova interativa pode começar pelo objetivo e trabalhar para trás. A tática experimenta reescritas, divide o problema, escolhe alternativas e recua. Ao fim, pode declarar que não restam subobjetivos. No LCF, ainda falta a pergunta essencial: as regras protegidas conseguem construir o teorema pedido a partir dos resultados obtidos?

Cada tática devolve também uma validação. Essa função recebe os teoremas dos subobjetivos e deve produzir o teorema do objetivo inicial. Ela transforma o plano de busca para trás numa derivação para frente. Se não cumprir essa promessa, o registro da busca não passa a valer como teorema.

O desenho resolvia um conflito entre extensibilidade e confiança. Usuários precisam escrever novos métodos de prova, e esses métodos podem conter erros. Se cada extensão pudesse criar teoremas diretamente, toda automação nova ampliaria a superfície confiável. Edinburgh LCF colocou a construção atrás de um tipo abstrato, normalmente chamado thm, e expôs axiomas e regras primitivas como os construtores permitidos.

Isso não torna táticas infalíveis. Elas podem divergir, escolher subobjetivos ruins, lançar exceções ou oferecer uma validação inválida. A garantia arquitetônica é mais estreita: falhar fora da interface não dá uma rota alternativa para fabricar thm. O fracasso permanece fracasso.

Uma linhagem construída por várias pessoas

Em 1972, Milner descreveu um verificador implementado para a Logic for Computable Functions de Dana Scott. A experiência de Stanford mostrou tanto a promessa quanto o custo de provas longas e pouco programáveis. A partir de 1973, em Edimburgo, o projeto avançou para um ambiente extensível.

O livro de 1979 é assinado por Michael J. C. Gordon, Robin Milner e Christopher P. Wadsworth. O artigo de 1978 sobre a metalinguagem inclui também Lockwood Morris e Malcolm Newey. Relatos posteriores de Larry Paulson e Michael Gordon ligam Stanford LCF a Edinburgh LCF, Cambridge LCF, HOL e Isabelle. A centralidade de Milner não transforma uma realização coletiva em autoria exclusiva.

ML surgiu como “Meta Language”, usada para programar procedimentos de prova. Seu sistema de tipos polimórficos tornou-se uma contribuição autônoma; em 1978, Milner publicou resultados de solidez semântica e sintática e descreveu o uso do algoritmo de inferência no LCF. O Prêmio Turing de 1991 reconheceu LCF, ML e CCS, mas o crédito técnico continua distribuído entre equipe e comunidade.

As regras de inferência trabalham para frente, de teoremas existentes a um novo teorema. As táticas trabalham para trás, de um objetivo a subobjetivos. A validação fecha o circuito. Os “tacticals” organizam sequência, repetição e escolha entre táticas; ampliam o controle da busca sem criar novas verdades primitivas.

O ganho e o limite do tipo abstrato

Um tipo abstrato esconde sua representação e permite apenas operações selecionadas. O código comum pode transportar um valor thm e passá-lo a regras, mas não editar sua estrutura interna para forjar outro. A disciplina de tipos preserva essa separação.

Assim, a revisão pode se concentrar num conjunto menor de axiomas e regras. Táticas podem mudar rapidamente sem receber autoridade direta de aceitação. O volume de código complexo deixa de coincidir com o volume de código que decide o nascimento de um teorema.

Mas um núcleo pequeno não elimina a confiança. As regras precisam ser corretas para a lógica escolhida. A implementação de ML, o compilador e a execução precisam preservar a abstração. Recursos inseguros, falhas de runtime e erros de hardware podem quebrar a premissa. Até parser e impressor podem mostrar algo diferente do termo armazenado. A raiz confiável diminui; ela não desaparece.

Solidez também não é o mesmo que consistência. Saber que um valor veio apenas de certas funções é uma afirmação sobre sua construção, não uma prova independente de que cada função representa uma inferência válida. E um teorema formal não prova que a especificação expressa o sistema real ou a intenção de quem o opera. Um núcleo impecável pode responder perfeitamente à pergunta errada.

A validação como compromisso executável

A validação carrega a obrigação adiada da tática. Ao propor subobjetivos, a tática promete que os teoremas correspondentes bastam para a meta original. Depois, a validação deve cumprir a promessa usando as regras aceitas.

Quando tacticals compõem buscas, também compõem validações. Uma sequência aplica uma estratégia após outra; uma repetição continua enquanto houver progresso. O controle pode ser sofisticado, mas o caminho de aceitação ainda retorna às operações primitivas.

Por isso, log de atividade, roteiro de prova e sinal verde não têm a mesma autoridade que o valor admitido. Eles podem explicar o processo, mas não substituem o construtor protegido.

HOL e Isabelle herdaram partes dessa arquitetura. Não são cópias uniformes. Paulson registra que Isabelle organiza regras e estados de prova por princípios diferentes dos do LCF clássico; outros sistemas guardam termos de prova ou exportam certificados. Assistentes como Coq têm outras fronteiras. O uso de táticas, sozinho, não identifica uma arquitetura LCF.

Fontes e limites

Este artigo oferece história e análise, não uma auditoria de um provador contemporâneo nem uma contagem de código do núcleo. A associação entre uma regra comum mínima e verificável e a liberdade para decisões futuras é uma leitura editorial inspirada pelo princípio de especificação inicial mínima de Lu Heng, não uma posição institucional atribuída a Milner.