Come funziona il kernel in un teorema LCF Prover

Question

Ho sentito che esiste un meccanismo nei fornitori di teoremi basati su LCF che consente solo alcune funzioni di creare valori di teorema del tipo.Credo che questi siano basati su tipi di dati astratti.

Qualcuno potrebbe schizzare in pseudo-codice come funziona?(nel caso in cui quanto sopra sia corretto)

Answer 1

Ecco alcuni pensieri e il codice dal kernel (file thm.ml in Isabelle / Pure) da 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

.

Anche qui è una citazione di Paulson Book su ML. Informazioni sui tipi di dati astratti che dice:

.

Una struttura modulare rende un programma più facile da capire. Meglio ancora, il I moduli dovrebbero servire come parti intercambiabili: sostituzione di un modulo da parte di un La versione migliorata non dovrebbe richiedere il cambiamento del resto del. programma. Standard I tipi e i funttori astratti di ML possono aiutarci a soddisfare anche questo obiettivo. Un modulo può rivelare i suoi dettagli interni. Quando il modulo è sostituito, altro Parti del programma che dipendono da tali dettagli falliranno. Ml fornisce diversi modi di dichiarare un tipo astratto e le relative operazioni, mentre nasconde il tipo Rappresentanza.

Quindi non è possibile istanziare un tipo di dati astratto, puoi usarlo (i suoi campi + funzioni). La questione su come implementare questa funzione è molto dipendente dalla lingua. Se vuoi farlo nel calcolo della Lambda, ci dovrebbe essere qualcosa del genere nel libro Tapl di Benjamin Pierce sui capitoli successivi.

Un bel riferimento per questo è anche qui .

Answer 2

Se ricordo correttamente, questo era il capitolo 5 o 6 del manuale di John Harrison della logica pratica e del ragionamento automatico .

Jon Sterling ha scritto alcuni note Per una recitazione un anno o due indietro, in particolare per un valorizzazione LCF utilizzando il calcolo di sequenti.