Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: hol2000@leopard.cs.byu.edu
Subject: Basic changes
Message-Id: <94May24.161719met_dst.8129@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 24 May 1994 16:17:06 +0200


If we are going to talk about changes to HOL, some of the most
significant changes might be in the logic and its relationship to its
metalanguage. How about the following characterization as a basis for
discussion?


	     CURRENT SYSTEM
            ****************

    hol_type: first order terms (with variables)

    term: a simply typed lambda calculus, built over hol_type.

    thm: A "thm" is an abstract type represented by pairing a term
         list with a term; free type variables in a thm are implicitly
         universally quantified. The primitive rules of the logic
         suffice to generate all derived inference rules, by using ML
         to compose existing rules. The collection of primitive rules is
         somewhat ad-hoc.

    PoD: principles of definition, to introduce abbreviations for types
         and terms.

    theory: A collection of hol_type constants, term constants,
            axioms, definitions, and theorems.


IMHO, there could be some interesting changes made:

    - hol_type: allow finer distinctions to be made, e.g., Tom
      Melham's type quantification work (this would be implemented
      in the datatype of terms, but direct modifications to the type
      system should also be considered). 
 
    - term: a more detailed (and hence more efficient) lambda-calculus, 
      perhaps with pairing or records "built-in"; 

    - thm: give a more well-rounded basis to the logic, e.g., adding
      the rules for universal generalization and specialization (GEN and
      SPEC) to the core. Computational aspects might be worth
      considering, e.g., a rewriting primitive incorporating matching 
      wouldn't be much more complex than the current substitution
      primitive and would presumably speed up this heavily-used proof
      procedure. An issue here would be satisfying the desire that all
      primitive rules terminate.

    - PoD: I'm not knowledgeable enough about logic to make a comment,
      but I'm generally in favour of deriving principles of definition
      from simple primitive ones, as is done now. Are there
      counterexamples where a derived PoD is too slow?

    - theory: This may be more pertinent to implementations, but
      anyway: the current notion of theory is barely adequate for
      current use, and is not flexible enough to build a really ace
      theorem proving environment on top of.

What I would not change would be the basic decision made in LCF to have
a "thm" ADT and use ML composition to build derived rules. For me, that
has a compelling simplicity.

Konrad.