Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Cc: Richard.Boulton@cl.cam.ac.uk
Subject: Notes from the HOL95 Workshop
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Tue, 10 Oct 1995 15:05:14 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:149700:951010140551"@cl.cam.ac.uk>

Below are notes I took at the discussion session and business meeting of the
HOL95 Workshop in Aspen Grove, Utah, on 14 September 1995. My apologies for
any inaccuracies or omissions.

Richard Boulton.

------------------------------------------------------------------------------
Richard J. Boulton, University of Cambridge Computer Laboratory,
New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom
Telephone: +44 (0)1223 334729, Fax: +44 (0)1223 334678
E-mail: Richard.Boulton@cl.cam.ac.uk, URL: http://www.cl.cam.ac.uk/users/rjb/
------------------------------------------------------------------------------

Minutes of the Discussion Session and Business Meeting at the HOL95 Workshop
============================================================================

Chaired by Tom Schubert (TS)

[Texts in square brackets are editor's remarks.]


Efficiency of HOL90 Theory Storage
----------------------------------

Steve Brackin (SB) had suggested that the theory storage in HOL90 is too big
and two slow. Regrettably, he was not able to be at the meeting.

Ralf Reetz (RR) agreed that there are problems with HOL90's theory storage.

Donald Syme (DS) said that Elsa Gunter has some ideas about this. In
particular, the mutrec library [for mutually recursive type definitions]
causes some problems because of all the constants defined by it.

RR suggested that the problem is due to there being no structure sharing.
Use of "let" terms can help.

DS reminded the meeting that he had posted some modifications to HOL90 that
reduce memory usage but not the size of theory files [info-hol 17 May 1995].
They are available on request.

Flemming Andersen (FA) said that he hadn't been able to integrate the
modifications.

DS responded that Ching-Tsun Chou had got them working.

Kelly Hall (KH) said that he liked the ASCII representation for theory files
and proposed that gzip [the GNU compression program] might be used to reduce
their size.

Wai Wong (WW) said that he had done this for the files produced by his proof
checker [see proceedings].

KH then observed that use of gzip doesn't address the low speed of parsing
theory files.

John Harrison (JH) said that he thinks theory files are bad and should be got
rid of. He suggested persistent storage as a possible alternative.

DS responded that this might make the core size too huge.

RR said that he has an example in which the memory consumption is acceptable
but the disk consumption is many megabytes. Type representation is the
problem.

DS agreed, remarking that type sharing helps in memory.

JH queried whether the type information was just stored for the leaf nodes of
terms [variables and constants].

DS said yes and expressed the belief that the problem was solvable for disk
storage.

Tom Melham (TM) remarked that the developers of HOL90 are aware of the
problem.


Single Set Theory
-----------------

DS proposed that the number of set theory libraries be reduced from three to
two, keeping the finite sets library but dropping one of the other two
[infinite sets represented either as predicates or with an explicit type of
sets].

Malcolm Newey (MN) added that Donald [Syme] thinks that the differences can be
made transparent by means of a user interface.

TS asked for reasons against dropping one of the libraries.

MN responded that there are fierce camps for both versions.

JH pointed out that there is basically no difference between the two: a type
abbreviation could be used to make the `pred_set' library look like the `set'
library. Thus, `pred_set' should be retained and `set' dropped.

TM responded that this would require polymorphic type abbreviations. They are
not trivial to implement.

Peter Homeier (PH) said that he is a heavy user of the finite sets library but
would be happy to change to another if helped.

MN replied that it wouldn't be conceptually simple to make this switch. One
gets stronger induction, etc., with finite sets.

PH said that he was confused by the set libraries when he first started so
picked the simplest.

JH remarked that there are things that should be added to all of the set
libraries.

MN responded that he had spent some time in Cambridge during which he made new
versions for HOL88. These have not been documented yet. The next job is to
port the new versions to HOL90.

TS then said that he could not see this issue being resolved.

JH said that there is a slight problem of cardinality in non-finite sets: a
"CARD s = n" assumption does not imply that s is finite, which makes the
cardinality function much less useful.

PH accepted this and agreed that the finite sets library should be retained.

DS then said that if the finite sets library is retained the names in it
should not overlap with the other set libraries. Perhaps an `F' could be put
in front of every name.

MN observed that there is an analogue of this non-overlapping name issue with
respect to natural numbers and integers.

Phil Windley (PW) said that this raises the issue of overloading.

PH asked why anyone would want both the finite sets library and one of the
other set libraries loaded at the same time.

DS cited his work on finite maps as a reason [see proceedings]. It uses
infinite sets and someone might want to use finite maps along with one of the
other set libraries.

Following some remarks on overloading by TS [sorry, got lost -- ed.] JH asked
what Isabelle uses.

DS replied that Isabelle has type classes.

JH asked how these relate to type classes in Haskell [a lazy functional
programming language].

Franz Regensburger (FR) said that Isabelle has overloading according to type
classes: there is inheritance of polymorphic functions but it is not possible
to overload the minus sign as both a binary and a unary operator; the arity
must be the same.

JH commented that computer algebra systems have implicit cast functions.

Mark Aagaard (MA) said that Carl Seger has added overloading to FL, the
language used by Voss [a combined model checker and theorem prover]. There are
drawbacks that don't come across immediately. It may be useful at times to
know which type an overloaded operator has.

TS responded, saying that with graphical user interfaces colour could be used
to indicate this.


Prototyping
-----------

Sara Kalvala (SK) had asked whether there could be quick and dirty prototyping
in HOL, but then how close would it be to the original representation? SK was
not at the discussion session.

There seemed to be general uncertainty as to what this meant, so JH asked for
clarification.

KH suggested that Sara meant some kind of weaker draft mode.

MA referred to Sara's talk. She implied that the type system in Isabelle is
looser, so concepts can be introduced faster.

TM replied that this was because the work Sara described was done in set
theory not higher-order logic. [Isabelle is a generic theorem prover that can
be instantiated with different logics.] Fast development methods are either
logically sound or not. How can the HOL community police quick and dirty
methods in private research?

MA asked whether the Isabelle features are transferable to HOL.

TM replied that HOL's type system doesn't allow it.

JH suggested it had to do with Isabelle's untypechecked terms.

FR said that in Isabelle one can introduce syntax which is transformed to
proper terms prior to type checking. It is just sugaring.

TM said this would be like having extensible preterms in HOL.

FR agreed. It has nothing to do with the logic. It is just syntax for binders,
infixes, tuples, etc.

TM said that this sounds useful.

FR agreed that it provides a nice interface and re-iterated that it is not to
do with the logic.

TM asked if anyone has a spare student to work on this.


Why is a Proof Checker Useful?
------------------------------

This question had been raised by RR following Wai Wong's talk and been
deferred. RR said that the question had been resolved [see proceedings].


Taxonomy of Goals / Frequently Asked Questions
----------------------------------------------

Paul Black (PB) claimed that there seem to be different types of goal. Some
have lots of assumptions, for example. Has anyone noticed these types?

FA said that he had noticed similar goals within [a verification of ?] the
same algorithm. Similar proof obligations appear again and again.

TM said that he thinks there are two levels. Kinds of goals are distributed
like kinds of animals in different countries. The kinds of goals that appear
depend on the application or theory. So a general list is probably not useful.
It may be more useful to identify kinds of goals for particular fields, e.g.
for microprocessor proofs the techniques to use are now well known. The
knowledge of how to handle goals in other areas will emerge slowly.

PB asked if there are any classes of goal that aren't subject specific.

RR replied that having lots of assumptions vs using conditional rewriting
might be an example. This is a question of style. However, HOL does not
currently have conditional rewriting. [Actually, there are some conditional
rewriting tools -- ed.]

PB asked RR if there are problems where he knows he will run into this issue.

RR responded, "When using resolution."

MA said that it is difficult to recall kinds of goals on the spot. Perhaps PB
could collect notes. When people realise they have identified a certain kind
of goal they could notify PB (or whoever is collating the information).

PW pointed out that lots of things like that would help new users, e.g. what
to do when an equality in an assumption is in the wrong direction to use as a
rewrite rule. It is not in the HOL documentation.

TM replied that this is true but such questions have been answered on the
info-hol mailing list. Sometimes the answer is to reformulate the goal, so a
cook-book method is not always right. For example, problems with the epsilon
operator are often like this.

PW said that such help is best given in person. It is often necessary to sit
with the user having the problem.

PB suggested that the wisdom be collected as case studies.

FA recalled that Brian Graham has written a paper on dealing with the epsilon
operator.

TM confirmed this and said that it is in the contrib area of the HOL
distribution [http://www.cl.cam.ac.uk/ftp/hvg/contrib/select/]. He also said
that he once tried to build a cook book but didn't keep it up.

PB suggested these things be looked at as small case studies.

PW observed that a lot of useful information could be collected by distilling
the info-hol mailing list.

TM agreed. There are some good stories in the info-hol archive on how to solve
certain problems.

Paul Curzon (PC) asked whether it would be useful to have a database of small
tactics to do things? In contrib? There is currently no mechanism for sharing
tactics except info-hol.

PW said that years ago he started a FAQ [Frequently Asked Questions list] for
error messages. There are about 9 or 10 entries and they are available on the
Web site [http://lal.cs.byu.edu/lal/hol-errors.html].

PC asked if the Web site was the best place for these. They need to be more
widely distributed than just a site in the USA because the link across the
Atlantic is heavily loaded.

It was agreed that it would be possible to mirror the information at other
sites.

PW took the opportunity to make an announcement regarding the search facility
at the Brigham Young University Web site. Version 2 is installed but it is not
possible to mirror it. It is possible to mirror Version 1 though. Version 3 is
under development and it should be possible to mirror it fairly easily.

PC said that it should be easy enough for new users to do.

PW replied that it is not necessary for every HOL user to have a local copy
but only certain, well distributed sites. That's the purpose of the network.

PC argued that the network could be too slow.

PW responded that having the information at more sites will solve the problem.

TS then closed the discussion by asserting that it had become one on problems
with the Internet.

PB suggested that part of the entrance fee for the 1996 Workshop should be a
word of HOL wisdom.


User Interfaces
---------------

Holger Busch (HB) started the discussion by asking about user interfaces for
particular applications. He asserted that a lot of the details can be hidden
from users.

TM said this was an interesting issue but that he wouldn't get into it. Donald
Syme is proposing to look at it as part of his PhD work.

DS said that this was the current plan. He wants to build systems with HOL as
a proof engine.

TM said that this was not the same problem as arbitrary user interface issues.

DS said that he would be investigating particular examples.

Francisco Corella (FC) asked if it was a good idea to hide the logic.

HB said he thought that for applications interaction can be at a different
level to when using the logic directly.

TM said that levels cannot be hidden. They can only be made to coincide.

FC thought that an interface could be made more specific to a problem domain.

DS cited window inference as an example. He also said that he doesn't think
HOL currently makes a good proof engine because of the ML systems used to
build it. HOL should be compilable in Caml Light, etc. Want to be able to
compile with C. Want HOL not to eat up all of the memory.

PH asked how this could be achieved.

DS replied that it could be done using an ML to Caml translator or by
co-operating with Moscow ML.

JH remarked that a new version of Caml Light has just been announced that has
a more sophisticated module system than previous versions.

TM thought that the porting exercise could be solved with money.

JH agreed, saying that it was pretty trivial apart from the interface.

Morten Welinder (MW) observed that the quotation mechanism is not
standardised.

JH said that the Standard ML of New Jersey (SML/NJ) quotations are not
optimal. They could be done another way. Quotations aren't Standard ML anyway.

MW thought that Caml would have to be changed.

JH replied that there is a quotation mechanism in Caml Light but it may not be
what people want.

TM requested that someone hire a student to do this work.

DS thought that support for multiple platforms should be built in from the
start.

TM said that Konrad Slind had aimed at system independence with HOL90.

JH asked why it is system dependent.

DS suggested that it was because of bad input/output primitives in The
Standard, e.g., it is not possible to find out whether or not a file exists.

MW thought that quotation, I/O, and pretty-printing were the only non-standard
features used by HOL90.

MN asked how many architectures SML/NJ works for.

PW said that there are advantages to SML but Lisp is universally available.
Lisp is ported to new systems more quickly than SML/NJ is. There are companies
with a vested interest in Lisp but only the theorem proving community has a
real interest in SML and we are small. We could find ourselves dependent on
AT&T Bell Labs. [the developers of SML/NJ], and they have only finite
resources.

TM responded that, in principle, different ML systems can be used for HOL.

FR said that Isabelle can be used with various ML systems. The problem is one
of how to construct the basic libraries.

PW recalled that John Carroll made HOL88 portable across several Lisps by
constructing appropriate basic libraries.


A Comment Regarding the HOL2000 Initiative
------------------------------------------

TM observed that there has been discussion about the HOL2000 initiative
[http://lal.cs.byu.edu/lal/hol2000/hol2000.html] on the mailing list but
nothing has actually happened. We need someone to do something. He then
announced that he is. However, he didn't want to appear to be hijacking the
initiative and so would like to inform the community about what he is doing.
He is trying to get money for a project to do some of the things that have
been discussed. He has a grant proposal submitted to do immediate work and
some new research. There is also a group looking for a Framework IV programme
(European Union) project. This involves European sites only but it is not an
attempt by European sites to run away with HOL2000. The group involved is keen
to work with everyone. Getting funding from Framework IV is a long shot.
*There is no money yet*. The main HOL sites in Europe are involved. They will
look into formal collaboration with other countries.


Form of the 1996 Workshop
-------------------------

The 1996 HOL Workshop [http://www.abo.fi/~jwright/hug96.html] will be held in
Turku, Finland from 26 to 30 August. The proposed duration is 3.5 days, or
4.5 days if there are tutorials.

It has been suggested that the 1996 workshop be a truly general higher-order
logic theorem proving conference. The idea would be to more actively encourage
other communities to participate. One day could be split into separate user
groups. Also, there could be tutorials.

PW suggested that there be three emphases:
 * Interactivity
 * Higher-order logic
 * LCF-style
The forum would be open to theorem proving research that involved at least two
of these categories. We want peripheral papers but not too far out of scope.
At least four members of the programme committee would be chosen from the
communities of other theorem provers.

JH thought this was perfect.

PC suggested the name be changed. In particular that the workshop/conference
be called "The 1st ...".

TM disagreed, on brand-recognition/marketing grounds.

PW thought the name was general enough now. But perhaps a new logo? HOL96 can
mean other things than "the HOL theorem prover".

PC argued that it was a question of how other people actually perceive the
conference, not how we want it to be perceived.

PW believed that having enough members on the programme committee from other
systems would create the right perception.

TM said that we want to preserve the good things about the meeting as it
stands, e.g. the open venue [allowing "work in progress" and the like to be
presented].

RR suggested that some members of the programme committee be from application
areas as well as from other theorem provers.

TM argued that to be the case already.

PW thought that we shouldn't pick someone out of the scope of the conference
just because they were involved in an application area.

PC suggested that in the longer term we encourage a non-HOL site to host the
meeting.

PW thought that would happen naturally from having appropriate programme
committee members.

TM said that there would be lots of papers to referee and therefore proposed
that the size of the programme committee be increased.

TS said he thought that had been done this year.

There was then a vote at which the proposals outlined by PW for a wider-scope
workshop in 1996 were given the approval of the meeting.

PB asked about the future of theorem proving for formal methods and said that
this would be interesting to address.

KH said that we should ask other communities whether they actually want to
work with us.

TM responded that informal contacts had already been made.


Summary of People's Initials
----------------------------

DS   Donald Syme, University of Cambridge
FA   Flemming Andersen, Tele Danmark Research
FC   Francisco Corella, Hewlett-Packard
FR   Franz Regensburger, Technical University Munich
HB   Holger Busch, Siemens AG
JH   John Harrison, Abo Akademi University
KH   Kelly Hall, Brigham Young University
MA   Mark Aagaard, University of British Columbia
MN   Malcolm Newey, Australian National University
MW   Morten Welinder, University of Copenhagen
PB   Paul Black, Brigham Young University
PC   Paul Curzon, University of Cambridge
PH   Peter Homeier, University of California at Los Angeles
PW   Phil Windley, Brigham Young University
RR   Ralf Reetz, University of Karlsruhe
SB   Steve Brackin, Arca Systems, Inc.
SK   Sara Kalvala, Warwick University
TM   Tom Melham, University of Glasgow
TS   Tom Schubert, Portland State University
WW   Wai Wong, Hong Kong Baptist University