Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <886.9303111611@frogland.inmos.co.uk>
Subject: Re: overloading in theorem provers
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Thu, 11 Mar 1993 16:11:15 +0000 (GMT)
In-Reply-To: <93Mar10.005632met.8116@sunbroy14.informatik.tu-muenchen.de> from "Konrad Slind" at Mar 10, 93 00:56:20 am
Content-Type: text
Content-Length: 3101

Konrad Slind has said:
> I am wondering what people think about overloading of constants in
> theorem provers. As a user, I don't think that I would use it, but as an
> implementor I have to cravenly obey the wishes of hoi polloi. A
> strong case can be made for some operators (matrix indexing comes to
> mind), but all too easily someone could overload conjunction (/\) as
> logical conjunction, a lattice operation, a set operation, and a
> conjunction operation in an embedded logic. And then use all of these in
> a single bletcherous term. One gets what one deserves, I suppose. 
> 
> One question is: isn't this just a user-interface issue, to be handled
> by parser and prettyprinter? The alternative seems to be putting overloading
> into the term structure, which seems drastic for something which is
> "mere notational convention", as scores of Mathematics books would have it.
> 
> This issue probably becomes more pressing with abstract theories, since if
> one takes a naive approach to instantiating an abstract theory, i.e.,
> the abstract signature somehow magically becomes a concrete signature,
> overloading is required, or at least must be addressed.

I think I would use overloading ... however it should only be at the
interface level.

I.e. I would like to be able to type

--`! (x:integer) y z . (x < y) /\ (y <= z) ==> (x < z)`--

where `<` and `<=` would parse to constants of type
==`:integer->integer->bool`==.

The main reason is that as you develop :nums, :ints, :rats, :reals,
:complexes etc it gets a bit irritating to have to think up new names
all the time for the same conceptual operators without having
unwieldly long names - i.e. I think

--`! x y z. (x int_less y) /\ (y int_leq z) ==> (x int_less z)`--

is a bit opaque.

However, in a parsed term an overloaded symbol should have a fixed meaning
i.e. a parsed term

--`! x y z. (x < y) /\ (y < z) ==> (x < z)`--

defines a single term, not a family parameterized by the various constants
named "<".

Thinking of implementions.

? Associate a "template" type with each overloaded constant which
defines the general shape of it - i.e. for "<" it would be
`:'a->'a->bool` (thus disallowing e.g. real-integer comparison, but
that sort of overloading is way over the top in my mind). Then at
parse/type-check time, the template type gets put in at the first pass
of typechecking. If the term typechecks (e.g. :'a->'a->bool can be
infered to :num->num->bool) then all is ok. Otherwise, perhaps there
should be a mechanism for selecting a prefered typing - e.g. while
proving integer theorems you would have "<" parse to type
`:integer->integer->bool` unless it can be infered to another type.
Another pass of type inference may then be necessary to filter this
new type information through the term.


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television
						      - Husbands and Wives