Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: reetz <reetz@ira.uka.de>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: hol90 should have more control about proofs 
In-Reply-To: Your message of "Thu, 08 Feb 1996 08:47:43 +0100."
             <"iraun1.ira.606:08.02.96.07.48.41"@ira.uka.de> 
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Thu, 08 Feb 1996 19:06:37 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <E0tkbg9-0001aS-00@bescot.cl.cam.ac.uk>


Ralf raise some very interesting points about proofs, and to what extent
a theorem prover should have proofs as first class objects.  These
are subjects that I have been giving alot of thought to, and
which I think are crucial to the usability of theorem provers.

The word "proof" is severely overloaded.  I want to make clear that
in this context we're not talking about "proof objects" 
i.e. low level representations of the sequence of 
deductions that lead to a theorem.  Instead I am interested
in the proof as the user enters it, i.e. the
tactics used to decompose the goal (in backward proof), or a
sequence of user-level opens/transformations (in window proof).
I agree that a quality theorem proving environment must provide facilities
to store and manage proofs at this level, and allow them to be 
maintained over the course of a project.

This necessitates the theorem proving assistant having more
power to manage the user's "workspace".  PVS certainly does this
better than other systems.  In HOL, the big challenge is to achieve
this and yet still deliver an open, programmable system.  

[In particular, I think programmability is most essential for 
the development of major new reasoning tools.  John Harrison's
recent work on first order automation is a good demonstration of this,
as is Richard Boulton's "arith" work.  We now know how to build
proof tools on top of LCF systems which are efficient, secure and powerful.
However, I must admit that the non-programmability of "closed" systems
allows alot more flexibility when building user support. ]

Other theorem provers regularly use other interaction languages besides
their implementation language, although their ease of programmability
sometimes suffer as a result.  Some examples:
   - Isabelle uses a special purpose language for theory descriptions.

   - PVS uses simple Lisp expressions to express proofs, and a 
     different theory language for theory descriptions.

   - Different proof styles plainly need different languages
to express them in.  John Harrison has been looking
at a new proof langauge based on Mizar.  I believe there 
is a need to support several such languages within a theorem prover.  

   - HOL already uses a special mini-language for datatype declarations.

So, in the long run I believe it would be better to 
clearly distinguish between user interaction languages and the 
implementation language.  In the short term I think this applies
expecially to theory description files - HOL should be usable as a
tool for making and investigating specification, which it clearly is
not at present.  The ability to describe theories via a theory file
format would help things alot.

Another interesting point about the use of ML as the interaction
language: Paul Curzon's wonderful "virtual theories" work largely abandons
the use of top-level ML bindings.  Paul's system assists the user by ensuring
that he/she only uses what is available in their "current scope".  
Excessive reliance on top level bindings is a curse for an interactive
theorem prover.  The use of distinct interaction languages would give
a natural place for access controls to be enforced (i.e. during the
parsing/interpretation of the interaction language).

These are "long term" thoughts.  For the moment, however, I am
considering how to enhance the primitive facilities
of HOL sufficiently to allow further experimentation with different kinds
of user environments.  


Don

-----------------------------------------------------------------------------
At the lab:							     At home:
The Computer Laboratory                                          Trinity Hall
New Museums Site                                                      CB2 1TJ
University of Cambridge                                         Cambridge, UK
CB2 3QG, Cambridge, UK
Ph: +44 (0) 1223 334688				      Ph: +44 (0) 1223 339030
http://www.cl.cam.ac.uk/users/drs1004/     
email: Donald.Syme@cl.cam.ac.uk
-----------------------------------------------------------------------------