Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Cc: annap@edu.uiuc.cs.ganges
In-Reply-To: Gavan Tredoux's message of Thu, 18 Feb 1993 22:01:58 +0100 <9302182101.AA12105@elc.mth.uct.ac.za>
Subject: Completeness proofs
Message-Id: <93Feb19.011111met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 19 Feb 1993 01:11:06 +0100


Gavan Tredoux writes, in reference to a planned embedding of the
Mason-Talcott calculus:

> How do you plan to set about this? I don't think this is going to
> be easy. There is a more general problem here: embedding logics
> within HOL, eg programming logics. These all do mostly the same thing,
> eg. need propositions of some sort, which are usually modelled as
> *predicates* in the HOL logic with the propositional operators
> like /\ lifted to the level of predicates.

I wouldn't be so pessimistic; the Mason-Talcott calculus is quite small,
allowing the inference of only two kinds of assertions: program
equivalence (e0 = e1) and program divergence. Mason and Talcott have
already given a reasonably formal presentation of the syntax and
semantics of the language, now "all" one has to do is mechanize that
work. This is straightforward but by no means trivial, assuming that
they have made no mistakes! As a datapoint, one has Myra VanInwegen's
work on formalizing the syntax and dynamic semantics of CoreSML last
summer; this was done over the course of two and a half months, by a
complete HOL novice, and part of that time was spent in writing a mutual
recursive type definition package with Elsa Gunter. CoreSML is *much*
larger than the language of Mason&Talcott.

I imagine that transcribing the meta-theory (e.g., Mason&Talcott's
completeness proof) would also be relatively straightforward, but that
reasoning about specific programs would be unbelievably painful without
language-specific parser and prettyprinter support.

My main point is that the hard work in embedding an object logic in any
logic lies in proving theorems either in or about it, not in
user-interface issues. (That is, provided one has facilities for
inductive definitions and recursive types. Without those, it is a hard
struggle!)

> Maybe it would be useful to set up some generic methods for embedding
> logics in HOL. The ideas used in Isabelle may be useful here.

I agree with this. One can't help thinking that higher-order unification
would be useful in HOL :). 

Konrad.