Question formal status of trees in H&GPSG

[Carl Pollard]

Ken,

The main issue about types in HPSG is what KIND of type theory to use.
You describe an algbraic notion of type. But HPSGs are not algebraic
theories, even if you allow sorted, or even order-sorted algebras,
because the kinds of constraints people write go beyond what is
expressible using equality, a collection of operator symbols of
designated arities, and the universal quantifier. The best worked out
formal system for writing HPSG's is relational speciated reentrant
logic (RSRL), which has all the boolean connectives and bounded
(universal andf existential) quantification, enough power in fact to
simulate the typed lambda calculus (though I'm not sure how faithful a
simluation it is -- perhaps someone out there knows?).

My view is that it is more straightforward just to START with typed
lambda calculus, more specifically a two-valued boolean higher order
logic along the lines of Lambek and Scott (plus a weak form of
parametric polymorphism). Once you do that then your symbolic
representation of (say) a finite S is just a closed term of type Sfin,
rather than an attribute-value matrix. But then, by the Curry-Howard
isomorphism, there is a one-to-one correspondence between sentences
and (equivalence classes of) derivations. Thus each sentence is BOTH a
derivation AND a model-theoretic entity (an inhabitant of the type
Sfin).  This resolves the difference, much discussed nowadays, between
model-theoretic syntax and derivational syntax.

I take exception to your assertion that unification is one of the
operations HPSG makes available. The subsumption order on HPSG (at
least, post-1980's HPSG) feature structures is flat (because the
structures are totally well typed and inequation resolved). So they
are not they kinds of things that can be unified (though DESCRIPTIONS
of them are).

Also, I don't think you want to think of attributes as atomic
entities. Rather, feature structures are static record types (=
indexed product types), and attributes are the indices (see, e.g.
the discussion of records in  Barr and Wells).

Cheers,

Carl