Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Message-Id: <9308261420.AA14504@easynet.crl.dec.com>
Date: Thu, 26 Aug 93 11:17:58 EDT
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11" <leonard@ricks.enet.dec.com>
To: richard.boulton@cl.cam.ac.uk
Cc: info-hol@dworshak.cs.uidaho.edu
Apparently-To: info-hol@dworshak.cs.uidaho.edu, richard.boulton@cl.cam.ac.uk
Subject: Re: numerals by pretty printer instead by num_CONV?

Richard Boulton asks:

>	Did you find having the most significant digit as the first element of
>	the list to be advantageous?

Each way has small advantages and disadvantages, but I think it really matters
very little.  I have to do some things right-to-left, and other things left-to-
right, so I have to cope with "the wrong" ordering either way.  Once I figured
out how, I really stopped caring which way the digits went.  This way's easier
for me to read. 


>	By defining the digits as fully expanded SUC forms there is no need
>	for num_CONV.

That's right.  I support a function of that name for compatibility, but it adds
one using numerals, and then substitutes SUC for add one.


>	One good thing about this [using only a few numeric constants] is that
>	the constants can be defined rather than being built in as an axiom
>	scheme:
>
>	   1 = SUC 0
>	   2 = SUC (SUC 0)
>	   3 = SUC (SUC (SUC 0))
>	   etc. (upto a *finite* (and fairly small!) number)

Yes, and that feels like a real advantage.  I *REALLY* would like to get rid
of the wordn axiom scheme, too.  It makes me gag every time I think of it (it's
possible to type in a constant of an undefined type, for example).  It may have
made sense at the time, but it'll be a real relief to have an alternative.
Would hol then be entirely free of such axiom schemata?


>	[discussion of the names for the numeric constants beyond 9]

I think you're confusing the user-visible syntax of numbers with the names of
single-digit numeric constants.  The numeric constants are for internal use of
the numerals library, parser, and pretty-printer only.  The names don't have to
be pretty, and the names can't be 0, 1, 2, and so on.  They'll probably be
something like number_0, number_1, and so on.  There can't be constants with
names like 0, because if a user types 0, it will be parsed into a term like
this (I'm winging this, so it probably has bugs): 

	mk_comb( mk_var(`DECIMAL`, ": num list -> num"),
		 mk_list( [mk_const(`number_0`, ": num")], ": num" )

The hol user specifies numbers by talking to the parser, using our new not-
yet-decided-upon syntax for non-decimal radices.  Single-digit numbers parse
to numerals (digit lists) of length one --- a type of object different from the
numeric constants that represent each digit. 


>	The pretty-printing would probably be easier if one avoids defining
>	DECIMAL, BINARY, etc., and simply use the more general function (which
>	I assume takes the radix as an argument).

Since the user-visible representation of decimal numbers is different from that
for numbers in other radices, I'd guess that it would actually be easier to
treat decimal as a special case.  But I agree that the others are probably best
handled using the general function that takes the radix as an argument, and 
arithmetic will be faster if all numerals are.