Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Overloading of constant names
In-Reply-To: Your message of Sun, 26 Jan 92 15:11:07 -0800. <9201262311.AA15708@maui.cs.ucla.edu>
Date: Mon, 27 Jan 92 00:58:09 +0000
From: John.Harrison@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.315:27.00.92.00.58.17"@cl.cam.ac.uk>


Ching Tsun (chou@edu.ucla.cs) asks:

> In HOL, if I have defined:
>
> (1)     neg:num->num = \x.0-x
>
> then I can no longer define:
>
> (2)     neg:bool->bool = \x.~x
>
> But why?  DESCRIPTION says a HOL constant is a (name, type) pair.
> Clearly neg:num->num and neg:bool->bool are two different constants.
> So why does definition (1) preclude definition (2)?

This just happens to be the way HOL works; you are only allowed to define a
constant name once in a theory hierarchy. But having recently constructed
integer, rational and real number systems, I too have felt the need for
several "+" operators amd several "0"s.

Hopefully, some form of operator overloading will eventually be included in
HOL. Having given this a little thought myself, I would be interested in
suggestions for a workable scheme. What you are suggesting, regarding constants
with the same name but different types as distinct, is all very well, but may
hit problems if the types are polymorphic and could be unified (i.e. the type
variables in two identically-named constants be instantiated so the types are
no longer distinct).

I had been thinking of making the surface syntax translate down to genuinely
different names (a bit like the hacks C++ uses for external names) according to
the type context. This seems reasonable, but it would need a rewrite of the
type inference system for terms, I think. Also, you would need to address the
issue of defaults, e.g. should "x + y" default to x and y being ":num", or
":real"? Upwards-compatibility might suggest the former, commonsense the
latter and the example of ML that it should be faulted.

In the short term you could try using the interface maps feature; this doesn't
give as much flexibility as overloading, and you can't use it on numerals, but
you can set up different environments for different parts of the proof. For
example I have used:

> set_interface_map
> [`num_add`,`+`; `+`,`real_add`;
>  `num_mul`,`*`; `*`,`real_mul`;
>  `num_sub`,`-`; `-`,`real_sub`;
>  `num_lt`,`<` ;`<`,`real_lt`  ;
>  `num_le`,`<=`; `<=`,`real_le`;
>  `num_gt`,`>` ;`>`,`real_gt`  ;
>  `num_ge`,`>=`; `>=`,`real_ge`];;

where the `real_xxx`s are my operators on reals, and the `num_xxx`s the new
names for the num counterparts.

John.

===============================================================================
  John Harrison (jrh@cl.cam.ac.uk)

  Hardware Verification Group
  University of Cambridge Computer Laboratory
  New Museums Site
  Pembroke Street
  Cambridge CB2 3QG
  England.
===============================================================================