RE: SUO: Montague's Type System
> Pierluigi Miraglia wrote:
> 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).
I see; <_, _> is a type constructor. In Delphi, it might be
more comparable to say:
type TGraduateStudent = Class(TStudent)...;
type TUndergradStudent = Class(TStudent)...;
type THonorsStudent = Class(TUndergradStudent)...;
so <_, _> could be used as
<THonorsStudent, t> indicates a subclass derived from THonorsStudent,
if I understand your explanation, while
<THonorsStudent, nil> indicates some class that is not descended
from THonorsStudent, etc.
And when you wrote:
> > > <<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)
I'm still missing the last part of that:
([[John]] has this type because it is the set of all
properties John has; [[every dog]] is of this type, too)
If I have a descendent type, such as THonorsStudent, it has all
the properties of TUndergradStudent, which has all the properties
of TStudent, but may not have some of the properties of TGraduateStudent.
Is that a bit more in line with MS?
Thanks,
Rich
> 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