Como o kernel funciona em um provador de teorema LCF

Question

Ouvi dizer que existe algum mecanismo nos provadores de teoremas baseados em LCF que permite apenas que algumas funções criem valores do tipo teorema.Acredito que estes sejam baseados em tipos de dados abstratos.

Alguém poderia esboçar em pseudocódigo como isso funciona?(caso o acima esteja correto)

Answer 1

Aqui estão algumas idéias e códigos do kernel (arquivo thm.ML em Isabelle/Pure) de Isabelle:

abstype thm = Thm of
 deriv *                        (*derivation*)
 {cert: Context.certificate,    (*background theory certificate*)
  tags: Properties.T,           (*additional annotations/comments*)
  maxidx: int,                  (*maximum index of any Var or TVar*)
  shyps: sort Ord_List.T,       (*sort hypotheses*)
  hyps: term Ord_List.T,        (*hypotheses*)
  tpairs: (term * term) list,   (*flex-flex pairs*)
  prop: term}                   (*conclusion*)
and deriv = Deriv of
 {promises: (serial * thm future) Ord_List.T,
  body: Proofterm.proof_body}
with

Também aqui está uma citação do livro de Paulson sobre ML.Sobre tipos de dados abstratos, ele diz:

Uma estrutura modular torna o programa mais fácil de entender.Melhor ainda, os módulos devem servir como partes intercambiáveis:Substituir um módulo por uma versão aprimorada não deve exigir alterar o restante do.programa.Os tipos e funções abstratos da ML padrão também podem nos ajudar a atingir esse objetivo.Um módulo pode revelar seus detalhes internos.Quando o módulo é substituído, outras partes do programa que dependem de tais detalhes falharão.O ML fornece várias maneiras de declarar um tipo abstrato e operações relacionadas, enquanto oculta a representação do tipo.

Portanto, você não pode instanciar um tipo de dados abstrato, você pode usá-lo (seus campos + funções).A questão de como você implementa esse recurso depende muito da linguagem.Se você quiser fazer isso no cálculo lambda, deve haver algo assim no livro TAPL de Benjamin Pierce nos capítulos posteriores.

Uma boa referência para isso também é aqui.

Answer 2

Se eu me lembro corretamente, este foi o capítulo 5 ou 6 do manual da lógica prática de John Harrison e do raciocínio automatizado

.

jon sterling escreveu alguns notas Para uma recitação por ano ou duas costas, especificamente para um provador de LCF usando cálculo sequence.