Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: Rob Arthan <rda@win.icl.co.uk>
Date: Mon, 6 Sep 93 13:42:23 BST
Message-Id: <9309061242.27960.0@norman.win.icl.co.uk>
To: info-hol@cs.uidaho.edu
Subject: Polymorphic literals

Konrad Slind writes:

> .... 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?

Two possibilities and some remarks:

Example 1:

One might feel the need for a supply of polymorphic literals for HOL in
developing an analogue of the classical set-theoretic treatment of
finite and infinite cardinalities.  One might, for example, want to
define the finite cardinals in something like the way that, I believe,
Frege and Russell did it:

  0 = { {} }
  1 = {A | For some x B, A = {x} cup B, x is not in B and B is in 0}
  ....
  i+1 = {A | For some x B, a = {x} cup B, x is not in B and B is in i}
  ....

so that the i-th cardinal is the set of all sets with exactly i
elements. Of course, it is easy in HOL to define the primitive
recursive function which sends a natural number i to the i-th cardinal
in the above sense, so that having these cardinals available as a new
family of literals would not give a great syntactic benefit, since it
would just exchange the need to name this transfer function explicitly
for the need to do whatever is required to a numeral to indicate that
it denotes one of these new user-defined cardinals. I have been working
on a theory of cardinality for ProofPower-HOL and haven't felt the need
for literals like these to be very strong.

Example 2:

In the above example, the new literals would be polymorphic in a very
simple way: each cardinal has type (*) SET SET; moreover, the new
literals can be defined in a uniform way within the HOL type system.
One can certainly conceive of cases where one might want ``literals''
for which this is not so. For example, consider the operator which
sends a set A to it's i-fold cartesian product:

  cp 1 A = {x | x is in A}
  ....
  cp (i+1) A = {(x, y) | x is in A and y is in cp i A}
  ....

It is plausible that one might want to treat the values of this
operator for literal constant values of i as a family of literals.
This would enable one to get a little closer to the language of untyped
set theory, where one writes A^1, A^2, ...  for cp 1 A, cp 2 A, ...
(with `^' = `superscription'), which cannot be mimicked in HOL as is,
because cp is not typable, since the equations above imply that the
types of the cp i are:

  cp 1 :(*)SET -> (*) SET
  cp 2 :(*)SET -> (* # *) SET
  cp 3 :(*)SET -> (* # * # *) SET
  cp 4 :(*)SET -> (* # * # * # *) SET
  ....

Again I can't say I've ever felt the need of notations like this
very strongly. In this case, while the feature would let you
specify something using a nicer notation, as soon as you started
doing proofs you'd find it was impossible to state the sorts
of general facts you'd want to have about the notation. E.g.,
you'd have to give a separate proof of each instance you needed
of facts like A^(1+i) = A # A^i.

Remarks:

ProofPower-HOL in effect supports literals for *programs* by
giving a framework in which the user can define what are in
effect new object languages with their own parsers and pretty
printers, typically implementing a semantic embedding of the
new language. The mechanisms used to do this could certainly
be used to add real literals and the like to the HOL language,
although that's not really the sort of task they were envisaged
for. Whether there is any useful difference in kind between
support for new literal forms and support for new object languages,
I do not know.

One question which is apparent from the second of my examples is
whether one should implement schemes encouraging users to define new
syntactic forms which give a facility of expression which is not
matched by the facility of reasoning provided by the logic. Our
experience with implementing embedded object languages (like Z) is
that it is vital to try to design in what you need to support proof for
the new language. With something like the iterated cartesian product
notation, you'd have to plan to code up rules and conversions to
stand in for the basic facts about the new notation which can't be
expressed as theorems.

The examples above are probably far from typical, since I've just
dreamt them up to answer Konrad's question about polymorphism.
More typically, people will just want real numbers and the like,
which can, I'd imagine, be handled by giving a slicker embedded
formulation of the treatment which a user could give at the
moment by writing say `REAL "3.14159"' to denote the first 5 decimal
places of pi where REAL is a HOL function from strings to reals which
computes the value of a decimal number (or whatever).

Perhaps more relevant than plain polymorphic examples in real use would
be if people wanted to mimic the sorts of notations used in algebra.
For example, it's fairly common in informal mathematics to write 0, 1,
2, ... to denote elements of an arbitrary ring-with-unit.  This can of
course be handled by a transfer function:

  tf 0 = the zero element of the ring
  tf 1 = the unit element of the ring
  ....
  tf (i+1) = the unit element + tf(i)
  ....

but using an explicit transfer function is perhaps clumsy. If you
really want to mimic the traditional notations accurately then this
is only part of the story: you would certainly need to support
operator overloading (including overloading for the literals) and
also the overloading of juxtaposition (so that `2 a' can mean
`2 * a' as it ought to). Moreover, the overloaded numeric literals
would in some instances be implicitly parameterised by information
about the type to which they were instantiated (viz. the zero and unit
elements in the above example).

ProofPower-HOL supports operator overloading (in the typechecker and
pretty-printer, not in the logic) but not of literals or of
juxtaposition. How far one goes down these paths would really seem to
depend on whether you're really trying to support a surface syntax
very close to that of informal mathematics or not?


Rob Arthan. (rda@win.icl.co.uk)			ICL Secure Systems,
						Eskdale Rd.	
						Winnersh,	
						Wokingham	
						Berks. RG11 5TT