Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <17891.9308251550@frogland.inmos.co.uk>
Subject: Re: numerals by pretty printer instead by num_CONV?
To: info-hol@dworshak.cs.uidaho.edu (info-hol mailing list)
Date: Wed, 25 Aug 1993 16:49:59 +0100 (BST)
Cc: info-hol@dworshak.cs.uidaho.edu
In-Reply-To: <"swan.cl.cam.:214940:930825153021"@cl.cam.ac.uk> from "John Harrison" at Aug 25, 93 04:30:13 pm
Content-Type: text
Content-Length: 3315

[[ n.b. I sent a reply earlier, but forgot that info-hol is set up
   so that (R)eplies go back to the sender only and not the list!
]]

John Harrison has said:
> Ralf Reetz writes:
> 
> > So, why shouldn't the pretty printer print SUCs as natural number constants
> > and leave the original term as it is? I myself don't have enough knowledge
> > about the code of HOL90.5 to do the fix, but maybe anybody else cares or
> > has already cared?
> 
> I agree quite strongly with the idea in principle. (I think this is what
> Isabelle does -- someone will no doubt correct me if I'm wrong.) However if
> making such a change I would prefer to implement numerals in a binary (or other
> positional) notation, e.g.
> 
>    2 prettyprints "NUMERAL [T; F]
> 
>   15 prettyprints "NUMERAL [T; T; T; T]
> 
> (SUC would still exist as before but num_CONV would become a derived rule.)
> 
> The advantages would be:
> 
> * One could do arithmetic with large numbers inside the logic, reasonably
>   quickly, which I think is important[%].

I've been developing some theory of word types based around hex-digits
and arithmetic is pretty fast! (Well certainly compared with adding 2 32bit
values using ADD_CLAUSES!)

Also, on the subject of fast arithmetic - I think theres a case, certainly
for many purposes, for making ADD_CONV into a hard coded routine. After all,
mk_thm is used in many derived rules already for efficiency. It really is
quite simple, and doesn't even need to depend on the underlying arithmetic
implementation as you can do digit arithmetic by lookup tables on
explode numeric strings.

> * It wouldn't use |mk_thm|. This is perhaps largely an academic point since the
>   LISP bignums are probably no less reliable than other critical code. However
>   hol90 under SML/NJ is stuck with machine arithmetic, so num_CONV is useless
>   for large numbers (surely one of the stupidest decisions by the SML
>   designers).

though with SML you can easily write your own bignum package - you could probably
even prove the algorithms in HOL! I asked on comp.lang.ml if any such packages
were available and with 24 hours I'd been sent 3!
 
> * One could implement words in a very similar way, again avoiding |mk_thm|.
> 
> The disadvantages would be:
> 
>  * num_CONV would probably be slower, and in general terms would be larger.
> 
>  * Some existing code probably depends on the fact that numerals are really
>    constants.
> 
>  * To define the arithmetic operations you need list recursive definitions, and
>    to get that far you would need to use explicit |SUC|s in the arithmetic
>    theorems required, then rewrite them retospectively.
> 
> John.
> 
> [%] See for example my paper with Laurent Thery (from this year's HOL meeting)
> on linking HOL and Maple. The cringe-making benchmarks for big trigonometric
> integrals can largely be laid at the door of slow arithmetic.

how much better would making ADD_CONV "efficient" make these figures?

--
--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley