Logic and Feature Structures

1 Introduction

The number of different feature structure devices and formalisms proposed in the "unification grammar'' lit­ erature is growing so fast that it is important to find a "common language" in which they can be expressed. This paper shows how a variety of different types of fea­ ture structures and constraints on them can be expressed in predicate logic (or standard non-monotonic extensions thereof), including:

• (parameterized) sorts,
• subsumption constraints, and
• non-monotonic constraints (specifically LFG "constraint equations").

These were chosen merely to give a feeling for the ease with which fairly complex constructions can be described in predicate logic; they by no means exhaust the class of feature structures and constraints that can be given first-order axiomatizations. This suggests that instead of requiring radically new types of interpretations, even complex feature structures and constraints on them can be described using standard techniques. Not all these ex­ tensions have to be used in an implementation, of course, a reasonable policy might be to only implement the de­ cidable extensions described below, for example. Since feature structures are a kind of frame representation, the results presented here should be of interest to the wider A.l. community.

·The research described here was conducted while I was a Gastprofessor at the Institut fiir maschinelle Sprachverar­ beitung, Universitii.t Stuttgart, which I would like to thank for providing a supportive environment in which to get this work done. Robert Carpenter, Jochen Dorre, Andreas Eisele, John Maxwell, Michael Moorreau and Gert Smolka have all made insightful comments on the work reported here; naturally all responsibility for errors remains my own.

The results in this paper extend those presented in earlier work, especially [8,9,10,20,21], with which (due to space limitations) familiarity is presupposed.

2 The Schonfinkel-Bernays Class

One advantage of axiomatizing feature structures in first­ order predicate logic is that its proof-theoretic, model­ theoretic and computational properties are well-known. This paper exploits some of the results on decidable classes of first-order logic [3,5] to show that the satis­ fiability and validity problems for certain types of fea­ ture structure constraints are decidable. We show that variety of such structures and constraints can be axioma­ tized using formulae from the Schonfinkel-Bernays class, (called SB below); since the satisfiability and validity of any formula in SB is decidable, the satisfiability and validity problems for these feature structure constraints must be decidable too.

A formula is in SB iff it is of the form

where ¢ is a formula containing no function or quantifier symbols. 1 SB formulae possess the finite model property, i.e. if a formula has a model then it has a finite model [7]. Lewis [6] investigated the computational complexity of the decision problem for such formulae and showed that the satisfiability and validity problems for SB formulae are PSPACE-complete, and (by Proposition 3.2 of [6]) that the satisfiability and validity problems for SBn are NP-complete, where SEn is the class of SB formulae con­ taining nor fewer universal quantifiers.

1 Because tjJ can always be expanded to disjunctive normal form, Schonfinkel-Bernays formulae are a generalization of Dat­ alog clauses that allow disjunctive consequents. I hope to ex­ plore this more fully in later work.

The conjunction (and disjunction) of two SB formulae is itself a SB formulae (after quantifiers have been moved outward) . This means that SB axiomatizations of differ­ ent kinds of feature structures can be conjoined, and the satisfiability of the composite system is also decid­ able. For example, Johnson [10] axiomatizes 'set values' using SB formulae, and these axioms can be combined with e.g. the SB axioms for sorts given below to yield a system with both 'set-valued' and 'sorted' objects com­ pletely axiomatized in SB, and hence with a decidable satisfiability problem.

3 Attribute-value features

Attribute-value features, popularized in the work of Shieber [18] and others, are the most common type of features used in computational linguistics. The treat­ ment here is effectively the same as that in [10,20,21], so it is only summarized here.

Attribute-value features are in effect partial functions (see [12,8]) , and they can be formalized in first-order logic either

• as relations that obey functionality axioms (as is done here), or
• as "total" functions over a domain that includes a designated element that is interpreted as an "unde­ fined" value (see [8,9]).

These two different formalizations reduce the satisfia­ bility problem for attribute-value feature structure con­ straints to different classes of first-order formulae, and lead to different insights about the original problem.

Here, we conceptualize "pure" attribute-value features as instances of an "arc" relation, where arc(x, a, y) is true iff there is an arc labelled a from x to y. (In some expositions the elements x and y are called nodes and a is called an attribute) . The following axioms express the constraints that the arc relation must satisfy for it to be an attribute-value structure. The predicate con is true of the attribute-value constants.

The first axiom requires that the arc relation is func­ tional. (Used as an inference rule in a forward chaining system, it requires the "unification" of the "destinations" of a pair of arcs labelled with the same attribute leaving the same node; see [9,10] for details).

The second axiom requires that requires that attribute­ value constants have no attributes. (This axiom is re­ sponsible for "constant-compound clashes").

The attribute-value constants have special properties ex­ pressed by the next two axiom schema. These schema stipulate properties of the entities that the attribute­ value constants, a subset of the constant symbols of the first-order language, denote. Not every constant symbol will be an attribute-value constant, since it is useful to have constant symbols that refer to other entities as well.

The first schema requires that every attribute-value constant have the property con.

For all attribute-value constants c, con(c). (3)

The second axiom schema requires that distinct attribute-value constants have distinct denotations. (This is sometimes called a "unique name assumption").

This axiomatization is quite permissive, in that it allows

• cyclic structures,
• infinite structures,
• intensional structures (i.e. different elements may share the same attributes and values),
• disconnected structures, and
• allows values to be used as attributes.

Additional axioms could have been added to prohibit such structures, but because there seems to be no lin­ guistic or computational motivation for such additional stipulations they are not made here. (Axioms prohibit­ ing cyclic structures and attributes from being values can be formulated in SB, an extensionality requirement can be axiomatized using a first-order formula not in SB, while an axiom prohibiting infinite structures cannot be expressed in first-order logic).

Each node in a syntactic parse tree is associated with an element (different nodes can be associated with the same element; see Chapter 3 of Johnson [8] for full de­ tails). Lexical entries and syntactic rules constrain the elements associated with parse-tree nodes. Following Kaplan and Bresnan [12] we represent these constraints by quantifier-free formulae.

For example, a (simplified) lexical entry for the En­ glish verb swim might require that:

• the attribute-value element u associated with a node dominating the terminal item swim have a semantics attribute whose value is swim' (which ab­ breviates the verb's "semantic value"),
• that u have an agreement attribute whose value is, say, v, and
• that the value of v's number and person attributes (representing the verb's agreement features) not be singular and and 9rd respectively (these are the fea­ tures of the inflected form swims).

These constraints might be expressed in an extended PATR-11 notation (see Shieber [18]) as

and in FDL notation (see Smolka [20,21]) as

This paper takes no position on what notation such fea­ ture constraints should be written in, but simply sug­ gests that whatever notation is used to express this con­ straint it should mean the same thing as the following

(universal) quantifier-free formula.

(In this formula u is a constant that is not an attribute­ value constant, while semantics, swim', number, singular, person and 8rd are attribute-value constants). Arbitary boolean combinations (including negation) of attribute-value constraints can be expressed in this manner. 2

Note that the axioms defining attribute-value features and formulae expressing attribute-value constraints are all in SB, so their conjunction is also (equivalent to) a SB formula, and hence the satisfiability of such systems of constraints is decidable. Further, the only quantifiers appear in the axioms 1 and 2 so this conjunction is infact in SB7 , and hence the satisfiability problem for systems of feature constraints is in NP. 3 Since the satisfiability problem for arbitrary conjunctions and disjunctions of atomic feature structure constraints (here, arc atoms) is NP-complete [13), the satisfiability problem for the system described here is NP-complete.

4 Sorts

The term "sort" is used to mean different things by dif­ ferent authors. We sketch here how two common in­ terpretations of sorts can be axiomatized by considering some simple examples, and follow Smolka [20,21] in mod­ elling sorts by unary predicates (parameterized sorts are modelled by predicates of higher arity).

First, suppose that sorts are taken to restrict the pos­ sible attributes of an element, so that e.g. something of sort agr can only have the attributes number or per­ son (with perhaps restrictions on the values of these at­ tributes that for simplicity are not dealt with here). The following axiom defines this notion of sort.

(This one-place predicate agr could be used in a more refined lexical entry for swim that requires agr(v), i.e. that v be of sort agr.)

Second, suppose that sorts are also to require that cer­ tain attributes must have a value, so that e.g. something of sort agr' must have values for the attributes number or person. (Axiom 5 only prevents anything satisfying agr from having any attributes other than person and number). The following axiom defines this sort.

2 The proper treatment of negation in "feature logics" has been the subject of considerable discussion [15,16,1,8,9,10]: however I know of no linguistic application in which a classical interpretation of negation yields intuitively "incorrect" results.

3 The axioms 1 and 2 can be replaced with an equivalent axiom that "shares" the universally quantified variables, so systems of attribute-value constraints can be expressed as for­ mulae in SB4.

Both kinds of sorts can be optionally augmented by an extensionality requirement, which stipulates that no two distinct elements in the same sort have identical values for their attributes. For example, the following axiom requires that no two elements of sort agr can have the same values for their person and number attributes.

Because axioms of the form of 5 and 7 are in SB, the satisfiability of attribute-value systems augmented with sort constraints of the first type is decidable, and (given a fixed set of sorts and hence a fixed number of universal quantifiers) is NP-complete. On the other hand, axioms of the form of 6 are not in SB. While this does not imply undecidability, Smolka [20,21] has shown that for sys­ tems that allow parameterized sorts (i.e. sort predicates with arity greater than one) this is infact the case.

Of course, there is no reason to restrict attention to unary predicates. For example, assuming that lists are represented in the standard, attribute-value formulation using first and rest attributes (see Shieber [18] or John­ son [8] for details), the following axioms define the predi­ cate member(x, l), which is true iff x appears somewhere in the proper list represented by l. 4

Again, since the axioms in 8 are in SB, they can be con­ joined with any other SB axioms and the system remains decidable.

5 Subsumption Constraints

This section and the next focusses on some of the most difficult aspects of the theory of feature structures. Sub­ sumption constraints are notoriously tricky to formulate. Partly, this is because the term 'subsumption' is used to refer to two different notions in the feature structure lit­ erature.

First, subsumption can be construed as a relation be­ tween system of constraints. ¢; subsumes '1jJ iff every fea­ ture structure that satisfies '1jJ also satisfies ¢. (This no­ tion of subsumption is used in the prediction step of generalized Earley and LR parsing algorithms for fea­ ture structure grammars, see Shieber [19,17] for details.) In the framework described here, ¢; and '1jJ are both quantifier-free formulae (e.g. boolean combinations of arc atoms), so¢ subsumes 7/J iff

"The axioms in 8 do not require that l be (an attribute­ value encoding of) a list. A unary 'sort' predicate that does require this is easily formulated, however. Among other things, this predicate should require that the "empty list" constant nil has neither first nor last arcs leaving it. (This could also be achieved by treating nil as an attribute-value constant).

where A is the relevant feature-structure axiomatization. Clearly, if A is in SB then this notion of subsumption is decidable.

Second, subsumption can be construed as a relation between elements within a feature structure, where e subsumes e', written e ~ e' iff there is a partial en­ domorphism h such that h(e) = e', that preserves attribute-value constants and attributes and their val­ ues (and possibly sorts). (This notion of subsumption is needed to describe the agreement agreement proper­ ties of conjoined phrases; see Shieber (19) for details.) It is straight-forward to axiomatize this in second-order predicate logic by treating the partial endomorphism h as a functional relation (i.e. h(x, y) iff h(x) is defined and equal toy).

Dorre and Rounds (2) have shown the undecidability of conjunctions of subsumption and attribute-value con­ straints, so clearly this notion of subsumption cannot be axiomatized in SB. Perhaps surprisingly, positively occuring subsumption constraints 5 can be axiomatized quite directly in first-order logic in a manner discovered jointly with John Maxwell.

As just formulated, subsumption seems to rely on an existential quantification over partial endomorphisms h, but by

• replacing the bi-conditional with an implication (which does not affect satisfiability if all subsump­ tion constraints occur positively), and
• skolemizing the embedded existential quantification we obtain an equivalent formulation in terms of a four­ place relation h', where h'(e,e',x,y) iff h(x,y), where h is the partial endomorphism whose existence is asserted by the existential in the definition of e ~ e'. The first axiom has the same effect as requiring that h(e) = e'.

The second axiom requires that h' preserve attributes and their values.

The third axiom requires that h' preserve constants.

The fourth axiom requires that h' is functional.

5 A subformula occurs positively iff it is in the scope of an even number of negation symbols. The simplification of a biconditional to an implication when the relation defined by the biconditional appears elsewhere only pooitively is described and proved not to alter satisfiability in (10].

6 Constraint equations and ANY values

Finally, we turn to perhaps the most thorny problem for any theoretical account of feature structures: default values and other non-monotonic constructions. This sec­ tion shows how these notions can be formalized by using circumscription to require satisfying models to be min­ imal models. 6 This approach has two major advantages over other approaches:

• expansion to disjunctive normal form is not re­ quired, and
• a single notion of satisfiability is defined which treats the monotonic and non-monotonic construc­ tions simultaneously.

Several versions of circumscription are discussed in the literature; for an introduction see e.g. Genesereth and Nilsson (4). The pamllel circumscription formula¢' for relations R1 , ··· , Rn in </> has the property that a model M satisfies</>/\</>' iff M is an Rt. ... , Rn-minimal model of¢. (In general </>' is a second-order formula).

An important intuition guiding early work in unifi­ catio:l grammar (especially that of Kaplan and Bres­ nan (12) and Kay (14)) is that only the minimal feature structures satisfying the constraints are of linguistic in­ terest, and that lexical entries and syntactic rules may impose additional conditions that a minimal model has to satisfy in order to be well-formed. This section shows how these intuitions can be formalized using circumscrip­ tion.

For example, most current theories of natural language syntax posit a requirement that all noun-phrases must be assigned a 'case feature' by some syntactic rule or lexical entry. This could be implemented in a feature-structure based system by adding a constraint to all lexical entries for nouns that a minimal model is well-formed only if the associated feature element has a case attribute; this is sometimes called an ANY-value constraint on the case attribute. Similarly, a constmint equation between two entities x =c y is satisfied iff x = y in a minimal model of the attribute-value formulae. (See the discussion on pages 108-110 of Johnson (8) for a more detailed expla­ nation of such constraints.)

"Constraint equations" and ANY values can be treated in the following way. We represent the constraint that an attribute a must be defined on an element x in a minimal model by any(x, a), and constraint equa­ tions by x =c y. Now let ¢ be the conjunction of the equality axioms, the attribute-value axioms and all of the (formulae corresponding to) feature structure con­ straints from a given parse, and let ¢' be the parallel circumscription formula for arc, con and = in ¢. We circumscribe precisely these relations because a minimal model is one which possesses as few arcs as possible, specifies attribute-value constants as the denotation of as few variables as possible, and identifies as equal or "unified" as few pairs of variables as possible (see the definition of the subsumption ordering on attribute-value models in (8)).

6 Femando Pereira suggested to me that circumscription could be used to provide a formal account of non-monotonic feature structure constraints.

Then a model M satisfies all of the constraints (includ­ ing the so-called "defining equations", the "constraint equations" and the ANY constraints) iff

The circumscription of equality requires that two con­ stants denote the same entity (i.e. are "unified") in a model iff interpreting them as denoting distinct entities would result in the violation of some axiom or constraint. The circumscription of arc and con requires that these relations are also minimal.

Note that this formulation restricts attention to "clas­ sical" minimal models. However, for some applications this seems to be too strong. For example, the constraint attached to the NP child in the LFG rule [12]

includes an optional feature structure constraint, which would be represented in the framework described here as

Now, the left-hand disjunct contributes nothing to the truth conditions if disjunction is interpreted classically (since </JV true= true), so this is clearly not the intended interpretation. Rather, Kaplan and Bresnan seem to in­ terpret disjunction as a kind of non-deterministic choice operator, so that all of the minimal models of both <P and 'ljJ are also minimal models of <P V '1/J.

7 Conclusion

This paper has shown how a wide variety of differ­ ent types of feature structures and constraints on them can be described using predicate logic. The decidabil­ ity of the satisfiability problem of many interesting fea­ ture structure systems follows directly from the fact that they can be axiomatized in the Schonfinkel-Bernays class. Further, axiomatizing feature structures in first­ order logic allows us to apply standard techniques to the formalization of non-monotonic feature structure con­ straints.