Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Full-Name: Joshua D. Guttman
Posted-Date: Wed, 10 Mar 93 10:03:20 -0500
Date: Wed, 10 Mar 93 10:03:20 -0500
From: guttman@org.mitre.linus
Message-Id: <9303101503.AA00534@circe.mitre.org>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: Konrad Slind's message of Wed, 10 Mar 1993 01:23:16 GMT
Subject: overloading in theorem provers
References: <1993Mar10.012316.4480@linus.uucp>

In Imps we also decided to make overloading a user interface issue.  For
instance, if you're working with a number of metric spaces (say, three, to show
that the composition of continuous functions is continuous), then there are a
ridiculous number of different "continuous" predicates (six, I suppose, of
which three actually will occur in this particular proof).  IMPS has a
mechanism to introduce these predicates uniformly by definition, with names
such as continuous_01, continuous_12, continuous_02, etc.  The standard parser
and printer ensures that they can all appear to the user as "continuous" so
long as context disambiguates the implicit type.  This is almost always the
case in our experience.  The Imps theory interpretation mechanism ensures that
theorems about the original version (continuous_01 in this case) are available
for all of its images.  This is essentially transparent to the user.  

It also interacts well with abstract theories: when the user declares the reals
to be a metric space under some translation (having first proved that the
images of the axioms are true), then a continuity predicate can be created and
all the theorems will be available.  

In any case, if a user decides not to use the standard parser/printer, she sees
exactly what's going on explicitly in the s-expression abstract syntax.

In Imps the logical operators (and, not, forall, etc) are quite distinct from
constants.  So there's no possibility of overloading them.  This avoids the
wretched situation Konrad describes:  

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

My own view is that the logical operators are very special and it's preferable
to protect them from the common lot of function symbols.

	Josh