Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Konrad Slind <slind@de.tu-muenchen.informatik>
To: info-hol@edu.uidaho.cs.ted
Subject: overloading in theorem provers
Message-Id: <93Mar10.005632met.8116@sunbroy14.informatik.tu-muenchen.de>
Date: Wed, 10 Mar 1993 00:56:20 +0100


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.

Konrad.