To: guttman@org.mitre.linus
Cc: Andrew.Pitts@uk.ac.cam.cl, info-hol@edu.uidaho.cs.ted
Subject: Re: semantics of polymorphic operators
In-Reply-To: Your message of Mon, 01 Apr 91 16:16:16 -0500. <9104012116.AA01018@malabar.mitre.org>
Date: Wed, 03 Apr 91 18:22:55 +0100
From: Andrew.Pitts@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.897:03.03.91.17.22.56"@cl.cam.ac.uk>

>I would prefer to think of the denotation of a term as
>relative to a choice of model *and* an assignment of values to the free (type
>and ordinary variables).  On this way of describing things, only a closed
>expression would have a denotation relative to a model simpliciter.  This
>contrasts with your way of putting things, according to which the denotation of
>an expression relative to a model is a function which when given values for the
>free variables returns ... the same result.
>
>Naturally, these two ways of doing things are completely equivalent, notational
>variants you might say.  I prefer the former because ....

I prefer the latter because it specifies the semantics in terms of
sets-and-functions rather than sets-and-elements, and hence can be generalised
directly by replacing the category of sets and functions by other categories
with suitable structure. (That was what Mike Fourman's mention of "Boolean
toposes" was about, in part). For the HOL logic using other categories is
maybe not so important; but
for other, more arcane type theories it's very useful for finding models. (By the
way, I also prefer the way I wrote things because the (meta-)type of a
denotation is emphasised, and I believe type information is useful (!!).)

Andy Pitts