Hi Ken, | John's e-mail on the motivation for HOL Light and his comparison with | Andrews' systems is highly interesting. I would suggest an article "On the | Logical Foundations of HOL Light" or similar to make the information | persistent, as the policy of the mailing list provider may change. For now, | I have quoted from the publicly available e-mail via the online link.
I am glad you found it interesting. Indeed, I don't think I've ever written a detailed canonical description of the HOL Light foundations, though there are brief summaries scattered in various places, so this is certainly something to think about. On the history of HOL Light and related systems, in addition to those you have already discussed, let me shamelessly plug a book chapter written by Josef Urban, Freek Wiedijk and myself on the history of interactive theorem proving in general. This in particular discusses LCF and its successors, especially HOL, in section 3, complete with another little "family DAG" of HOL systems on page 19: http://www.cl.cam.ac.uk/~jrh13/papers/joerg.html Also of historical interest may be my old unpublished note "HOL Done Right": http://www.cl.cam.ac.uk/~jrh13/papers/holright.html That describes an intermediate stage in the evolution of HOL Light when the logical kernel still had implication as a primitive. The setup described there is also of some relevance to the discussion of type definition principles in a related thread, because it sketches what (as Rob notes in his paper) was the first version of a definitional principle that is roughly a "unary" version of his own idea. At the risk of reiterating what you can read in Rob's paper, let me explain my motivations there. Roger Jones gave an excellent description of the origins of what in HOL88 were called "new_definition" (a simple |- c = t binding) and "new_specification" (introducing constants satisfying a predicate given an existential theorem). One more perceived rough edge in HOL88 and hol90 that I wanted to fix in HOL Light was that there should indeed be two completely different definitional principles when they are tantalizingly close to being interderivable: * Since |- exists x. x = t is clearly provable, one can derive "new_definition" fron "new_specification". There is however a bootstrapping problem because "new_definition" is used to define the existential quantifier on which "new_specification" depends! * Once the epsilon operator is present, one can easily derive "new_specification" from "new_definition", but only with the motivating drawback mentioned by Roger Jones that you get "too much information" about the introduced constants. In the early versions of HOL Light I chose the slightly different approach of taking as primitive a variant of "new_specification" that allowed one to introduce a new constant c and a theorem |- P[c] given an input theorem |- P[t] for a specific term t, not |- exists x. P[x] as in "new_specification". Then no quantifiers are involved, and "new_definition" is a trivial instance because of reflexivity |- t = t, while "new_specification" can be derived from the epsilon operator without exposing too much information. One needs of course some restrictions on variables and type variables analogous to those Roger discussed. (Amusingly, I too got them wrong in the first instance, as Tom Melham spotted instantly when I first showed him the code. This was long before HOL Light was a public system.) At some point I switched HOL Light back to the simple |- c = t "new_definition" because it seemed slightly simpler and more intuitive, and I have personally never been very interested in the "too much information" problem (I generally want to define things explicitly, not leave them underspecificed). I can quite well see the arguments for Rob's version though. John. ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
