2. TYPED FEATURE STRUCTURES

Let us begin with an example from the Prolog programming language:

In one respect, these two clauses are a logical definition of what it means for three lists to stand in the append relation. The second is an implication (with, as is standard with Prolog, the consequent stated before the antecedent) that uses the recursive structure of lists themselves to relate different instances of append.

In another respect, this is a program that specifies how to search for a proof that three given lists stand in the append relation. Prolog has a standard order in which clauses are tried as it constructs a proof and a standard order in which conjoined antecedent goals are proved depth first during that search.

Now let us define the same relation with typed feature structures. A set of well-typed feature structures is induced by a signature that defines the type system and its relationship to a specified set of features. Figure 1 shows the signature for the append example. Every signature consists of a partially ordered set of types, in which order is interpreted as inclusion. The partial order must be bounded complete, which is equivalent to the requirement that every consistent set of types have a least upper bound, or, in the finite case, that every pair of types have a greatest lower bound. This entails the existence of a most general type, ⊥ (pronounced bottom). A signature also defines appropriateness conditions for each type: the set of features for which feature structures of that type can have defined values. The types of those values are also constrained by another part of the appropriateness condition called a value restriction. The type, append, in Figure 1, for example, has three appropriate features, each of which must be a list. We often require our feature structures to bear values for all of their type's appropriate features, in which case we say that the feature structures are totally well typed. Even though our feature structures are totally well typed, our descriptions of them do not need to mention all of the appropriate features, however. Indeed, for large signatures, totally well-typed feature structures may be required to have hundreds or thousands of substructures because each of their features' values must also be totally well typed. However, descriptions are typically very sparse: they only specify the information about a feature structure and its substructures that we could not infer from appropriateness conditions. Every nondisjunctive description has a unique most general feature structure that satisfies it (its most general satisfier), provided that, for every feature, there is a unique most general type in the signature to which that feature is appropriate.

A signature for typed feature structures defining the append relation. Appropriate features are given in small capitals; types are given in lowercase.

Similarly, our specifications of appropriateness conditions are sparse in that they take advantage of the requirement that every feature appropriate to a type must be appropriate to all of its subtypes. This means that we must only mention features in a signature specification where they first become appropriate, or where their value restrictions are refined. Append-base, for example, still has arg2 and result as appropriate features (we know this because it is a subtype of append), but it only refines the value restriction of arg1, from list to empty-list.

There are certain constraints on typed feature structures that signatures, as they are conventionally defined, cannot express, notably that two feature values are the same, no matter what their type. We often augment the signature with a set of type-antecedent implicational constraints to express this additional information. For append, we must add the constraints:

These are stated in the Attribute Logic Engine (ALE) programming language (Carpenter & Penn, 1996), a logic programming language based on typed feature structures. In practice, linguists do not augment their signatures only with constraints. ALE also provides a relational language very similar to Prolog, and a means of defining the lexicon and rewriting rules of a feature-structure-based phrase-structure grammar, all of which use descriptions of typed feature structures relative to a given signature specification, where Prolog would otherwise use first-order terms. A grammar in LTFS consists of a signature augmented with these other constraints and control structures.

To consider the use of constraints alone, however, which seems to accord best with Woodbury's and Burrow's use of LTFS, we may note the use of a special recurse feature in Figure 1 corresponding to the recursive use of append in the above Prolog program. These features are affectionately known as junk-slots (Aït-Kaći, 1984) and are required, in the absence of other control structures, to simulate the kinds of search that languages like Prolog conduct.

3. INFORMATION STATES

There are at least three ways of viewing what these signatures are defining. The first is simply a collection of partially ordered records, very much as an object-oriented language like C++ could define, only without methods. The second is a collection of information states about some discretely ordered set of objects. In this view, objects in the world really are not partially ordered (two objects are either equal or not, but the states of our knowledge about them are). The symbol ⊥, for example, is the type denoting no information (apart from an object's existence). Because LTFS is intensionally typed, we have no idea how many typed feature structures there are of type ⊥; but, assuming ⊥ has no appropriate features, we generally cannot distinguish them anyway (although see Section 5.5). The relation that compares the information contained in two feature structures is called subsumption, and is induced directly from the subtyping relationships among the types in the signature together with all of the possible sharings of feature values, such as those produced by the path equations in the constraint for append-rec. We can assemble all of the feature structures that mutually subsume each other into equivalence classes, and refer to each class collectively as an abstract (typed) feature structure. These abstractions stand in a one to one correspondence with the information contained in the typed feature structures relative to a fixed signature. Totally well-typed abstract feature structures for which every more informative extension satisfies the constraints of the grammar can be said to be grammaticalized.¹

Every abstract feature structure stands in a one to one correspondence with a set of primitive pieces of information about its structure, and every finite abstract feature structure sits at the top of a Boolean lattice of (not necessarily well typed) abstract feature structures that possess every possible subset of those primitive pieces. If we restrict ourselves to totally well-typed abstract feature structures, some of the elements of that lattice disappear (namely, the non-well-typed ones), and if we consider only those totally well-typed feature structures that satisfy the constraints of the grammar, then still more elements disappear. My reading of Woodbury et al. (2000) is that they elect to associate every (nondisjunctive) description from typed feature logic, as shown in Figure 2, with one of several peregrinations (constituting an explicit design space) from some initial totally well-typed abstract feature structure (probably an uninformative one of type ⊥ in many cases), through the most general satisfier of the description in the category of totally well-typed abstract feature structures, to the most general satisfier of the description in the category of grammaticalized abstract feature structures. The semilattice of totally well-typed feature structures bounded on bottom and top, respectively, by these two most general satisfiers constitutes an implicit design space through which the designer may wander, each step of which corresponds to the information added by the implicational constraints of the grammar that share some common type as their antecedent. This characterization of descriptions provides a designer with the ability to survey the very large space of totally well-typed abstract feature structures using the idioms of the grammar itself (the constraints) in a controlled way. To my knowledge, no one has cast the problem in formal terms before, but this is exactly what linguists want to do when they debug their grammars.

A subsumption-ordered explicit design space (solid lines) through an implicit space (dotted lines) defined by an initial state (here the abstract feature structure of type ⊥), the most general totally well-typed satisfier of a description (second from bottom), and the most general grammaticalized satisfier of the same description (fourth from bottom). The description used in this example is arg1:tail:empty-list ∧ arg2:empty-list.

Subsumption among typed feature structures is a preorder (not antisymmetric), so subsumption among abstract typed feature structures is a partial order, and it is bounded complete when the underlying partial order of types is. Given two feature structures, F and G, the unification of F and G selects a representative from the equivalence class located at the least upper bound of the abstract feature structures to which F and G respectively belong. In linguistic applications, unification is considered the LTFS operator par excellence. It consistently combines information from different words into a single representation of the information about a phrase. In their enumeration of design space exploration operators, Woodbury et al. (2000) define an equivalent operationalized variant that is consistent with their own view, called design unification. Design unification reapplies the sequence of steps that paint the explicit space of one abstract feature structure using another abstract feature structure as the starting point.

4. SEARCH

A third way of viewing what signatures are defining is to fall back upon the Curry–Howard isomorphism (Howard, 1980), interpreting types as propositions, and objects of those types as proofs of the corresponding propositions. Under this view, subtypes correspond to specific kinds of proof, and so proof search corresponds to a search for more specific subtypes. It is with this view that we can perhaps best understand how to use the append signature of Figure 1. Given an initial query description of type append, we can conduct a Prolog-style search by nondeterministically selecting a substructure of a non-maximally specific type and nondeterministically promoting it to one of its subtypes. To behave exactly like Prolog, we would need to adopt analogous conventions of which order to try subtypes in (left to right, as shown in in Fig. 1), and which order to select substructures in (depth first, junk slots last), but this general strategy, which is called maximal sort resolution, is how search is generally conceived of in pure, constraint-based LTFS.

All three of the above views of signatures are consistent. The completely fleshed-out proofs we seek in the third way correspond to abstract feature structures in which every substructure's type cannot be made more specific (sort-resolved), and every pair of substructures is either identical or explicitly inequated (grounded). Sort-resolved, grounded abstract feature structures stand in a one to one relationship with the discretely ordered objects of the second view, and are as close to a Herbrand universe²

Search is also thus a peregrination through the space of totally well-typed abstract feature structures, but it proceeds monotonically upward, backtracking only through information states previously visited, and its goal is any maximal (i.e., sort-resolved and grounded) information state. Burrow and Woodbury (1999) call their view of design space exploration incremental π-resolution when its path monotonically increases. π-Resolution is the name of the inference step in LTFS that promotes a totally well-typed feature structure to one of its minimal grammaticalized extensions. It is normally not associated with search (see Fig. 2) because it involves only don't-care nondeterminism (all of the constraints must eventually be enforced). As the authors seem to be concerned with directed search toward a specific and not necessarily maximal grammaticalized abstract feature structure (when the initial description is nondisjunctive and satisfiable), the departure does seem to be warranted.

5. WHAT'S WRONG WITH TYPED FEATURE STRUCTURES?

There are a few properties of LTFS that have proved to be a liability for large-scale grammar design, and I suspect that the same may very well be true for any large-scale design task. For the most part, they arise from the fact that designers love to change signatures. It is only very late in the design process that constraints and other constructs outside the signature become the predominant locale for modification, and even then only because the modifications tend to be minor.

5.2. Lack of modularity

Unification of typed feature structures is determined in part by the least upper bounds among types in the signature. Bounded completeness guarantees that a unique least upper bound will exist between any two consistent types. What it does not guarantee is that a small change in one part of the partial order (removing a subtype link, adding a new type, etc.) will not completely alter the least upper bounds for many pairs of types even seemingly distant from the site of the change. Least upper bounds only make sense in consideration of the signature as a whole, and do not in general admit a more localized definition. Some bounded complete partial orders are very well behaved in this respect, typically ones that either have a low percentage of join-reducible types or have a very small distance between every join-reducible type and the meet of the pair it reduces to. As if motivated only by cruelty, however, a great many HPSG linguists make design decisions that necessitate the use of type signatures with exactly the opposite properties. Figure 3, for example, is a type signature for English relative clauses that has recently been very influential on the look and feel of HPSG type signatures. This has a number of problems with it, beginning with the use of different subtypes like clausality and headedness where different dimensions of analysis were intended. However, it is not bounded complete, and it has a large percentage of joins, and large join-to-meet distances relative to its size.

A type signature for English relative clauses. Adapted from Sag (1997).

The classical view of modularity from the theory of programming languages is that the type system itself is responsible for mediating the communication between modules. LTFS has a very simple type system, so it is perhaps unsurprising that the partial order should be forced into such contortions. There have been alternatives proposed, such as using parametric types or other higher order type constructors (Penn & Hoetmer, 2003), or using more features, relations, and complex descriptions in favor of fewer types (Penn, 2004). Both are essentially attempts to enable designers to view types in independent dimensions more cleanly than through a tangled web of subtype relationships.

5.3. Subtype covering

Consider the signature given in Figure 4. The feature structure

is totally well typed, but it has no maximally typed extension; that is, even though verb is not a maximally specific type in the signature, the abstract feature structure to which this feature structure belongs is maximally specific in the corresponding subsumption-ordered semilattice. This can happen when the value restrictions on a collection of features appropriate to the same type are refined at subtypes in a manner that does not cover all of their possible values. Such is the case here for aux and inv. Their value restrictions at aux-verb and main-verb do not cover all of the possible values they could have taken at the type, verb.

A signature in which not every sort-resolved feature structure has a maximally specific type.

In the view of signatures as characterizing information states among discretely ordered objects, this is a problem, because it means that finding the sort-resolved abstract feature structures is not as simple as starting with the abstract feature structures that have maximally specific types. In fact, some would argue that such sort-resolved but non-maximally typed structures simply do not denote. It is possible to add extra inference rules to LTFS to detect these cases, but these rules make nondisjunctive type inference NP-complete (Penn, 2001). Most LTFS-based systems, including ALE, do not add the extra rules and simply carry the risk that some queries will return answers that, upon further investigation by the grammar's designer, are just a long-winded indication of failure. Arguably these designers should have written their signatures so that such cases did not arise, but there can be other esthetic criteria that determine the shape of signatures, making these unavoidable. One can always add extra constraints to the grammar, called subtype covering constraints, that legislate these cases out of existence, but it is up to the designer to do so.

5.4. Nondistributivity

Consider now Figure 5, a type signature with no appropriate features. Taking [sqcup ] to be unification (join), and [sqcap ] to be generalization (meet), we may observe that (a [sqcup ] b) [sqcap ] c = d [sqcap ] c = c, whereas (a [sqcup ] c) [sqcap ] (b [sqcup ] c) = d [sqcap ] d = d. Signatures in which these two operations are not always the same are said to be nondistributive. At first, this seems to be only of theoretical interest. However, in the case of unification and generalization, it is also true that if a [sqcup ] b [sqcap ] c = a [sqcap ] c [sqcup ] b, for all a, b, and c, then the signature is distributive. By contraposition, nondistributive signatures do not have this property, which means that if we take “join with b” and “meet with c” to be elementary operations for navigating around a lattice, then the order of these operations really will matter. In addition, we cannot take “meet with b” to be the inverse of “join with b,” in the sense that composing one after the other would yield the identity function—it does not. When we look at a complex description, it invites us to think of “join with b” as one of the primitive operations we must execute on feature structures during satisfiability testing, and thus during the sort of navigation that Woodbury and Burrow propose. As mentioned above, abstract feature structures can also be decomposed into order-invariant primitive operations that serve to identify the information they contain. The moral of this example is that we unfortunately cannot have both at the same time. There must be some degree of separation between what descriptions tell us to do and the primitive pieces of information that declaratively characterize our abstract feature structures. Burrow and Woodbury's (1999) proposal is to use constraints with the same type antecedent as primitive steps in incremental π-resolution, and the consequents of those constraints are stated with descriptions. This is why they must deal with order-dependent sequences of these steps rather than sets. This adds some additional complexity to how we must think about design space navigation with LTFS, but it does seem to be unavoidable.

A nondistributive lattice.