Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Rob Arthan <rda@win.icl.co.uk>
Date: Thu, 21 Apr 94 09:35:31 BST
Message-Id: <9404210835.21838.0@win.icl.co.uk>
To: reetz@ira.uka.de
Subject: Re: RE^2: overloaded constants
Cc: info-hol@cs.uidaho.edu

In ProofPower-HOL we follow Classic HOL and HOL90 in not permitting
overloading at the logical level. We do however have a parsing/pretty
printing facility for giving an alias to a constant name/type pair.
This was designed to be a more flexible replacement for the interface
maps used in other HOLs.

These aliases can be overloaded and the parser resolves the overloading
much as suggested in David Shepherd's posting,i.e., an alias name is
treated during type inference as an object whose polymorphic type is
the antiunifier of all the types of the constants for which the name is
an alias (where the antiunifier of t1, t2, ... tk means the least
general type which can be instantiated to each of t1, t2, ... tk).
If the type which is inferred for the alias uniquely identifies one of
the constants, then that's the constant to use and the term generated
by the parser has the constant name in it rather than the alias.
When a term is pretty-printed, each constant is printed out using
the most recent alias (if any) for which the type of the constant
is an instance of the type associated with an alias.

E.g., in the ProofPower-HOL theory of integers, addition is defined
something like:

	new_spec( ..... +_Z : INT -> INT -> INT ... );

(new_spec corresponding to new_specification in other HOLs and actually
invoked by markup characters which make the definition display and print
in a Z-like format).

This definition is followed by an alias declaration something like:

	declare_alias("+", ... +_Z : INT -> INT -> INT ... );

and thereafter type inference for the name "+" is carried out as
if it had the polymorphic type "'a -> 'a -> 'a" (being the antiunifier
of "NAT -> NAT -> NAT" and "INT -> INT -> INT").

Simple use of this facility leads to clearer specifications and no
problems in proofs (where, if you want to enter say "x + y", and there's
not enough information to determine the types of "x" and "y", you can
always bypass the alias by using the real constant name: "x +_Z y").

In general, the association between alias names and constants can be
many-many. This sounds chaotic but is actually very useful if used
sensibly. E.g., the bi-implication symbol "<=>" is declared as
an alias for the boolean instance of equality, "=:BOOL->BOOL->BOOL".
This means that when you're programming tactics etc., you rarely have
to worry about bi-implication as a special case, while the user writes
and sees standard logical notation.


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