Comment le noyau fonctionne dans un prouveur de théorémisme LCF

Question

J'ai entendu dire qu'il existe un mécanisme dans les théorèmes à base de LCF qui permet uniquement certaines fonctions de créer des valeurs de théorème de type.Je crois que ceux-ci sont basés sur des types de données abstraites.

Quelqu'un pourrait-il esquisser en pseudo-code comment cela fonctionne-t-il?(dans le cas où le ci-dessus est correct)

Answer 1

Voici quelques pensées et code du noyau (fichier thm.ml à 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

Aussi ici est une citation de Paulson Book sur ML. Sur les types de fichiers abstraits qu'il dit:

Une structure modulaire facilite la compréhension d'un programme. Mieux encore, le Les modules doivent servir de pièces interchangeables: remplacement d'un module par un La version améliorée ne doit pas nécessiter de changer le reste de la. programme. Standard Les types abstraits et les foncteurs de ML peuvent nous aider à répondre également à cet objectif. Un module peut révéler ses détails internes. Lorsque le module est remplacé, d'autres Certaines parties du programme qui dépendent de ces détails échouera. Ml fournit plusieurs façons de déclarer un type abstrait et des opérations connexes, tout en cachant le type Représentation.

Vous ne pouvez donc pas instancier un type de données abstrait que vous pouvez l'utiliser (ses champs + fonctions). La question sur la manière dont vous implémentez cette fonctionnalité dépend de la langue. Si vous voulez le faire dans le Calmbda-Calculus, il devrait y avoir quelque chose comme celui du livre TapL de Benjamin Pierce sur les derniers chapitres.

Une belle référence pour cela est aussi ici .

Answer 2

Si je me souviens bien, c'était le chapitre 5 ou 6 du manuel de John Harrison de la logique pratique et du raisonnement automatisé .

JON Sterling a écrit une partie Notes Pour une récitation d'une année ou de deux dos, spécifiquement pour un prouveur de LCF utilisant un calcul séquent.