Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Message-Id: <9308251831.AA01276@easynet.crl.dec.com>
Date: Wed, 25 Aug 93 14:32:10 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" <leonard@ricks.enet.dec.com>
To: info-hol@dworshak.cs.uidaho.edu
Apparently-To: info-hol@dworshak.cs.uidaho.edu
Subject: Re: numerals by pretty printer instead by num_CONV?

> So, why shouldn't the pretty printer print SUCs as natural number constants
> and leave the original term as it is? 

There are several issues here, of which I'd like to address two:

    1.  In what form should numbers be represented while they're being
	manipulated in a proof?

    2.  In what form should users read and write numbers?

I will assume that the parser should accept the second form and produce the
first, and the pretty-printer should accept the first and produce the second,
and that hol will not generally support other representations, but other (read
"worse") arrangements are possible, and you may want to think about it before
accepting the assumption. 

Since my opinions about these are determined by the first issue, I'll address
it first.  I'm doing proofs about Alpha, and the first time I needed to add two
64-bit numbers in HOL, I realized I needed something more than REDUCE_CONV. 
After giving the problem some thought, I implemented a library for numeral
arithmetic (where a numeral is a list of digits in a given radix).  With the
numeral library, HOL88 can (slowly but automatically) convert numbers in the
current (SUC) representation to and from numerals in any radix greater than 1,
and can quickly and automatically simplify expressions built up of numerals
combined with SUC, PRE, +, -, *, DIV, and MOD.  (I can't remember if I finished
EXP --- it's been months since I've had time to look at it.)  It's no slower
than the REDUCE library for single-digit numbers, and is much faster for large
numbers.  10-digit decimal numbers are no problem at all, for example, though
the multiplication code (and thus the DIV, MOD, and EXP code, which depends on
it) is still in draft form and is slower than it should be.  The library works,
but isn't ready for release.  (If you need it now and can cope with it as-is,
let me know.) 

Given such a library, I think it makes sense to represent numbers as numerals
when you want to do arithmetic on them.  The representation I use now looks
like this:

	DECIMAL [1;2;3;4;5]		% = 12345	%
	BINARY [1;0;0;0;0]		% = 16		%
	HEX [15;15]			% = 255		%

(DECIMAL, BINARY, OCTAL, and HEX are actually defined in terms of a more
general function that takes a radix as an argument.)  Note that I'm using the
numeric constants between 0 and the radix.  I needn't have --- I could use just
0 and SUC --- but that's not what I propose.  Here's my suggestion: 

     o	that hol define a small number (like 16) of numeric constants *for use
	only by the numeral library, parser, and pretty-printer*

     o	that the parser and pretty-printer use DECIMAL and lists of those
	numeric constants to represent numbers as terms

     o	that the numeral library be included as a basic part of hol (otherwise
	the terms produced by the parser won't have meanings)

     o	that is_num and similar functions related to numbers be rewritten to
	assume this representation of numbers

     o	that the num_CONV and REDUCE_CONV names be attached to routines in a
	compatibility library that perform the same functions but on the new
	representation (the old num_CONV and REDUCE_CONV routines must still
	exist, because the numeral library depends on them, but they can now be
	internal functions)

     o	that the user-visible syntax of numbers be extended to support binary,
	octal, and hexadecimal, as well as decimal

There are lots of ways of extending the syntax to represent other radices in
ASCII, and I don't like any of them, but I'm willing to live with anything that
is an already accepted syntax somewhere else (like in a programming language). 
The most general I've heard so far is the "10r99" format, where digits before
the "r" are interpreted as a radix (in decimal) and digits after the "r" are
interpreted in that radix as the value of the number.  Note that this is
necessary just for non-decimal numbers; the default is still decimal.  I've
also used systems in which the default radix was variable, and I suggest that
we avoid that. 

These are the advantages and disadvantages I see to my proposal:

     o	As John points out, to define the arithmetic operations you need list
	recursive definitions, and to get that far you would need to use SUC
	in the arithmetic theorems required, so in building HOL some theorems
	will have to be proven, then rewriten retrospectively.

     o	Existing code that depends (in ways other than calling is_num and other
	converted functions) on numbers being represented by simple constants
	will break.

     o	Other code, including code that uses num_CONV and the REDUCE library,
	should still work.

     o	The parsing and pretty-printing of numerals is now trivial (and
	doesn't use mk_thm), and can stay that way even when the user-visible
	language is extended to support numerals in other radices.

     o	Users can easily use other radices.

     o	Users can easily do simple arithmetic computations by proof, in a 
	reasonable amount of time.