Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
To: info-hol@dworshak.cs.uidaho.edu
Subject: Re: numerals by pretty printer instead by num_CONV?
In-Reply-To: Your message of "Wed, 25 Aug 93 16:49:59 BST." <17891.9308251550@frogland.inmos.co.uk>
Date: Wed, 25 Aug 93 17:23:51 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:229940:930825162405"@cl.cam.ac.uk>


David Shepherd writes:

| 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.

This seems a reasonable compromise, since it's quite easy to get addition
right. I think ICL ProofPower adopts this solution.

| 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!

It would require serious thought before installing such a thing and using it in
HOL. You have to assess carefully whether it is a serious carefully written
package or bug-infested garbage from some talentless hacker. In a language
which is supposed to have a well-defined semantics, the use of machine
arithmetic is absurd. Any nontrivial program verification is going to be
littered with details about the ranges of numbers.

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

I don't know exactly. None of the polynomial normalization stuff was well
written. But I am sure it would make a dramatic difference, the difference
between practical and impractical.

John.