Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 22 Aug 1995 10:00:41 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA034171306;
          Tue, 22 Aug 1995 02:48:26 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA034051241;
          Tue, 22 Aug 1995 02:47:21 -0600
Received: from ira.uka.de (actually i80s16.ira.uka.de) by iraun1.ira.uka.de 
          with SMTP (PP); Tue, 22 Aug 1995 10:33:30 +0200
X-Mailer: exmh version 1.5.3 12/28/94
To: John Harrison <John.Harrison@cl.cam.ac.uk>
Cc: hol2000@leopard.cs.byu.edu
Subject: Re: Paper available: "HOL Done Right"
In-Reply-To: Your message of "Mon, 21 Aug 1995 15:40:38 BST." <"swan.cl.cam.:251800:950821144045"@cl.cam.ac.uk>
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 22 Aug 1995 10:30:35 +0200
From: reetz <reetz@ira.uka.de>
Message-Id: <"iraun1.ira.944:22.08.95.08.33.35"@ira.uka.de>

> All comments welcome, though I don't have much time for discussions right now.
>
> John.

I have read the paper. It sounds really great. Just four comments (rather than
a discussion as I don't have the time either): you have extensively discussed 
a pretty much better representation for natural number ``constants''.
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 :-(.
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.
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.
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).

Ralf.

(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*  fax:    +49 721 370455                                         *)
(*  tel:    +49 721 6083771                                        *)
(*                                                                 *)
(*******************************************************************)