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
In-Reply-To: <9406081532.AA10246@switha.dcs.gla.ac.uk> (tfm@dcs.gla.ac.uk)
Subject: Re: Alternate Subgoal Package / Natural Deduction.
Message-Id: <94Jun12.183554met_dst.8079@sunbroy14.informatik.tu-muenchen.de>
Date: Sun, 12 Jun 1994 18:35:49 +0200


Terminological note: the word "tactic" in each system is being used for
ML functions with completely different types: in LCF/HOL a "tactic" is
an ML function with type

    goal -> goal list * validation

while, for instance, in Isabelle, a "tactic" is basically an ML function
with type

    thm -> thm sequence.

In Isabelle, a thm is used to represent the state of the proof, and
application of a tactic produces a stream of alternative proof states
(the stream is necessary because higher-order unification can return
more than one "answer").  In ProofPower, I surmise that the type would
be something like "thm -> thm".

The weakness of tactics in LCF/HOL due to validity checking is blameable
on the weakness of the ML type system (as I found when implementing
hol90, as many others have no doubt also noticed, and as has been
recently explored by Randy Pollack in the context of using Type Theory
to accurately specify tactics).  The correctness of a tactic is not
ascertainable in ML-style typing. Recall that the application of tactic
T to goal g gives some subgoals [SG1, ..., SGn] and a validation
function "f : thm list -> thm". This fails to capture the following
requirements:

    1. The number of subgoals needs to be identical to the length of the
       argument list to f (this is checked, believe it or not, at runtime);

    2. SGi must be aconv with the concl of the ith thm in the argument
       to f, for each i in 1..n (this isn't even explicitly checked
       unless you make a call to VALID, which is flawed as others have
       pointed out).

So it can be argued that ML, while being a good language for encoding
proof systems in, is not an entirely satisfactory language for writing
tactics in, at least as tactics are defined in LCF/HOL.

The proof state encodings of Isabelle, ProofPower, LAMBDA and others
gets the job done wrt eliminating the checking of validity of tactics,
but I imagine that they are difficult to explain to new users (or even
experienced ones). Furthermore, I don't take it as a virtue that
alpha-convertible goals may get silently solved, since the existence of
such is often a clue that one is doing something wrong.

Also, if we consider consider supporting a nuPRL-style proof tree
interface to backwards proof, notice that the simple structural criteria
for being done, i.e., that the assumptions of the "proof state" are
empty, no longer applies, since the entire fringe of the proof tree must
be scanned to see that there are no more unsolved goals. Validity
checking, it seems to me, then becomes necessary again.

There are at least four different notions of what a tactic is, so we
have to be careful about what we are talking about. For me, the
proof-interface issues in HOL2000 won't be so much in deciding what
*the* best interface to backwards or forwards proof is, but rather in
how to coherently integrate many different ideas of what a proof is.
Some ideas about this can be found in my paper on proof management in
the upcoming HOL workshop.

Konrad.