Cómo funciona el kernel en un Prover Thorem LCF

Question

Escuché que hay algún mecanismo en los ProVers teoremas basados en LCF que solo permite que algunas funciones creen valores de tipo teorema.Creo que estos se basan en tipos de datos abstractos.

¿Podría alguien dibujar en el pseudo-código cómo funciona esto?(En caso de que el anterior sea correcto)

Answer 1

Aquí hay algunos pensamientos y código del kernel (archivo thm.ml en isabelle / puro) desde 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

También aquí hay una cotización de Paulson Book en ML. Sobre los tipos de datos abstractos, dice:

Una estructura modular hace que un programa sea más fácil de entender. Mejor aún, el Los módulos deben servir como partes intercambiables: reemplazando un módulo por un La versión mejorada no debe requerir cambiar el resto de la. programa. Estándar Los tipos abstractos de ML y los funcores pueden ayudarnos a satisfacer este objetivo también. Un módulo puede revelar sus detalles internos. Cuando se reemplaza el módulo, otro Las partes del programa que dependen de dichos detalles fallarán. ML proporciona varios Formas de declarar un tipo abstracto y operaciones relacionadas, mientras oculta el tipo representación.

Para que no pueda crear una instancia de un tipo de datos abstracta, puede usarlo (sus campos + funciones). El asunto sobre cómo implementa esta función es muy dependiente del idioma. Si quieres hacerlo en el lambda-cálculo, debería haber algo así en el libro Tapl de Benjamin Pierce en los capítulos posteriores.

Una buena referencia para esto también es aquí .

Answer 2

Si recuerdo correctamente, este fue el Capítulo 5 o 6 del Manual de John Harrison de Logic Prácticas y el Razonamiento Automático .

Jon Sterling escribió un poco Notas Para una recitación de un año o dos de vuelta, específicamente para un ProVer LCF usando Cálculo Seciente.