Date: Fri, 22 Mar 91 12:06:47 GMT
From: Rob Arthan <rda@uk.co.stc.icl.win>
Message-Id: <9103221206.AA28080@win.icl.stc.co.uk>
To: info-hol@edu.ucdavis.iris
Original-Sender: rda <rda%uk.co.stc.icl.win@uk.co.stc.stl>

My colleague Roger Jones tells me that Mr. Guttman has asked for a
reference or an off-the-cuff explanation of HOL polymorphism.  The
following is an attempt at both:

A treatment of the HOL semantics inside ZF (or any adequately strong
set theory) may be found in the chapter on the semantics of HOL (due to
A. Pitts) in the `Description' volume of the HOL manual. I have given a
fully formal treatment of the syntax and semantics in HOL itself in
some internal ICL papers which can be made available externally if
anyone wants them (they are currently only drafts).  My treatment
works within HOL itself by defining polymorphic predicates which
identify what a model of HOL would be, without axiomatically asserting
the existence of such a model.

In both treatments, the semantics is done in terms of classical set
theory.  One  can view the monomorphic sublanguage of HOL as typed set
theory.  More accurately, it is a typed (or many-sorted) version of
Zermelo set theory with choice (Zermelo set theory being ZF without the
axiom of replacement).

It is presumably possible to take a purely syntactic view of the
polymorphism.  It is more or less clear that any proof of a monomorphic
fact could be transformed into a proof only involving monomorphic
terms. However, I, for one, haven't checked out all the details and
suspect that it might be more complicated than it seems at first glance,
if one wishes to take into account the various definitional (or
conservative extension) mechanisms.

It is well-known (e.g. see Kunen's book `Set Theory: An Introduction to
Independence Proofs') that Zermelo (with choice) has a standard model
in ZF (with choice). The universe of a standard model of Zermelo is
some set, U, say, inside ZF and, in U, membership, power set, union
etc. all mean exactly the same as they do in ZF. Neither Pitts nor I
explicitly mention the syntactic side of Zermelo, we simply specify the
closure conditions which U must satisfy.

Essentially, both Pitts and myself then interpret a polymorphic object
with n type variables, say, as a function from U**n to U. Instantiation
is then just application of these functions. The technical details in
the two accounts differ (because of the different metalanguages). The
actual construction is fairly straightforward in both accounts once the
basic framework is established. Everything goes through in what is, I
believe, a fairly weak subtheory of ZF - certainly you don't need
ridiculously large cardinals or anything like that.

I don't really understand your question about ``first l = cons''.  At
first glance the answer is yes, in Cambridge HOL syntax, for example,
``FST (CONS, X)'' is equal to ``CONS'' for any ``X''! Are you thinking
of some sort of construction within the type system itself as in
Girard's system F or the like? If that is what you had in mind then the
answer is that the type system itself is not intended as a source of
logical strength so much as a useful type discipline for the users, I
believe.

A general treatment of systems like HOL viewed in this sort of way may
be found in Feferman's contribution on theories of finite type in
Barwise's Handbook of Mathematical Logic. However, Feferman is largely
concerned with theories which are proof-theoretically weaker than HOL
(e.g. theories which are conservative over Peano arithmetic). He is also
not concerned with polymorphism, I seem to recall.


Rob Arthan (rda@win.icl.stc.co.uk)


PS.  I would like to be on the info-hol mailing list, but we don't know
what the official way of doing this is these days. Can some kind soul
let me know what to do?