Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 25 Aug 1993 16:37:11 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02317; Wed, 25 Aug 93 08:30:26 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA02313; Wed, 25 Aug 93 08:30:24 -0700 Received: from albatross.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 25 Aug 1993 16:30:18 +0100 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 09:10:23 +0700." <"iraun1.ira.703:25.07.93.07.08.10"@ira.uka.de> Date: Wed, 25 Aug 93 16:30:13 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:214940:930825153021"@cl.cam.ac.uk> 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[%]. * 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). * 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.