Full-Name: Joshua D. Guttman
Posted-Date: Thu, 21 Mar 91 12:33:31 -0500
Date: Thu, 21 Mar 91 12:33:31 -0500
From: guttman@org.mitre.linus
Message-Id: <9103211733.AA02828@malabar.mitre.org>
To: info-hol@edu.uidaho.cs.ted
Subject: semantics of polymorphic operators

I'm looking for a citation (or else an off-the-cuff explanation) for the
semantics of HOL polymorphism.  I know that lots has been written about the
syntax of polymorphism (typing algorithms etc.), but I'm in the dark about the
(formal) meaning of them.

[Note:  I'm asking about the polymorphic operators in the HOL formal logic
rather than those in ML.]  

That is to say, given a model for the polymorphism-free part of an HOL-theory,
can we find objects that are the denotations of polymorphic constants such as
cons, pair, composition (of functions), etc.?

There are of course two main lines of response (namely yes and no).  The "yes"
response would assert that we can construct denotations for the polymorphic
operators "above" the given model. 
 
  Note:  I figure that they can't already be inside the model, supposing it to
  be a normal stratified model for simple type theory.  Clearly "pair" can not
  have as its denotation an object of level n,  because it is applicable to
  objects of yet higher level.  

One question relevant to whether the "yes" approach will work is whether there
is an expression l in the hol language such that
 first(l)=cons
can be proved; i.e. can lists be built out of polymorphic operators themselves?
If so, one might have to use a very complicated construction to "fill out" the
original stratified model.

The "no" response would assert that we can't or don't need to construct
denotations for the polymorphic operators.  Rather, they might be construed as
"pure syntax" with no denotation.  Their meaning (such as they had) would
simply be as a device to construct uniformly their ultimately monomorphic
instances, which are given denotations in the straightforward way.

One version of this "no" approach would be similar to Hilbert's mature view:
the directly meaningful mathematical assertions are a particular class (in his
case, the finitist assertions).  The rest of mathematics should be construed as
a collection of "ideal" assertions.  They have no intrinsic meaning, but serve
as an elaborate scaffolding that allows us to marshal real, finitist assertions
in useful ways.  Therefore, the constraint on ideal mathematics is that it
should be conservative over real, finitist mathematics.  Hilbert was able to
reformulate this in terms of simple consistency because of the nature of
finitist assertions.

In the analogy here, the real statements would be the monomorphic ones, and the
ideal statements those with *s in their types.   

There is one other antecedent for the "no" approach that I'm familiar with,
going back to Russell.  Since Principia Mathematica has non-cumulative types,
objects like the cardinal numbers recur at every type.  Rather than prove that
e.g. 1+1=2 holds at every type, Russell construed such statements as "typically
ambiguous".  I believe that he meant by this that such a statement should be
construed as a uniform presentation of all the instances that result when a
type is chosen for the cardinals.  Naturally, they all look the same, and their
*proofs* are also perfectly uniform.  A typically ambiguous assertion is thus
not really a particular proposition, but a piece of syntax that lets us present
a class of real propositions.  Perhaps polymorphic operators can be cashed out
as a more sophisticated latter-day syntactic mechanism to accomplish a more
inclusive range of goals.  

In any case, I would be interested in all work that's been done, either
developing a semantics for these operators, or in developing a rationale for
avoiding giving them full-fledged semantics.