Via:  uk.ac.nsf; 27 May 89 20:02 BST  (UK.AC.Cam.Cl.scaup)
Date: Sat, 27 May 89 14:49:49 BST
From: Tom Melham <tfm%uk.ac.cam.cl@uk.ac.nsf>
To: info-hol <info-hol%edu.ucdavis.clover@uk.ac.nsf>
Message-Id:  <8905271451.aa21229@scaup.Cl.Cam.AC.UK>
Sender: tfm <tfm%uk.ac.cam.cl%uk.ac.nsf@edu.ucdavis.clover>
Status: R

RE: numerals in HOL.

I agree with the basic idea behind Paul's message
about Val_CONV, namely that it's better to work with an internal
representation of numbers which is a power series, rather than
a unary representation.  There are a few details that should be
thought about (e.g. what's the exact logical status of the numerals?
Are they an infinite family of constants, or metalingustic abbreviations
for a power series?), but the general idea is a good one.

There seem to be a few options.

   1) define the numerals 1,2,3,4,5,6,7,8,9 as constants, using
      the equations:

        1 = SUC 0
        2 = SUC 1
        ... etc

      then take a number, for example, 1562 to be a METALINGUISTIC
      abbreviation for a term of the form

        "series [2,6,5,1]"

      where "series" is an appropriate function defined over lists.
      Here, the transfomations

        "1562" ------> "series [2,6,5,1]"  -------> "1562"
                  ^                            ^
                  |                            |
                parser                    pretty-printer

      are done by the parser and pretty-printer, and "1562" is NOT a
      constant, but a metalinguistic abbreviation for a term.


   2) A similar scheme, but make the numerals an infinite family
      of constants, defined by a "conversion" (e.g. like num_CONV),
      so that:

        num_CONV "1562" ----> |- 1562 = series [2,6,5,1]

      Here, the numeral 1562 is actually an object-language constant.

   3) Retain the present status of numerals (and the present num_CONV),
      but provide option 1 as well, by introducing a new syntax for
      meta-linguistic abbreviations for power series.  E.g.

        "1562"    = a constant defined by num_CONV "1562" as at present

        "#1562"   = a metalinguistic abbreviation for "series [2,6,5,1]"

   4) do one of the above, but represent numbers base 2.  In this case,
      the parser and prettyprinter end up doing COMPUTATION... contrary
      to their status as establishers of simple meta-language abbreviations.

I'm not sure which of these is preferable.  The best thing, of course,
is to avoid reasoning about properties which hold of only one particular
large natural number.

Tom


Concerning  David Shepherd's remarks about the define_type package:

>Perhaps part of the lesson of this is that after struggling with
>"new_type_defintion" type definitions we saw "define_type" as a
>universal panacea to all our type definition problems....

The present implementation of define_type is, of course, not the universal
panacea to all type definition problems.  All it can do for you is to
construct the formal definition for any CONCRETE recursive type. This is still
a great improvement over defining these types "by hand" (if you don't believe
me, try one or two manual definitions), but it doesn't help very much with
defining ABSTRACT types (i.e. types whose values also satisfy some given set
of properties).   As David pointed out, equality on concrete types is
determined syntactically (that's why they're concrete), so you can't just add
extra axioms to force certain terms to be equal.

I'm presently working on a new package for defining certain abstract types
auomatically (finite sets are a typical example).  The details are more or
less worked out---I just have to code it efficiently in HOL.  With this new
package, Phil's type of finite sets will be described by user input that will
look something like:

     `set = EMPTY | INSERT x set
          where INSERT x (INSERT x s) = INSERT x s
          and   INSERT x (INSERT y s) = INSERT y (INSERT x s)`

The result will be a theorem characterizing this type.  I hope to get a
prototype implementation done as soon as possible, which I'd like to release
to interested parties for comments---before it's included on the distribution
tape.

Tom