Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@dworshak.cs.uidaho.edu
In-Reply-To: "Tim Leonard, DTN 225-5809, HLO2-3/C11"'s message of Thu, 26 Aug 1993 17:17:58 +0200 <9308261420.AA14504@easynet.crl.dec.com>
Subject: numerals by pretty printer instead by num_CONV?
Message-Id: <93Aug27.105014met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Fri, 27 Aug 1993 10:50:05 +0200


Tim Leonard writes:

> I *REALLY* would like to get rid of the wordn axiom scheme, too. ... 
> Would hol then be entirely free of such axiom schemata?

No. There's "string_CONV" in the string library.

Literals for numbers, words, and strings are problems for logic
implementations. Why? Because one has to

    A) represent a large or "infinite" number of related constants 
       in the signature,

    B) give each constant a definition (in a presumably uniform manner).

This isn't a problem in a informal presentation of a logic, but an
implementation needs to do some extra work. Why are literals there in
the first place? Two reasons - readability and space conservation.
Parsing and prettyprinting takes care of the first problem, but not the
second - representing string literals as num lists takes a lot of space!

I find Christopher Landauer's comments germane - a closed world approach
where we just focus on the current hacks is not going to be
satisfactory. We should consider what literals we might possibly want,
to see if there is a general way of handling them. I can see that we
will want literals for nums, words, strings, integers, reals, floating
point numbers, and possibly programs. Are there others? The literals I
know of are ground - does anyone have an example of a useful family of
polymorphic constants?

Konrad.