1
$\begingroup$

I heard that there is some mechanism in LCF-based theorem provers that only allows some functions to create values of type theorem. I believe these are based on abstract data types.

Could someone sketch in pseudo-code how does this work? (in case the above is correct)

$\endgroup$
  • $\begingroup$ Are you familiar with abstract data types from the ML family of languages? $\endgroup$ – Andrej Bauer Feb 22 at 23:29
1
$\begingroup$

Here are some thoughts and code from the kernel (file thm.ML in Isabelle/Pure) from 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

Also here is a quotation of from Paulson book on ML. About abstract datatypes he says:

A modular structure makes a program easier to understand. Better still, the modules ought to serve as interchangeable parts: replacing one module by an improved version should not require changing the rest of the. program. Standard ml's abstract types and functors can help us meet this objective too. A module may reveal its internal details. When the module is replaced, other parts of the program that depend upon such details will fail. ML provides several ways of declaring an abstract type and related operations, while hiding the type's representation.

So you cannot instantiate an abstract datatype you can use it (its fields + functions). The matter on how you implement this feature is very of dependent of the language. If you want to do it in the lambda-calculus, there should be something like that in Benjamin Pierce's TAPL book on the later chapters.

A nice reference for this is also here.

| cite | improve this answer | |
$\endgroup$
1
$\begingroup$

If I recall correctly, this was chapter 5 or 6 of John Harrison's Handbook of Practical Logic and Automated Reasoning.

Jon Sterling wrote some notes for a recitation a year or two back, specifically for an LCF prover using sequent calculus.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ thank you for sharing, those are very good references $\endgroup$ – Rodrigo Mar 29 at 11:50
  • $\begingroup$ thank you for sharing, those are very good references $\endgroup$ – Rodrigo Mar 29 at 11:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.