Re: SUO: Montague's Type System
On Wed, Feb 18, 2004 at 08:45:47AM -0800, Richard Cooper wrote:
> Pierluigi Miraglia wrote:
> > > Anyone,
> > >
> > > I'm having trouble understanding a small passage
> > > in the CoreLex thesis. It goes like this:
> > >
> > > ----------------------------
> > > "(17) John and every (other) student went to her party.
> > >
> > > In Montague's type system (e for individual; t for proposition)
> > > [every (other) student]NP is of type <<e,t>,t>, whereas [John]PN
> > > is of type e. Although of different type they are coordinated
> > > on the same level by the conjunction operator (functor) 'and'.
> > > One can soleve this problem by shifting [John]PN from type e
> > > to type <<e,t>,t> [Partee, 1987]. The semantical motivation
> > > behind this is that 'John' can be interpreted as the set of
> > > properties of 'John', which is exactly expressed by the
> > > type <<e,t>,t>: a function from sets of properties (<e,t>) to
> > > truth values (t). "
> > > ---------------------------
> > >
> > > I understand that (and) takes two truth values, not an individual
> > > and a proposition. What throws me is the meaning of "<<e,t>,t>"
> > > as a type notation. Can anyone explain what words to use when
> > > speaking "<<e,t>,t>" out loud?
> > >
> > > Thanks,
> > > Rich
> > >
> >
> >
> > There is more than one way, but here is one that usually works for me:
> > for any type S, you identify a set of objects of type S with its
> > characteristic function -- a function from S to {0, 1}.
>
> In programming languages like Delphi, the type name
> is also used as a characteristic function. So
> ----------------------
>
> type TStudent = Class(...);
>
> var John : TObject; {or some descendent class thereof}
>
> ...
> if TStudent(John)
> then Enroll(John);
>
> ---------------------
> So I interpret the characteristic function as sort of built
> into the language. I guess the example above would be:
>
> <John, t> is an individual (the var Alpha) of type TStudent.
>
> <<John, t>, t> is the class TStudent, including all its
> individual instances.
>
> Is that a correct interpretation?
no wait, the notation <_, _> constructs _type-denoting_ terms from
other _types_. So '<John, t>' is meaningless (unless 'John' denotes a
type in your language).
In MS, there are 2 primitive types, e (the set of individuals) and t
(truth value set). Say you want to add as a primitive type TStudent,
the class of all students.
Then '<TStudent, t>' would have a meaning: it would designate the type
of (all) subsets of TStudent -- an element of this type would be a
subset of TStudent. ("Subsets" would be represented in this type by
their characteristic functions, which are properly elements of the
type.)
An object of this type would be something that returns a t-value when
the argument is a (instance of) TStudent. So _John_ would not be an
element of this type (though {John} would be). 'enroll' would be, and
'TStudent' itself too.
Another type would be <<TStudent, t>, t>. An object of this type is
something that returns a t-value when the argument is a _property_ of
students, i.e., a subset of TStudent.
>
> But wouldn't the class TStudent include John a second time?
>
> So <<John, t> t> includes John twice, unless there is
> some key that can indicate there is really only one John.
>
> But if so, why use such a round about way of saying that
> "every (other) student" is a class of the same class as John?
> It seems like a difficult notation compared to modern
> programming languages - maybe it historical paths are the
> confusing part here.
>
!!! :) We part company on that last statement... But actually I think
the general conception of types in programming languages is not at all
different from that in lambda calculus or similar. Problems tend to
arise because each of the individual languages make distinct specific
stipulations about (what they call) "types"...
>
> > Since 't' as you note is the primitive type Truth-Value (or Boolean),
> > you can think of anything of the form <S, t> as the type of all
> > functions from S to t, and therefore the type (class) of all sets of
> > objects of type S.
> >
> > So, given the primitives e and t:
> >
> > <e, t> = type of sets of objects of type e
> > = type of sets of individuals
> > = type of (extensions of) unary predicates (the
> > denotations of N = "Noun")
> >
> > <<e, t>, t> = type of sets of objects of type <e, t>
> > = type of sets of properties (= unary predicates)
> > ([[John]] has this type because it is the set of all
> > properties John has; [[every dog]] is of this type, too)
> >
> > <<e, t>, <<e, t>, t>>
> > = type of functions from properties to sets of properties
> > = type of quantifiers (the denotation of 'every', e.g., is
> > \lambda P \lambda Q [\forall x Px \rightarrow Qx])
> >
> > etc.
> >
> > The 'and' of NP coordination denotes an operator different from the
> > truth-functional, sentential 'and'.
> >
> > (The best explanation I know of all this is in Dowty-Wall-Peters.)
> > Hope this serves, maybe somebody will be kind enough to correct my own
> > misconceptions...
>
> Thanks, I'll google up some Dowty-Wall-Peters references.
> Rich
>
>
> > regards
> >
> > --
> > - - - - * * * * * - - - - * * * * * - - - - * * * * * - - - -
> > Pierluigi Miraglia Cycorp, Inc.
> > Ontologist 3721 Executive Center Dr.
> > (512) 514-2988 Austin, TX 78731
> >
> > sr
> >
>
--
- - - - * * * * * - - - - * * * * * - - - - * * * * * - - - -
Pierluigi Miraglia Cycorp, Inc.
Ontologist 3721 Executive Center Dr.
(512) 514-2988 Austin, TX 78731