Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
To: reetz <reetz@ira.uka.de>
Cc: hol2000@leopard.cs.byu.edu
Subject: Re: Paper available: "HOL Done Right"
In-Reply-To: Your message of "Tue, 22 Aug 1995 10:30:35 +0200." <"iraun1.ira.944:22.08.95.08.33.35"@ira.uka.de>
Date: Tue, 22 Aug 1995 12:59:28 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:119490:950822115936"@cl.cam.ac.uk>


Hi Ralf,

Thanks for your comments. Despite pretending I don't have time for much
discussion:

| 1) What about integers? Can this scheme be applied to signed integers as
| well? Signed integers are often used and the current implementation in
| HOL90 is in my very personal point of view not very handy, as I had to
| discover myself :-(.

Yes, the approach, including the use of rewrites for arithmetical calculation,
easily extends to integers. By the way, there is an alternative integers theory
which you may find suits you better. There's no hol90 version, but the only
files with real code in them, namely "equiv.ml" and "useful.ml", are already
ported to hol90 in the reals library. You can FTP it from "ftp.cl.cam.ac.uk"
as "hvg/contrib/int/int.ml".

| 2) What about ARITH_CONV and some similiar decision procedures with this
| scheme? In comparsion with other theorem provers, HOL90 really needs more
| automatic proving facilities. E.g. there's is no version of ARITH_CONV for
| integers.

I worked on the analog of ARITH_CONV for the reals (in fact as part of my
thesis writeup, I am about to exhume it and get it running). Using the obvious
injection Z->R, one can thus get trivially those universal theorems about Z
which also hold for R (in fact, if I understand Richard's work correctly, these
are exactly the ones his variable-elimination procedure proves anyway, i.e. it
does not prove theorems which depend on discreteness). One could even get
something like Richard's package for N as a byproduct, though it'd probably be
markedly less efficient. I believe someone at BYU is contemplating writing an
arithmetic procedure for Z directly.

| 3) Does the new mutual recursive definition scheme need significantly less
| memory? E.g. in one of my first versions of a grammar for ``my'' subset of
| VHDL, I needed more than 600 MB heap size to define the types with "mutrec"
| because of a bunch of mutual recursions.

This part of the implementation is still in flux and currently doesn't work
properly; when I've got my thesis out of the way, I'll rewrite it. I believe
that it may require less time and memory, but that's largely guesswork. I've
kept the example you sent me a few months ago to stress-test it when it works
better.

| 4) In general, as some people (like me) try to use HOL for ``real-world''
| problems (but real-world is a VERY questionable term, I do know), concrete
| speed and memory consumptions (what about a benchmark set for HOL-systems??)
| in comparison with existing LCF-style theorem provers are often of more
| interest than more theoretical elegance (if theoretical elegance leads to more
| efficient systems, the better, of course).

Yes, I agree. This wasn't my prime concern in the work I describe, though I
tried to make operations like "subst" as fast as I could. Part of the slowness
of HOL isn't due to its being LCF-style, but the fact that it's not written in
C or LISP, for which faster compilers are available. As SML/NJ and other ML
implementations develop, I believe the gap will be closed significantly.

John.