Bericht Nr. 59, 1994

ISSN 0947-6954/94

Arbeitspapiere des Sonderforschungsbereichs 340

Sprachtheoretische Grundlagen für die Computer linguistik

Paul John King :

An expanded logical formalism for head-driven phrase structure grammar

Universität Stuttgart Universität Tübingen Deutschland Informationssysteme GmbH

An expanded logical formalism for head-driven phrase structure grammar

Paul John King Sonderforschungsbereich 340 Seminar für Sprachwissenschaft Eberhard-Karls-Universität Wilhelmstraße 113 72074 Tübingen Germany Email: king@sfs.nphil.uni-tuebingen.de

4th July, 1994

Abstract. Though [Pollard and Sag 1994] assumes that an unspecified variant of the formal logic of [Carpenter 1992] will provide a formalism for HPSG, a precise formulation of the envisaged formalism is not immediately obvious, primarily because a principal tenet of [Carpenter 1992], that feature structures represent partial information, seems to conflict with a principal tenet of [Pollard and Sag 1994], that feature structures represent abstract linguistic entities. This has caused many HPSGians to be mistakenly concerned with partial-information specific notions, such as subsumption, that are appropriate for the [Carpenter 1992] logic but inappropriate for the formalism [Pollard and Sag 1994] envisages. This paper hopes to allay this concern and the confusion it engenders by substituting [King 1989] for [Carpenter 1992] as the basis of the envisaged formalism. It demonstrates that the formal logic of [King 1989] provides a formalism for HPSG that meets all [Pollard and Sag 1994] asks of the envisaged formalism. It further shows that the most credible variant of the [Carpenter 1992] logic consistent with the aims of [Pollard and Sag 1994] is not only incompatible with the tenet that feature structures represent partial information, but also an instance of the [King 1989] logic.

1 Introduction

A grammar comprises two components: a means to express accounts of natural language fragments, and a collection of accounts of natural language fragments expressed via this means. For facility, I henceforth (mis)use the term ‘formalism’ to refer to the first of these components. Though a natural language can serve as a formalism, a grammar that yields painstaking accounts of extensive natural language fragments requires a more precise formalism. Since mathematics offers peerless precision of expression, many grammarians espouse mathematical formalisms. In particular, researchers have provided a succession of mathematical formalisms for the HPSG (head-driven phrase structure grammar) of [Pollard and Sag 1987] and [Pollard and Sag 1994]. This paper resolves a troubling aspect of the mathematical formalism [Pollard and Sag 1994] envisages for HPSG. However, an understanding of what troubles me and the method I use to resolve it requires a review of earlier HPSG formalisms and a summary of the formalism [Pollard and Sag 1994] envisages.

[Pollard and Sag 1987] originally gave HPSG a formalism that uses mathematical entities called feature structures to represent partial information about linguistic entities, and

Page 2

expresses an account of a natural language fragment as a feature structure representing the partial information about linguistic entities that is available to mature users of the fragment. The feature structures constitute a Heyting algebra (see [Partee et al. 1990, chapter 12]), and the formalism uses the algebraic operations to construct representations of the partial information available to mature users of natural language fragments. [Pollard and Sag 1987] held that some linguistic information is universal, being

the information about language that is available to all normal adult humans by virtue of their shared genetic endowment, independent of which language communities they belong to. [Pollard and Sag 1987, page 44]

[Pollard and Sag 1987] codified this universal linguistic information into a small number of so-called universal principles. All of the universal principles are implicative. For example,

To say that [the head feature principle] is a universal principle is to say: human beings implicitly have the information about any linguistic object—in any language whatsoever—that if it is a phrasal sign then its head features coincide with the head features on its head daughter. [Pollard and Sag 1987, page 44]

In order to construct accurate representations of implicative information, the formalism must meet the condition that a feature structure represents partial information about a linguistic entity iff the pseudocomplement of the feature structure represents partial information not about the entity. However, [King 1989] showed that the formalism does not meet this condition, and researchers consequently pursued three new approaches to providing an HPSG formalism, the first based on the algebra of [Pollard and Sag 1987], the second on the KRL (Kasper-Rounds logic) of [Rounds and Kasper 1986], and the third on the SRL (speciate re-entrant logic) of [King 1989].

HPSG uses a taxonomic system whereby each linguistic entity is assigned one or more symbols called sorts or types in order to encode linguistic-entity well-formedness conditions called appropriateness conditions. The [Pollard 1989] and [Pollard and Moshier 1990] HPSG formalisms retain the [Pollard and Sag 1987] Heyting algebra, but abandon the pseudocomplement operation, and use instead sorts to encode implicative information. The formalisms express an account of a natural language fragment as a total function from sorts to feature structures that assigns each sort a feature structure representing the partial information available to mature fragment users about linguistic entities of that sort. Informally, assigning sort σ feature structure F represents the implicative information ‘if the linguistic entity is of sort σ then F is about the entity’. Thus, implication is not part of the algebra, but is reified as the algebra is used to express a natural language fragment. The formalisms can only express implicative information in which the antecedent is of the form ‘the linguistic entity is of such-and-such a sort’, but many HPSGians believe that, by judiciously reconfiguring the sort taxonomy, these formalisms can express any reasonable HPSG account of a natural language fragment.

Underlying KRL is the intuition that partial information can be accrued. That is, adding information to a first piece of partial information yields a second, more informative piece of partial information. I say that the second piece of partial information elaborates the first. Adding information ad infinitum to a piece of partial information therefore yields an infinite sequence of pieces of partial information, where each successor in the sequence elaborates its predecessor. I call such a sequence an elaboration sequence. One can picture an elaboration sequence as a succession of ever more explicit pieces of partial information tending asymptotically to some limiting piece of ‘total’ information, much like a succession of ever longer decimal numbers tending asymptotically to some limiting real number. I call such a limiting piece of ‘total’ information an ultimate elaboration of the initial piece of partial information. The fundamental presupposition of KRL is that a piece of partial information is significant not only for itself but also for its ultimate elaborations, these being indicated by the elaboration sequences it initiates.

Page 3

Like the [Pollard and Sag 1987] formalism, KRL uses feature structures to represent partial information. KRL uses a subsumption relation to represent elaboration: a first feature structure subsumes a second feature structure iff the partial information the second represents elaborates the partial information the first represents. Thus, KRL represents an elaboration sequence as an infinite sequence of feature structures, where each member of the sequence subsumes its successor. However, unlike the [Pollard and Sag 1987] formalism, KRL uses a formal language to constrain the feature structures. KRL provides a set of formulae, and a satisfaction relation between the feature structures and the formulae. The set of formulae is closed under conjunction and disjunction, and a feature structure satisfies the conjunction/disjunction of two formulae iff the feature structure satisfies the first and/or the second formula. KRL expresses its concern with ultimate elaborations in a condition that I call subsumption monotonicity: if a first feature structure satisfies a formula and subsumes a second feature structure then the second feature structure satisfies the formula. Subsumption monotonicity ensures that if the representation of a piece of partial information satisfies a formula then the representation of each member of each elaboration chain the piece of partial information initiates satisfies the formula, or, more informally, that a formula cannot denote a piece of partial information without ‘denoting’ each of its ultimate elaborations. [Rounds and Kasper 1986] showed that KRL is subsumption monotonic.

A [Pollard and Sag 1987] feature structure and a KRL feature structure differ markedly. However, the EKR (extended Kasper-Rounds logic) of [Moshier 1988] incorporates sorts into KRL such that a [Pollard and Sag 1987] feature structure is a set of EKR feature structures with the set representing the disjunction of the partial information its members represent, and the LTFS (logic of typed feature structures) of [Carpenter 1992] incorporates appropriateness conditions and a richer formal language into EKR. This encouraged some researchers to attempt to base HPSG formalisms on KRL-style logics. However, KRL, EKR and LTFS cannot deliver representations of implicative information. Researchers overcame this limitation in two ways, the first mimicking the [Pollard and Sag 1987] formalism, the second the [Pollard 1989] and [Pollard and Moshier 1990] formalisms. The first method

incorporates negation into a KRL-style logic so that the partial information the set of satisfiers of the negation of a formula represents is the negation of the partial information the set of satisfiers of the formula represents, and expresses an account of a natural language fragment as a KRL-style formula whose satisfiers constitute a [Pollard and Sag 1987] feature structure representing the partial information available to mature fragment users.

This method appears simple at first sight. For example, close the formulae under negation, and extend satisfaction classically so that a feature structure satisfies the negation of a formula iff the feature structure does not satisfy the formula. However, this apparent simplicity is deceptive. Firstly, [Moshier and Rounds 1987] showed that a KRL-style logic with classical negation is not subsumption monotonic. Secondly, in order to deliver accurate representations of implicative information, the formalism must meet the condition that some satisfier of a formula represents partial information about a linguistic entity iff no satisfier of the negation of the formula represents partial information about the entity. It is easy to show that a KRL-style logic with classical negation does not meet this condition. [Moshier and Rounds 1987], [Langholm 1989] and others have proposed various subsumption-monotonic extensions of KRL with nonclassical negations, and these extensions easily adapt to EKR and LTFS, but it remains an open question whether any of these extensions can deliver accurate representations of implicative information. The second method retains a negation-free KRL-style logic, but expresses an account of a natural language fragment as a total function from sorts to KRL-style formulae that

Page 4

assigns each sort a formula whose satisfiers constitute a [Pollard and Sag 1987] feature structure representing the partial information available to mature fragment users about linguistic entities of that sort. [Carpenter 1992] based such an HPSG formalism on LTFS. [Pollard 1989] quantified the parallels between this formalism and the [Pollard 1989] and [Pollard and Moshier 1990] formalisms, and the former both suffers the same expressive limitations and of course merits the same HPSGian confidence as the latter. Moreover, the ALE (attribute logic engine) of [Carpenter 1993] is a computer implementation of LTFS. As a result, the [Carpenter 1992] formalism is very popular among HPSGians.

Underlying SRL is the intuition that a description is a well-formed string of symbols that can be interpreted as true or false of an object. For example, the description ‘it is black’ can be conventionally interpreted as true of a soot particle but false of a snow flake. To formalise this intuition, SRL provides a class of formal languages, each comprising a set of descriptions and a class of interpretations, where each interpretation comprises a universe of objects and a denotation function that assigns each description the collection of objects in the universe of which the description is true. The set of descriptions is closed under negation, conjunction and disjunction. Formally, the denotation of the negation of a description is the complement of the denotation of the description, and the denotation of the conjunction/disjunction of two descriptions is the intersection/union of the denotations of the two descriptions. Informally, the negation of a description describes an entity iff the description does not describe the entity, and the conjunction/disjunction of two descriptions describes an entity iff the first and/or the second description describes the entity.

Though [King 1989] created SRL specifically to provide a formalism for HPSG, partial information plays no part in SRL. Rather, [King 1989] reasoned that partial information in HPSG is actually an irrelevance. [King 1989] observed that [Pollard and Sag 1987] used feature structures sometimes to represent partial information:

The fundamental nature of linguistic information remains a mystery. We cannot look at a piece of linguistic information under a microscope; we aren’t even sure whether to look inside human brains or somewhere else. Still, although we aren’t sure what linguistic information is, we can still theorize about it by trying to say what it is like. To be more precise, we can try to construct formal models that reflect certain interesting aspects of the things we are studying. … In the past several years, theoretical and computational linguists working within a number of distinct research traditions have found it useful to construct formal models of linguistic information. … the formal objects of choice in information-based linguistics are things known as feature structures. [Pollard and Sag 1987, page 27]

sometimes to describe linguistic entities:

In our applications, we will think of feature structures as partial descriptions of signs (or sign tokens) and other linguistic objects which occur as parts of signs.

[Pollard and Sag 1987, page 28]

and sometimes to do both:

Intuitively, a feature structure is just an information-bearing object that describes or represents another thing by specifying values for various attributes of the described thing; we think of the feature structure as providing partial information about the thing described. [Pollard and Sag 1987, page 28]

Evidently, [Pollard and Sag 1987] conflated ‘partial information about a linguistic entity’ with ‘description of a linguistic entity’. In fact, description is the only aspect of partial information the [Pollard and Sag 1987] formalism uses to express an account of a natural language fragment. For example, see the explanation of the head feature principle I quoted earlier from [Pollard and Sag 1987]. [King 1989] argued that in order to meet concerns about irrelevant, nondescriptive aspects of partial information, [Pollard and Sag 1987]

Page 5

had formulated an overly complex formalism unable to meet concerns about the relevant, descriptive aspect of partial information. For example, in order to construct accurate representations of the descriptive aspect of implicative information, the formalism must meet the simple condition that the pseudocomplement of a feature structure describes a linguistic entity iff the feature structure does not describe the entity. Yet, as a means to meet this condition, the formalism is both unnecessarily complicated and demonstrably unsuccessful. Choosing to focus solely on the description of linguistic entities, [King 1989] took each linguistic entity to be an SRL object; substituted SRL descriptions for feature structures, SRL conjunction for meet, SRL disjunction for join, and SRL negation for pseudocomplement; and expressed an account of a natural language fragment as an SRL formula denoting the collection of linguistic entities acceptable to mature fragment users. The [King 1989] formalism’s inherent narrowing of scope from partial information about linguistic entities to linguistic entities alone is both beneficial and detrimental. On the one hand, the [King 1989] formalism can express an account of a natural language fragment without the inaccuracies or expressive limitations of the other HPSG formalisms. On the other, the [King 1989] formalism cannot distinguish between natural language fragments as finely as the other HPSG formalisms can. For example, suppose that I_{1} and I_{2} are the partial information available to mature users of natural language fragments F_{1} and F_{2} respectively. Suppose further that I_{1} and I_{2} are different, but mature users of F_{1} and F_{2} deem exactly the same linguistic entities acceptable. Unlike the other HPSG formalisms, the [King 1989] formalism cannot distinguish between F_{1} and F_{2}.

There is a sharp ontological distinction between KRL-style logics and SRL: a KRL-style logic formalises the accrual of partial information, whereas SRL formalises the description of objects. Thus, partial-information specific notions, such as subsumption, are central to a KRL-style logic, but irrelevant to SRL. The ontological distinction engenders an equally sharp distinction in the HPSG formalisms the logics provide: a KRL-based formalism delivers a representation of partial information, whereas an SRL-based formalism delivers a collection of linguistic entities. Thus, a formula constrains a linguistic entity directly in an SRL-based formalism, but indirectly in a KRL-based formalism: the KRL-style formula constrains a representation of partial information, and the partial information is about the linguistic entity. Classical negation illustrates both differences clearly. Firstly, classical negation conflicts with subsumption monotonicity, an intuition that underlies KRL-style logics, whereas classical negation accords with each intuition that underlies SRL. Secondly, KRL-based HPSG formalisms express each universal principle as implicative information whose accurate representation precludes classical negation, whereas SRL-based HPSG formalisms express each universal principle as an implicative description whose accurate interpretation requires classical negation. However, there is a widespread belief, even among researchers who acknowledge these differences, that, differences of ontology and application apart, SRL is a predicate-logic generalisation of LTFS – the KRL-style logic that most closely resembles SRL – with classical negation. This belief is false. Before showing how it is false I will show how it became prevalent, via a short detour into a formalism for another grammar, the LFG (lexical-functional grammar) of [Kaplan and Bresnan 1982].

[Johnson 1988] created AVL (attribute-value logic) specifically to provide a formalism for LFG. Despite their independent development and a number of nontrivial technical differences, AVL and SRL have much in common, and it is natural to consider AVL and SRL sister logics, the former tailored to LFG, the latter to HPSG. In particular, both are concerned with objects, not partial information. [Johnson 1988] did outline an embedding of KRL within AVL that generalised subsumption from KRL to AVL, but [Johnson 1988] also warned that whereas subsumption formalises the “partiality” that underlies what [Johnson 1988] called “unification approaches”, it formalises nothing in AVL. Several researchers, including perhaps Johnson himself, ignored or underestimated

Page 6

this warning. For example, [Johnson 1988] offered the classical negation of AVL as a means to include negation in the “unification approaches”, and [Smolka 1988] explicitly presented FL (feature logic), an extension of AVL that retains classical negation, as an extension not only of AVL but also of KRL. Conversely, [Carpenter 1992] criticised AVL for not being subsumption monotonic. Nevertheless, even if the [Johnson 1988] warning is heeded, it remains true that AVL is a predicate-logic generalisation of KRL with classical negation. Given the similarity between AVL and SRL, it is unsurprising therefore that many believe SRL is a predicate-logic generalisation of LTFS with classical negation.

The mendacity of this last belief arises from the different provenances of AVL and SRL. LFG is rather flexible about what constitutes a linguistic entity, and one AVL object can appear to be an elaboration of another. This provokes the suspicion that the partialinformation/object distinction is an illusion, an ontological ruse to admit classical negation into KRL. However, the appropriateness conditions make HPSG quite strict about what constitutes a linguistic entity, and each SRL object meets the appropriateness conditions exhaustively. The LTFS feature structures also observe the appropriateness conditions, but only partially. Consequently, an LTFS feature structure cannot ordinarily serve as an SRL object. Later in this paper, I reconfigure the LTFS feature structures to meet the appropriateness conditions exhaustively, and I embed the reconfigured LTFS within SRL. However, the reconfigured feature structures are too large to be ordinary LTFS feature structures, and subsumption over the reconfigured feature structures flattens to feature structure isomorphism.^{1} The reconfigured feature structures represent possibly infinite information that cannot be elaborated. Thus, the partial-information/object distinction that seemed immaterial between KRL and AVL becomes substantial between LTFS and SRL: LTFS can be embedded in SRL only by a reconfiguration of LTFS that nullifies the intuitions of [Carpenter 1992] concerning partial information.

[Pollard and Sag 1994] itself provides no formalism for HPSG, but envisages instead an HPSG formalism that synthesises components taken from several of the HPSG formalisms reviewed above. Like [King 1989], [Pollard and Sag 1994] seeks to express an account of a natural language fragment by denoting the collection of linguistic entities acceptable to mature fragment users. However, [King 1989] and [Pollard and Sag 1994] disagree over both the nature of the linguistic entities, and how to denote them.

[Pollard and Sag 1994] distinguishes between linguistic tokens and linguistic types.^{2} A token is a concrete particular, whereas a type is an abstract universal that signifies a collection of tokens. I say that a type abstracts a token iff the type signifies a collection containing the token. For example, the individual disturbance in air pressure generated by a specific utterance of the English sentence ‘I think’ by a specific person at a specific time in a specific location is a linguistic token, the sequence of English phonemes represented by the string /a� ���k/of IPA (international phonetic alphabet) symbols is a linguistic type, and the latter abstracts the former. Though [King 1989] never mentions tokens, [King 1989] evidently considers linguistic entities to be token-like. [Pollard and Sag 1994] has a different opinion however.

One thing that [language] certainly does not consist of is individual linguistic events or utterance tokens, for knowledge of these is not what is shared among the members of a linguistic community. Instead, what is known in common, that makes communication possible, is the system of linguistic types. For example, the type of the sentence I’m sleepy is part of that system, but no individual token of it is.

[Pollard and Sag 1994, page 14]

1Thus, ironically, [Carpenter 1992] was not only wide of the mark, but also wrong to criticise SRL for not being subsumption monotonic!

2It is unfortunate that [Pollard and Sag 1987] and [Pollard and Sag 1994] use the same term ‘type’, but for different purposes. A [Pollard and Sag 1987] type is actually a [Pollard and Sag 1994] sort. For clarity, I henceforth keep to the [Pollard and Sag 1994] usage.

Page 7

[Pollard and Sag 1994] concedes that the nature of a linguistic type is unclear. Just what sorts of things these linguistic types are is another question. Indeed, the precise ontological status of linguistic types is the subject of a very long-standing debate among various schools of conceptualists (e.g. Ferdinand de Saussure, Noam Chomsky), who take them to be mental objects, and realists (e.g. Leonard Bloomfield, Jerrold Katz, Paul Postal, Jon Barwise), who consider them to belong to extramental reality. Thus we might identify linguistic types with such psychological entities as Saussure’s signs or with certain presumably nonmental objects of situation theory (situation types or perhaps infons). For our part, we doubt that the question of whether objects of knowledge are mental or extramental is an empirical one.

[Pollard and Sag 1994, page 14]

In order to gain a purchase on the recondite linguistic types, [Pollard and Sag 1994] makes the methodological assumption that scientists model empirical objects with corresponding mathematical objects, theorise about the mathematical objects directly, and theorise about the empirical objects indirectly via the correspondence.

In any mathematical theory about an empirical domain, the phenomena of interest are modelled by mathematical structures, certain aspects of which are conventionally understood as corresponding to observables of the domain. The theory itself does not talk directly about the empirical phenomena; instead, it talks about, or is interpreted by, the modelling structures. Thus the predictive power of the theory arises from the conventional correspondence between the model and the empirical domain.

[Pollard and Sag 1994, page 6]

[Pollard and Sag 1994] re-enlists feature structures, albeit to represent linguistic types, not partial information, and envisages expressing an account of a natural language fragment by denoting the collection of feature structures that represent the linguistic entities acceptable to mature fragment users.

In HPSG, the modelling domain … is a system of sorted feature structures, which are intended to stand in a one-to-one relation with types of natural language expressions and their subparts. The role of the linguistic theory is to give a precise specification of which feature structures are to be considered admissible; the types of linguistic entities that correspond to the admissible feature structures constitute the predictions of the theory. [Pollard and Sag 1994, page 8]

[Pollard and Sag 1994] makes very clear that feature structures used to represent partial information differ markedly from feature structures used to represent linguistic types, and that partial-information specific notions, such as subsumption, play no part in the HPSG formalism it envisages. Nonetheless, [Pollard and Sag 1994] assumes that some variant of LTFS will be the basis of the envisaged formalism.

[[Carpenter 1992]] in particular sets forth a logic very close to the one that we assume will underlie a fully formalized version of our theory. In very general terms, this can be characterized as a sorted variant of Kasper and Rounds’s logic (1986) augmented with path inequalities, definite relations, and set values. [Pollard and Sag 1994, page 8] This last assumption troubles me deeply. LTFS is a logic of partial information, but

the formalism [Pollard and Sag 1994] envisages requires a logic of description, and such logics are immiscible in the presence of appropriateness conditions. To settle my disquiet, I do the following in this paper. I use SRL, a logic of description, to build an HPSG formalism that includes tokens, types, type abstraction and type admission. I then build a mathematical model of this formalism. I then use the model to prove that the formalism meets all [Pollard and Sag 1994] asks of the envisaged HPSG formalism. I lastly show that the most credible LTFS variant that meets the requirements of [Pollard and Sag 1994] is not just incompatible with the intuitions about partial information that underlie LTFS, but is in fact an instance of SRL.

Page 8

2 The K-formalism

In this section I use SRL to build an HPSG formalism I call the K-formalism. I review the formal language of SRL, repeating the definitions of [King 1989], but with a small number of minor notational and terminological improvements. I then construct the K-formalism by giving SRL-based definitions of tokens, types, what it is for a type to abstract a token, and what it is for a theory to admit a type.

2.1 The logic

SRL provides a class of formal languages, each comprising a signature and a class of interpretations. The signature provides the syntactic resources from which descriptions are constructed, and each interpretation provides a universe of objects and assigns the syntactic resources a meaning from which a denotation function is generated. 1 Definition. Σ is a signature iff

Σ is a triple ⟨𝔖, 𝔄, 𝔉⟩,

𝔖 is a finite set, 𝔄 is a set, and 𝔉 is a total function from the Cartesian product of 𝔖 and 𝔄 to the powerset of 𝔖.

Strictly, all subsequent work should be done with respect to explicit signatures. However, for notational facility, I work with respect to an implicit signature ⟨𝔖, 𝔄, 𝔉⟩. I call each member of 𝔖 a species, each member of 𝔄 an attribute, and 𝔉 the appropriateness function. I assume that none of the symbols :, ∼, ≈, ¬, [, ], ∧, ∨ or → is a species or an attribute. 2 Definition. I is an interpretation iff

I is a triple ⟨U, S, A⟩,

U is a set,

S is a total function from U to 𝔖,

A is a total function from 𝔄 to the set of partial functions from U to U, for each α ∈ 𝔄 and each u ∈ U,

if A(α)(u) is defined then S(A(α)(u)) ∈ 𝔉⟨S(u), α⟩, and for each α ∈ 𝔄 and each u ∈ U,

if 𝔉⟨S(u), α⟩ is not empty then A(α)(u) is defined. Suppose that I is an interpretation, and I = ⟨U, S, A⟩. I call each member of U an object in I, S a species assignment function, and A an attribute interpretation function. Each species is a symbol that names one of a finite number of categories that partition U, and S assigns each object in I the name of the unique category to which it belongs. Each attribute is a symbol that names one of an arbitrary number of partial functions from U to U, and A assigns each attribute the partial function it names. The appropriateness function encodes, and the last two conditions in the definition of an interpretation enforce, a relationship between the interpretations of species and attributes: if 𝔉⟨σ, α⟩ is empty then the partial function that attribute α names acts upon no object in the category that species σ names, and if 𝔉⟨σ, α⟩ is not empty then the partial function that attribute α names acts upon each object in the category that species σ names to yield an object in a category named by one of the species in 𝔉⟨σ, α⟩.

A term is a : symbol followed by a finite string of attributes, and each interpretation generates a term interpretation function that assigns each term a unary partial function in the interpretation. 3 Definition. τ is a term iff τ is a member of the smallest set 𝔗 such that

: ∈ 𝔗, and

for each α ∈ 𝔄 and each τ ∈ 𝔗, τα ∈ 𝔗.

Page 9

I write 𝔗 for the set of terms. 4 Definition. T is a term interpretation function over I iff

I is an interpretation ⟨U, S, A⟩, T is a total function from 𝔗 to the set of partial functions from U to U, T (:) is the identity function from U to U, and for each α ∈ 𝔄 and each τ ∈ 𝔗,

T (τα) is the functional composition of T (τ) and A(α). For each interpretation I, there is a unique term interpretation function over I. I write T_{I} for the term interpretation function over I. Suppose that I is an interpretation, and I = ⟨U, S, A⟩. T_{I}(:α_{1} … α_{n}) is the functional composition of the unary partial functions in interpretation I named by attributes α_{1}, …, α_{n}.

A description is a finite, well-formed string of species, terms and other symbols, and each interpretation generates a description denotation function that assigns each description a set of objects in the interpretation. 5 Definition. δ is a description iff δ is a member of the smallest set 𝔇 such that

for each σ ∈ 𝔖 and each τ ∈ 𝔗, τ∼σ ∈ 𝔇, for each τ_{1} ∈ 𝔗 and each τ_{2} ∈ 𝔗, τ_{1}≈τ_{2} ∈ 𝔇, for each δ ∈ 𝔇, ¬δ ∈ 𝔇, for each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇, [δ_{1} ∧ δ_{2}] ∈ 𝔇, for each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇, [δ_{1} ∨ δ_{2}] ∈ 𝔇, and for each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇, [δ_{1} → δ_{2}] ∈ 𝔇.

I write 𝔇 for the set of descriptions. I call descriptions of the form τ∼σ and τ_{1}≈τ_{2} atomic. descriptions, and call descriptions of the form ¬δ, [δ_{1}∧δ_{2}], [δ_{1}∨δ_{2}] and [δ_{1} → δ_{2}] compound descriptions. 6 Definition. D is a description denotation function over I iff

I is an interpretation ⟨U, S, A⟩, D is a total function from 𝔇 to the powerset of U, for each σ ∈ 𝔖 and each τ ∈ 𝔗,

D(τ∼σ) = \{u ∈ U |\begin{matrix}T_{I}(τ)(u) is defined, and \\ S(T_{I}(τ)(u)) = σ \end{matrix} \},

for each τ_{1} ∈ 𝔗 and each τ_{2} ∈ 𝔗,

D(τ_{1}≈τ_{2}) = \{u ∈ U |\begin{matrix}T_{I}(τ_{1})(u) is defined, \\ T_{I}(τ_{2})(u) is defined, and \\ T_{I}(τ_{1})(u) = T_{I}(τ_{2})(u) \end{matrix} \},

for each d ∈ 𝔇, D(¬d) = U \ D(d), for each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇, D([δ_{1} ∧ δ_{2}]) = D(δ_{1}) ∩ D(δ_{2}), for each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇, D([δ_{1} ∨ δ_{2}]) = D(δ_{1}) ∪ D(δ_{2}), and for each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇, D([δ_{1} → δ_{2}]) = (U \ D(δ_{1})) ∪ D(δ_{2}).

For each interpretation I, there is a unique description denotation function over I. I write D_{I} for the description denotation function over I. Suppose that I is an interpretation, and I = ⟨U, S, A⟩. Informally, D_{I}(δ) is the set of those objects in interpretation I of which δ is true. Thus, D_{I}(τ∼σ) is the set of those objects u in interpretation I of which

partial function T_{I}(τ) acts upon object u to yield object u′, and object u′ is in the category named by species σ;

D_{I}(τ_{1}≈τ_{2}) is the set of those objects u in interpretation I of which partial function T_{I}(τ_{1}) acts upon object u to yield object u_{1}, partial function T_{I}(τ_{2}) acts upon object u to yield object u_{2}, and object u_{1} and object u_{2} are the same object;

D_{I}(¬δ) is the set of those objects in interpretation I of which description δ is false;

Page 10

D_{I}([δ_{1} ∧ δ_{2}]) is the set of those objects in interpretation I of which description δ_{1} is true and description δ_{2} is true; D_{I}([δ_{1} ∨ δ_{2}]) is the set of those objects in interpretation I of which description δ_{1} is true or description δ_{2} is true; and D_{I}([δ_{1} → δ_{2}]) is the set of those objects in interpretation I of which description δ_{2} is true whenever description δ_{1} is true.

For notational facility, I occasionally write

⊤ for description :≈:, ⊥ for description ¬⊤, ⋁⟨⟩ for description ⊥, ⋁⟨δ⟩ for description δ, and ⋁⟨δ_{0}, …, δ_{n}, δ⟩ for description [⋁⟨δ_{0}, …, δ_{n}⟩ ∨ δ].

Abbreviation ⊤ is true of each object in each interpretation, abbreviation ⊥ is false of each object in each interpretation, and abbreviation ⋁⟨δ_{1}, …, δ_{n}⟩ is the left associative disjunction of descriptions δ_{1}, …, δ_{n}.

A theory is a set of descriptions, and each interpretation builds from its description denotation function a theory denotation function that assigns each theory a set of objects in the interpretation. 7 Definition. θ is a theory iff θ ⊆ 𝔇. 8 Definition. Θ is a theory denotation function over I iff

I is an interpretation,

Θ is a total function from the powerset of 𝔇 to the powerset of U, and for each θ ⊆ 𝔇, Θ(θ) = ⋂{D_{I}(δ) | δ ∈ θ}.

For each interpretation I, there is a unique theory denotation function over I. I write Θ_{I} for the theory denotation function over I. Suppose that I is an interpretation. Θ_{I}(θ) is the set of those objects in interpretation I of which each description in θ is true.

[King 1989] furnished each SRL formal language with a Tarski-style entailment relation and a Hilbert and Ackermann-style deduction relation, and then used standard predicate logic techniques to show that deduction is sound and complete with respect to entailment. However, the K-formalism does not need entailment and deduction, and I do not reproduce this work here.

2.2 The formalism

Since a token is a concrete particular, a token might seem to be an object. However, imagine a type T that abstracts all the tokens that have the same surname as their father, and imagine a stepson who has taken the surname of his stepfather. A lawyer investigating the legal guardianship of the stepson might reasonably consider the stepson’s father to be the stepson’s stepfather, and hence the lawyer might reasonably consider type T to abstract the stepson. However, a doctor investigating the susceptibility of the stepson to a hereditary disorder might equally reasonably consider the stepson’s father to be the stepson’s genetic father, and hence the doctor might equally reasonably consider type T to not abstract the stepson. Thus, if a token were an object then the stepson would be a token that type T both abstracts and does not abstract. Clearly, a token is not an object. Rather, various objects (the stepson, the stepfather and the genetic father, for example) stand in various relations (fatherhood, for example), and a token must comprise at least an object and a record of the various relations in which the object stands. In SRL, an interpretation supplies such a record. Thus, a token is not an object in isolation, but an object in an interpretation. 9 Definition. t is a token iff

t is an ordered pair ⟨u, I⟩,

I is an interpretation ⟨U, S, A⟩, and

u ∈ U.

Page 11

The tokens may constitute a proper class.

A type is an abstract universal that signifies a collection of tokens, and a type abstracts a token iff the type signifies a collection containing the token. Most simply, a type is a collection of tokens that signifies itself, and a type abstracts a token iff the token is in the type. Thus, I need only define what it is for two tokens to be of the same type in order to define types and type abstraction. Two tokens are indiscernible iff no description can tell them apart. 10 Definition. t_{1} and t_{2} are indiscernible iff

t_{1} is a token ⟨u_{1}, I_{1}⟩,

t_{2} is a token ⟨u_{2}, I_{2}⟩, and
for each δ ∈ 𝔇,
u_{1} ∈ D_{I_{1}}(δ) iff u_{2} ∈ D_{I_{2}}(δ).

Two tokens are of the same type iff the tokens are indiscernible. Since indiscernibility is an equivalence relation over the class of tokens, a type is an equivalence class under indiscernibility. 11 Definition. T is a type iff

T is a class of tokens, and

for some t in T, for each token t′,

t′ is in T iff t and t′ are indiscernible. A type may be a proper class. A type abstracts a token iff the token is in the type. 12 Definition. T is a type abstraction of t iff

T is a type, t is a token, and t is in T.

Each token has a unique type abstraction. Also, two tokens are indiscernible iff the tokens have identical type abstractions. 13 Proposition. For each token t_{1} and each token t_{2},

t_{1} and t_{2} are indiscernible iff the type abstraction of t_{1} is the type abstraction of t_{2}. One might think that indiscernibility is too weak to capture the notion ‘of the same

type’, and that some structural isomorphism between tokens would be a more suitable formalisation. For example, the components of a token ⟨u, I⟩ are the objects accessible in interpretation I from object u. 14 Definition. u is a component of t iff

t is a token ⟨u′, I⟩,

I is an interpretation ⟨U, S, A⟩, and

for some τ ∈ 𝔗,

T_{I}(τ)(u′) is defined and T_{I}(τ)(u′) = u.

I write C_{t} for the set of components of t. Two tokens are congruent iff there is a structure and species preserving bijection between their components. 15 Definition. f is a congruence from t_{1} to t_{2} iff

t_{1} is a token ⟨u_{1}, I_{1}⟩,

t_{2} is a token ⟨u_{2}, I_{2}⟩,
I_{1} is an interpretation ⟨U_{1}, S_{1}, A_{1}⟩,
I_{2} is an interpretation ⟨U_{2}, S_{2}, A_{2}⟩,
f is a bijection from C_{t_{1}} to C_{t_{2}},
for each τ ∈ 𝔗 and each u ∈ C_{t_{1}},
T_{I_{1}}(τ)(u_{1}) is defined and T_{I_{1}}(τ)(u_{1}) = u
iff T_{I_{2}}(τ)(u_{2}) is defined and T_{I_{2}}(τ)(u_{2}) = f(u), and
for each u ∈ C_{t_{1}}, S_{1}(u) = S_{2}(f(u)).

Page 12

16 Definition. t_{1} and t_{2} are congruent iff for some f, f is a congruence from t_{1} to t_{2}. One might consider two tokens to be of the same type iff the tokens are congruent. Since congruence is an equivalence relation over the class of tokens, one might therefore consider a type to be an equivalence class under congruence. However, the ‘weak’ and ‘strong’ definitions of a type are actually equivalent. 17 Proposition. For each token t_{1} and each token t_{2},

t_{1} and t_{2} are indiscernible iff t_{1} and t_{2} are congruent. Proof. For each token ⟨u_{1}, I_{1}⟩ and each token ⟨u_{2}, I_{2}⟩,

⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are indiscernible

⟹ \{⟨u′_{1}, u′_{2}⟩ |\begin{matrix}for some τ ∈ 𝔗, \\ T_{I_{1}}(τ)(u_{1}) is defined, \\ T_{I_{1}}(τ)(u_{1}) = u′_{1}, \\ T_{I_{2}}(τ)(u_{2}) is defined, and \\ T_{I_{2}}(τ)(u_{2}) = u′_{2} \end{matrix} \} is a congruence from ⟨u_{1}, I_{1}⟩ to ⟨u_{2}, I_{2}⟩

⟹ ⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are congruent, and

⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are congruent

⟹ for some f, f is a congruence from ⟨u_{1}, I_{1}⟩ to ⟨u_{2}, I_{2}⟩

⟹ for each δ ∈ 𝔇,

u_{1} ∈ D_{I_{1}}(δ) iff u_{2} ∈ D_{I_{2}}(δ) … by induction on the complexity of δ

⟹ ⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are indiscernible.

[Pollard and Sag 1994] tacitly assumes that type admission is recursive. For example, [Pollard and Sag 1994, pages 33–34] uses the English sentence ‘Kim gives Sandy Fido’ to illustrate two universal principles, the head feature principle and the subcategorization principle, and it is evident throughout the illustration that the principles admit ‘Kim gives Sandy Fido’ iff they admit each constituent of ‘Kim gives Sandy Fido’. No type has a structure over which to define admission recursively, but the components provide each token with just such a structure. Consequently, I first define an admission relation between the theories and the tokens such that token admission is recursive over the components of a token, and then naturally abstract the admission relation from tokens to types.

A theory admits a token iff the theory is true of each component of the token. 18 Definition. θ token admits t iff

θ ⊆ 𝔇,

t is a token ⟨u, I⟩, and
C_{t} ⊆ Θ_{I}(θ).

Notice two things. Firstly, token admission is recursive over the components of a token. 19 Lemma. For each object u′ and each token ⟨u, I⟩,

if u′ ∈ C_{⟨u,I⟩} then C_{⟨u′,I⟩} ⊆ C_{⟨u,I⟩}. 20 Proposition. For each θ ⊆ 𝔇 and each token ⟨u, I⟩,

θ token admits ⟨u, I⟩ iff for each u′ ∈ C_{⟨u,I⟩}, θ token admits ⟨u′, I⟩. Secondly, token admission cannot distinguish between indiscernible tokens. 21 Lemma. For each object u, each token ⟨u_{1}, I_{1}⟩, each token ⟨u_{2}, I_{2}⟩ and each f,

if f is a congruence from ⟨u_{1}, I_{1}⟩ to ⟨u_{2}, I_{2}⟩ and u ∈ C_{⟨u_{1},I_{1}⟩}

then the restriction of f to C_{⟨u,I_{1}⟩} is a congruence from ⟨u, I_{1}⟩ to ⟨f(u), I_{2}⟩.

22 Proposition. For each θ ⊆ 𝔇, each token t_{1} and each token t_{2}, if t_{1} and t_{2} are indiscernible and θ token admits t_{1} then θ token admits t_{2}.

Page 13

Proof. For each θ ⊆ 𝔇, each token ⟨u_{1}, I_{1}⟩ and each token ⟨u_{2}, I_{2}⟩, ⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are indiscernible and θ token admits ⟨u_{1}, I_{1}⟩ ⟹ for some congruence f from ⟨u_{1}, I_{1}⟩ to ⟨u_{2}, I_{2}⟩, … by proposition 17

for each object u′_{2}, u′_{2} ∈ C_{⟨u_{2},I_{2}⟩}

⟹ for some u′_{1} ∈ C_{⟨u_{1},I_{1}⟩}, f(u′_{1}) = u′_{2}

⟹ for some u′_{1} ∈ Θ_{I_{1}}(θ), the restriction of f to C_{⟨u′_{1},I_{1}⟩} is a congruence from ⟨u′_{1}, I_{1}⟩ to ⟨u′_{2}, I_{2}⟩ … by lemma 21

⟹ for some u′_{1} ∈ Θ_{I_{1}}(θ), ⟨u′_{1}, I_{1}⟩ and ⟨u′_{2}, I_{2}⟩ are indiscernible

… by proposition 17

⟹ u′_{2} ∈ Θ_{I_{2}}(θ)

⟹ θ token admits ⟨u_{2}, I_{2}⟩.

By propositions 13 and 22, I can felicitously abstract admission from tokens to types. 23 Definition. θ type admits T iff

θ ⊆ 𝔇,

T is a type, and

for some (or equivalently, each) t in T, θ token admits t.

3 A mathematical model of the K-formalism

In this section I build a mathematical model of the K-formalism that facilitates subsequent proofs that the K-formalism meets all [Pollard and Sag 1994] demands of the envisaged HPSG formalism. I construct mathematical entities I call morphs, and define what it is for a morph to abstract a token, and what it is for a theory to admit a morph. I then define a one-to-one correspondence between the types and the morphs, and show that a type abstracts a token iff the corresponding morph abstracts the token, and a theory admits a type iff the theory admits the corresponding morph.

3.1 The morphs

[Nerode 1958] gave an elegant representation of an automaton^{3} that abstracts away from the states of the automaton. Pair ⟨Δ, Γ⟩ is the Nerode representation of automaton A over input alphabet I iff

Δ = \{w |\begin{matrix}w is a finite string of symbols from I, and \\ A transits from its initial state on input w \end{matrix} \}, and

Γ = \{⟨w_{1}, w_{2}⟩ |\begin{matrix}w_{1} is a finite string of symbols from I, \\ w_{2} is a finite string of symbols from I, \\ A transits from its initial state to some state q_{1} on input w_{1}, \\ A transits from its initial state to some state q_{2} on input w_{2}, and \\ q_{1} = q_{2} \end{matrix} \}.

Each automaton has a unique Nerode representation. Further, pair ⟨Δ, Γ⟩ is the Nerode representation of some automaton over input alphabet I iff

Δ is a nonempty set of finite strings of symbols from I,

for each symbol i from I and each finite string w of symbols from I, if wi ∈ Δ then w ∈ Δ,

3[Hopcroft and Ullman 1979] covers much of the automata theory I use in this paper. Notice, I assume that each automaton is rooted and deterministic, but I impose no finiteness restrictions on the states, transitions or alphabets of automata.

Page 14

Γ is an equivalence relation over Δ, and for each symbol i from I, each finite string w_{1} of symbols from I and each finite string w_{2} of symbols from I,

if w_{1}i ∈ Δ and ⟨w_{1}, w_{2}⟩ ∈ Γ then ⟨w_{1}i, w_{2}i⟩ ∈ Γ. [Moore 1956] allowed an automaton to output symbols. A Moore automaton over input alphabet I and output alphabet O is an automaton over input alphabet I that outputs a symbol from O at each state. [Moshier 1988, section 3.1.3] extended Nerode representation to give an equally elegant representation of a Moore automaton. Triple ⟨Δ, Γ, Λ⟩ is the Moshier representation of Moore automaton A over input alphabet I and output alphabet O iff

⟨Δ, Γ⟩ is the Nerode representation of A, and

Λ = \{⟨w, o⟩ |\begin{matrix}w is a finite string of symbols from I, \\ o is a symbol from O, \\ A transits from its initial state to some state q on input w, and \\ A outputs o at state q \end{matrix} \}.

Each Moore automaton has a unique Moshier representation. Further, triple ⟨Δ, Γ, Λ⟩ is the Moshier representation of some Moore automaton over input alphabet I and output alphabet O iff

Δ is a nonempty set of finite strings of symbols from I, for each symbol i from I and each finite string w of symbols from I,

if wi ∈ Δ then w ∈ Δ, Γ is an equivalence relation over Δ, for each symbol i from I, each finite string w_{1} of symbols from I and each finite string w_{2} of symbols from I,

if w_{1}i ∈ Δ and ⟨w_{1}, w_{2}⟩ ∈ Γ then ⟨w_{1}i, w_{2}i⟩ ∈ Γ, Λ is a total function from Δ to O, and for each finite string w_{1} of symbols from I and each finite string w_{2} of symbols from I,

if ⟨w_{1}, w_{2}⟩ ∈ Γ then Λ(w_{1}) = Λ(w_{2}). I say that A is a special automaton iff

A is a Moore automaton over input alphabet 𝔄 and output alphabet 𝔖, for each σ_{1} ∈ 𝔖, each σ_{2} ∈ 𝔖, each α ∈ 𝔄, each state q_{1} of A and each state q_{2} of A,

if A transits from q_{1} to q_{2} on input α,

A outputs σ_{1} at q_{1}, and
A outputs σ_{2} at q_{2}
then σ_{2} ∈ 𝔉⟨σ_{1}, α⟩, and

for each σ ∈ 𝔖, each α ∈ 𝔄 and each state q of A,

if A outputs σ at q, and 𝔉⟨σ, α⟩ is not empty

then A transits from q on input α. A morph is the Moshier representation of a special automaton. 24 Definition. ω is a word iff

ω is a finite string of attributes. I write 𝔚 for the set of words. 25 Definition. M is a morph iff

M is a triple ⟨Δ, Γ, Λ⟩, Δ is a nonempty subset of 𝔚, for each α ∈ 𝔄 and each ω ∈ 𝔚,

if ωα ∈ Δ then ω ∈ Δ,

Page 15

Γ is an equivalence relation over Δ, for each α ∈ 𝔄, each ω_{1} ∈ 𝔚 and each ω_{2} ∈ 𝔚,

if ω_{1}α ∈ Δ and ⟨ω_{1}, ω_{2}⟩ ∈ Γ then ⟨ω_{1}α, ω_{2}α⟩ ∈ Γ, Λ is a total function from Δ to 𝔖, for each ω_{1} ∈ 𝔚 and each ω_{2} ∈ 𝔚,

if ⟨ω_{1}, ω_{2}⟩ ∈ Γ then Λ(ω_{1}) = Λ(ω_{2}), for each α ∈ 𝔄 and each ω ∈ 𝔚,

if ωα ∈ Δ then Λ(ωα) ∈ 𝔉⟨Λ(ω), α⟩, and for each α ∈ 𝔄 and each ω ∈ 𝔚,

if ω ∈ Δ and 𝔉⟨Λ(ω), α⟩ is not empty then ωα ∈ Δ. I write 𝔐 for the set of morphs.

If morph M is the Moshier representation of special automaton A, and A transits from its initial state to state q on input word ω then the ω submorph of M is the Moshier representation of the special subautomaton of A that has initial state q. 26 Definition. M′ is an ω submorph of M iff

M′ is a morph ⟨Δ′, Γ′, Λ′⟩ M is a morph ⟨Δ, Γ, Λ⟩, ω ∈ Δ, Δ′ = {ω′ |ωω′ ∈ Δ }, Γ′ = {⟨ω_{1}, ω_{2}⟩ |⟨ωω_{1}, ωω_{2}⟩ ∈ Γ }, and Λ′ = {⟨ω′, σ⟩ |⟨ωω′, σ⟩ ∈ Λ }.

For each ⟨Δ, Γ, Λ⟩ ∈ 𝔐 and each ω ∈ Δ, there is a unique ω submorph of ⟨Δ, Γ, Λ⟩.

A morph abstracts a token iff the morph represents exactly the atomic descriptions that are true of the token. 27 Definition. M is a morph abstraction of t iff

M is a morph ⟨Δ, Γ, Λ⟩, t is a token ⟨u, I⟩, for each ω_{1} ∈ 𝔚 and each ω_{2} ∈ 𝔚,

⟨ω_{1}, ω_{2}⟩ ∈ Γ iff u ∈ D_{I}(:ω_{1}≈:ω_{2}), and for each ω ∈ 𝔚 and each σ ∈ 𝔖,

⟨ω, σ⟩ ∈ Λ iff u ∈ D_{I}(:ω∼σ). Each token has a unique morph abstraction. Also, two tokens are indiscernible iff the tokens have identical morph abstractions. 28 Proposition. For each token t_{1} and each token t_{2},

t_{1} and t_{2} are indiscernible iff the morph abstraction of t_{1} is the morph abstraction of t_{2}.

Proof. For each token ⟨u_{1}, I_{1}⟩ and each token ⟨u_{2}, I_{2}⟩, ⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are indiscernible ⟹ the morph abstraction of ⟨u_{1}, I_{1}⟩ is the morph abstraction of ⟨u_{2}, I_{2}⟩

and the morph abstraction of ⟨u_{1}, I_{1}⟩ is the morph abstraction of ⟨u_{2}, I_{2}⟩ ⟹ for each δ ∈ 𝔇,

u_{1} ∈ D_{I_{1}}(δ) iff u_{2} ∈ D_{I_{2}}(δ) … by induction on the complexity of δ ⟹ ⟨u_{1}, I_{1}⟩ and ⟨u_{2}, I_{2}⟩ are indiscernible.

A description approximates a morph iff the description and the set of atomic descriptions that the morph represents are consistent.

Page 16

29 Definition. δ approximates M iff ⟨δ, M⟩ is a member of the smallest set A such that

for each σ ∈ 𝔖, each ω ∈ 𝔚 and each morph ⟨Δ, Γ, Λ⟩,

if ⟨ω, σ⟩ ∈ Λ then ⟨:ω∼σ, ⟨Δ, Γ, Λ⟩⟩ ∈ A, for each ω_{1} ∈ 𝔚, each ω_{2} ∈ 𝔚 and each morph ⟨Δ, Γ, Λ⟩,

if ⟨ω_{1}, ω_{2}⟩ ∈ Γ then ⟨:ω_{1}≈:ω_{2}, ⟨Δ, Γ, Λ⟩⟩ ∈ A, for each δ ∈ 𝔇 and each morph M,

if ⟨δ, M⟩ ∉ A then ⟨¬δ, M⟩ ∈ A, for each δ_{1} ∈ 𝔇, each δ_{2} ∈ 𝔇 and each morph M,

if ⟨δ_{1}, M⟩ ∈ A and ⟨δ_{2}, M⟩ ∈ A then ⟨[δ_{1} ∧ δ_{2}], M⟩ ∈ A, for each δ_{1} ∈ 𝔇, each δ_{2} ∈ 𝔇 and each morph M,

if ⟨δ_{1}, M⟩ ∈ A or ⟨δ_{2}, M⟩ ∈ A then ⟨[δ_{1} ∨ δ_{2}], M⟩ ∈ A, and for each δ_{1} ∈ 𝔇, each δ_{2} ∈ 𝔇 and each morph M,

if ⟨δ_{1}, M⟩ ∉ A or ⟨δ_{2}, M⟩ ∈ A then ⟨[δ_{1} → δ_{2}], M⟩ ∈ A. A theory admits a morph iff every description in the theory approximates every submorph of the morph. 30 Definition. θ morph admits M iff

θ ⊆ 𝔇, M is a morph ⟨Δ, Γ, Λ⟩, and for each δ ∈ θ and each ω ∈ Δ, δ approximates the ω submorph of M.

Notice that morph admission is recursive over the submorphs of a morph. 31 Proposition. For each θ ⊆ 𝔇 and each ⟨Δ, Γ, Λ⟩ ∈ 𝔐,

θ morph admits ⟨Δ, Γ, Λ⟩ iff for each ω ∈ Δ, θ morph admits the ω submorph of ⟨Δ, Γ, Λ⟩.

3.2 A correspondence

A morph is an image of a type iff the morph and the type abstract a common token. 32 Definition. M is an image of T iff

M ∈ 𝔐, T is a type, and for some t in T, M is the morph abstraction of t.

Image is functional and injective by propositions 13 and 28, but proving that image is surjective requires proving that morph abstraction is surjective. To this end, I construct mathematical entities I call standard tokens, and show that each morph abstracts some standard token.

I say that pair ⟨A, q⟩ is a focused automaton over input alphabet I iff A is an automaton over input alphabet I, and q is a state of A.

Nerode representation easily extends to focused automata. Triple ⟨Δ, Γ, E⟩ is the Nerode representation of focused automaton ⟨A, q⟩ over input alphabet I iff

⟨Δ, Γ⟩ is the Nerode representation of A, and

E = \{w |\begin{matrix}w is a finite string of symbols from I, and \\ A transits from its initial state to q on input w \end{matrix} \}.

Each focused automaton has a unique Nerode representation. Further, triple ⟨Δ, Γ, E⟩ is the Nerode representation of some focused automaton over input alphabet I iff

Δ is a nonempty set of finite strings of symbols from I, for each symbol i from I and each finite string w of symbols from I,

if wi ∈ Δ then w ∈ Δ,

Page 17

Γ is an equivalence relation over Δ,

for each symbol i from I, each finite string w_{1} of symbols from I and each finite string w_{2} of symbols from I,

if w_{1}i ∈ Δ and ⟨w_{1}, w_{2}⟩ ∈ Γ then ⟨w_{1}i, w_{2}i⟩ ∈ Γ, and E is an equivalence class under Γ.

One can similarly speak of a focused Moore automaton, and extend Moshier representation to focused Moore automata. A standard object is the Moshier representation of a focused special automaton. 33 Definition. u is a standard object iff

u is a quadruple ⟨Δ, Γ, Λ, E⟩, ⟨Δ, Γ, Λ⟩ is a morph, and E is an equivalence class under Γ.

I write Ũ for the set of standard objects. If focused special automaton ⟨A, q⟩ outputs species σ at q then the standard species assignment function assigns σ to the Moshier representation of ⟨A, q⟩. 34 Definition. f is a standard species assignment function iff

f is a total function from Ũ to 𝔖, and

for each σ ∈ 𝔖 and each standard object ⟨Δ, Γ, Λ, E⟩,

f⟨Δ, Γ, Λ, E⟩ = σ iff for some (or equivalently, each) ω ∈ E, Λ(ω) = σ. There is a unique standard species assignment function. I write S̃ for the standard species assignment function. If focused special automaton ⟨A, q_{1}⟩ transits from q_{1} to state q_{2} on input attribute α then the standard attribute interpretation function assigns α a partial function that maps the Moshier representation of ⟨A, q_{1}⟩ to the Moshier representation of ⟨A, q_{2}⟩. 35 Definition. f is a standard attribute interpretation function iff

f is a total function from 𝔄 to the set of partial functions from Ũ to Ũ, and for each α ∈ 𝔄, each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ and each ⟨Δ′, Γ′, Λ′, E′⟩ ∈ Ũ,

f(α)⟨Δ, Γ, Λ, E⟩ is defined and f(α)⟨Δ, Γ, Λ, E⟩ = ⟨Δ′, Γ′, Λ′, E′⟩
iff ⟨Δ, Γ, Λ⟩ = ⟨Δ′, Γ′, Λ′⟩ and for some ω ∈ E, ωα ∈ E′.

There is a unique standard attribute interpretation function. I write Ã for the standard attribute interpretation function. 36 Proposition. ⟨Ũ, S̃, Ã⟩ is an interpretation. 37 Definition. I is the standard interpretation iff I is the interpretation ⟨Ũ, S̃, Ã⟩. I write Ĩ for the standard interpretation. 38 Definition. t is a standard token iff t is a token ⟨u, Ĩ⟩. Each morph is the morph abstraction of some standard token. 39 Lemma. For each ω ∈ 𝔚, each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ and each ⟨Δ′, Γ′, Λ′, E′⟩ ∈ Ũ,

T_{I}(:ω)⟨Δ, Γ, Λ, E⟩ is defined and T_{I}(:ω)⟨Δ, Γ, Λ, E⟩ = ⟨Δ′, Γ′, Λ′, E′⟩

iff ⟨Δ, Γ, Λ⟩ = ⟨Δ′, Γ′, Λ′⟩ and for some ω′ ∈ E, ω′ω ∈ E′.

Proof. By induction on the length of ω. 40 Lemma. For each ω ∈ 𝔚 and each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ,

if ω ∈ E then the ω submorph of ⟨Δ, Γ, Λ⟩ is the morph abstraction of ⟨⟨Δ, Γ, Λ, E⟩, Ĩ⟩. 41 Lemma. For each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ,

if the empty word is in E then ⟨Δ, Γ, Λ⟩ is the morph abstraction of ⟨⟨Δ, Γ, Λ, E⟩, Ĩ⟩. 42 Proposition. For each M ∈ 𝔐, for some standard token t,

M is the morph abstraction of t. Thus, image is a one-to-one correspondence between the types and the morphs.

Page 18

43 Proposition.

For each type T, for some unique M, M is an image of T. For each M ∈ 𝔐, for some unique T, M is an image of T.

Notice a nice consequence of this proposition. A type may be a proper class, but the types constitute a ‘set sized’ class of classes!

Image provides a correlation between type abstraction and morph abstraction. 44 Proposition. For each token t,

the image of the type abstraction of t is the morph abstraction of t. Proof. From propositions 13 and 28. Image also provides a correlation between type admission and morph admission. 45 Lemma. For each token ⟨u, I⟩ and each ⟨Δ, Γ, Λ⟩ ∈ 𝔐,

if ⟨Δ, Γ, Λ⟩ is the morph abstraction of ⟨u, I⟩

then for each M ∈ 𝔐 and each ω ∈ 𝔚, T_{I}(:ω)(u) is defined and M is the morph abstraction of ⟨T_{I}(:ω)(u), I⟩ iff ω ∈ Δ and M is the ω submorph of ⟨Δ, Γ, Λ⟩.

46 Lemma. For each δ ∈ 𝔇 and each token ⟨u, I⟩,

u ∈ D_{I}(δ) iff δ approximates the morph abstraction of ⟨u, I⟩. Proof. By induction on the complexity of δ. 47 Lemma. For each θ ⊆ 𝔇 and each token t,

θ token admits t iff θ morph admits the morph abstraction of t. Proof. For each θ ⊆ 𝔇, each token ⟨u, I⟩ and each ⟨Δ, Γ, Λ⟩ ∈ 𝔐,

if ⟨Δ, Γ, Λ⟩ is the morph abstraction of ⟨u, I⟩

then θ token admits ⟨u, I⟩ ⟺ for each δ ∈ θ and each u′ ∈ C_{⟨u,I⟩}, u′ ∈ D_{I}(δ)

⟺ for each δ ∈ θ and each u′ ∈ C_{⟨u,I⟩},

δ approximates the morph abstraction of ⟨u′, I⟩ … by lemma 46 ⟺ for each δ ∈ θ and each ω ∈ Δ,

δ approximates the ω submorph of ⟨Δ, Γ, Λ⟩ … by lemma 45 ⟺ θ morph admits ⟨Δ, Γ, Λ⟩.

48 Proposition. For each θ ⊆ 𝔇 and each type T,

θ type admits T iff θ morph admits the image of T. Proof. From lemma 47 and propositions 13 and 28. Thus, a type abstracts a token iff the image of the type abstracts the token, and a theory admits a type iff the theory admits the image of the type.

4 The appositeness of the K-formalism

In this section I prove that the K-formalism meets all [Pollard and Sag 1994] asks of the envisaged HPSG formalism. I extract an exact definition of a [Pollard and Sag 1994] feature structure, demonstrate a one-to-one correspondence between the morphs and the feature structures, and show that the K-formalism types correspond to the types [Pollard and Sag 1994] envisages. I then propose a plausible definition of [Pollard and Sag 1994] feature structure admission, demonstrate that a theory admits a morph iff the theory admits the corresponding feature structure, and show that if my definition of feature structure admission is true then K-formalism type admission corresponds to the type admission [Pollard and Sag 1994] envisages.

Page 19

4.1 The feature structures

[Pollard and Sag 1994] does not define a feature structure, but references [Moshier 1988], [Pollard and Moshier 1990] and [Carpenter 1992] instead. These sources define several kinds of feature structure, and [Pollard and Sag 1994] favours no one particular kind. However, [Moshier 1988], [Pollard and Moshier 1990] and [Carpenter 1992] all agree that a feature structure is either a Moore automaton over input alphabet 𝔄 or an isomorphism class of such automata. Additionally, [Pollard and Sag 1994] remarks that

the feature structures employed in HPSG are sorted. This means simply that each node is labelled with a sort symbol that tells what type of object the structure is modelling … Second, we require feature structures to be well-typed (Carpenter 1992). This means that what attribute (or, equivalently, feature) labels can appear in a feature structure are determined by its sort; this fact is the reflection within the model of the fact that what attributes (or, equivalently, features or components of structure) an empirical object has depends on its ontological category. … In addition, given a sort of feature structure and an attribute label appropriate for that sort, the value of that attribute must also be of a sort appropriate for the given sort and attribute label. … Third, feature structures that serve as models of linguistic entities are required to satisfy further criteria of completeness. Roughly what this means is that they are total (not merely partial) models of the objects that they represent. More precisely, they are required to be both totally well-typed (Carpenter 1992) and sort-resolved. A feature structure is totally well-typed in case it is well-typed, and, moreover, for each node, every feature that is appropriate for the sort assigned to that node is actually present. … A feature structure is sort-resolved provided every node is assigned a sort label that is maximal (i.e. most specific) in the sort ordering.

[Pollard and Sag 1994, pages 17 and 18]

Of the sorts, [Pollard and Sag 1994] says that

The (finite) set of all sort symbols is assumed to be partially ordered,

[Pollard and Sag 1994, pages 17 and 18]

and adds that The sort hierarchy is presented as a taxonomic tree, with the root labelled object (the sort of all linguistic entities with which the grammar deals). For each local tree in the hierarchy, the sorts σ_{1}, …, σ_{n}, which label the daughters, partition the sort σ, which labels the mother; that is, they are necessarily disjoint subsorts of σ that exhaust σ. For two sorts σ and τ, τ is a subsort of σ if and only if it is dominated by σ; sorts that label terminal nodes are called maximal (in the sense of maximally informative or maximally specific). A feature declaration of the form

σ : [\begin{matrix}F_{1} & τ_{1} \\ … \\ F_{n} & τ_{n} \end{matrix} ]

where σ, τ_{1}, …, τ_{n} are sorts and F_{1}, …,F_{n} are feature labels, signifies that for each i = 1, …, n, (1) the feature F_{i} is appropriate for all objects of sort σ, and (2) for any such object, the value of the F_{i} feature must be an object of sort τ_{i}. If sorts σ_{1} and σ_{2} bear declarations [F τ_{1} ] and [F τ_{2} ] for the same feature F and σ_{2} is a subsort of of σ_{1}, then τ_{2} must be a subsort of τ_{1}. A sort inherits the feature declarations of its supersorts; hence any feature that is defined for a given sort is defined for all of that sort’s subsorts. By convention, the features that are declared for a maximal sort (including those inherited from its supersorts) are the only features defined for that sort. [Pollard and Sag 1994, page 395]

Page 20

Thus, the sorts comprise a finite partial order, a sort is maximal iff the sort has no proper subsorts (sic), a sort is root iff the sort is a supersort of each sort, and the sort partial order has a root sort. Further, under each interpretation, each sort denotes a set of objects in the interpretation, the root sort denotes the set of all objects in the interpretation, the denotation of a sort is partitioned by the denotations of its maximal subsorts, and each attribute names a unary partial function from objects to objects in the interpretation that is defined on all or no objects in the denotation of each maximal sort. From the foregoing, [King 1989, pages 46–48] deduced a simple relationship between the sorts and the species:

Each maximal sort is a species.

Attribute α is appropriate for maximal sort σ iff 𝔉⟨σ, α⟩ is not empty.

If maximal sort σ bears feature declaration [α τ ] then 𝔉⟨σ, α⟩ is the set of maximal subsorts of τ.

A [Pollard and Sag 1994] feature structure is therefore either a special automaton or an isomorphism class of special automata, and [Pollard and Sag 1994]’s stated intention that the feature structures “stand in a one-to-one relation” with the types precludes the former. To prove this, suppose that a feature structure is a special automaton, and that A_{1} and A_{2} are distinct but isomorphic feature structures that model types T_{1} and T_{2} respectively. The feature structures stand in a one-to-one relation with the types, and A_{1} and A_{2} are distinct. Therefore, T_{1} and T_{2} are distinct. However, states play no conceivable role in the one-to-one relation between feature structures and types, and A_{1} and A_{2} are isomorphic. Therefore, T_{1} and T_{2} are identical. To avoid reductio ad absurdum, a feature structure must be an isomorphism class of special automata. Notice that a feature structure may be a proper class, since the special automata may constitute a proper class.

There is a simple correlation between the morphs and the [Pollard and Sag 1994] feature structures. I say that feature structure F is the twin of morph M iff M is the Moshier representation of some special automaton in F. Reworking [Moshier 1988, corollary 2] and [Moshier 1988, lemma 5] shows that two special automata are isomorphic iff the automata have identical Moshier representations, and that each morph is the Moshier representation of a special automaton. Thus, twin is a one-to-one correspondence between the morphs and the feature structures. Further, by propositions 43, the composition of image and twin is a one-to-one correspondence between the K-formalism types and the feature structures. Thus, the K-formalism types correspond to the types [Pollard and Sag 1994] envisages.

4.2 Feature structure admission

[Pollard and Sag 1994] says very little about feature structure admission, and I cannot extract an exact definition. However, I base a plausible definition of feature structure admission on the [Pollard and Sag 1994] claim that LTFS is “very close to the [logic] that we assume will underlie a fully formalised version of our theory.”

The LTFS formal language easily adapts to special automata and SRL descriptions. Satisfaction becomes the smallest relation between the special automata and 𝔇 such that

for each special automaton A, each σ ∈ 𝔖 and each ω ∈ 𝔚,

if A transits from its initial state to state q on input ω, and

A outputs σ at q then A satisfies :ω∼σ,

for each special automaton A, each ω_{1} ∈ 𝔚 and each ω_{2} ∈ 𝔚, if A transits from its initial state to state q_{1} on input ω_{1},

A transits from its initial state to state q_{2} on input ω_{2}, and q_{1} = q_{2}

then A satisfies :ω_{1}≈:ω_{2},

Page 21

for each special automaton A and each δ ∈ 𝔇, if A does not satisfy δ then A satisfies ¬δ,

for each special automaton A, each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇,

if A satisfies δ_{1} and A satisfies δ_{2} then A satisfies [δ_{1} ∧ δ_{2}], for each special automaton A, each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇,

if A satisfies δ_{1} or A satisfies δ_{2} then A satisfies [δ_{1} ∨ δ_{2}], and for each special automaton A, each δ_{1} ∈ 𝔇 and each δ_{2} ∈ 𝔇,

if A does not satisfy δ_{1} or A satisfies δ_{2} then A satisfies [δ_{1} → δ_{2}]. As said earlier, [Pollard and Sag 1994] tacitly assumes that type admission, and hence

feature structure admission, is recursive. A feature structure, being an isomorphism class of special automata, has no structure over which to define admission recursively, but the subautomata provide each special automaton with just such a structure. Echoing my strategy for defining type admission, I first define an admission relation between the theories and the special automata such that special automaton admission is recursive over the subautomata of a special automaton, and then naturally abstract the admission relation from special automata to feature structures.

I say that

θ ⊆ 𝔇 admits special automata A iff each subautomaton of A satisfies each δ ∈ θ. Clearly,

θ ⊆ 𝔇 admits special automaton A iff θ admits each subautomaton of A. Thus, admission is recursive over the subautomata of a special automaton. Equally clearly,

for each special automaton A_{1}, each special automaton A_{2} and each state q in A_{1}, the restriction of Moore automaton isomorphism f to the states of the q subautomaton of A_{1} is a Moore automaton isomorphism from the q subautomaton of A_{1} to the f(q) subautomaton of A_{2}.

Thus, by induction on the complexity of δ, if A_{1} and A_{2} are isomorphic special automata and A_{1} satisfies δ ∈ 𝔇 then A_{2} satisfies δ.

Thus, if A_{1} and A_{2} are isomorphic special automata and θ ⊆ 𝔇 admits A_{1} then θ admits A_{2}.

Thus, admission cannot distinguish between isomorphic special automata. I can therefore felicitously abstract admission from special automata to feature structures. I say that

θ ⊆ 𝔇 admits feature structure F

iff θ admits some (or equivalently, each) special automaton in F.

There is a simple correlation between morph admission and feature structure admission. By induction on the complexity of δ,

special automaton A satisfies δ ∈ 𝔇

iff δ approximates the Moshier representation of A. Thus, a theory admits a morph iff the theory admits the twin of the morph. Further, by propositions 48, a theory admits a K-formalism type iff the theory admits the twin of the image of the type. Thus, if my definition of feature structure admission is true then K-formalism type admission corresponds to the type admission [Pollard and Sag 1994] envisages.

Page 22

5 The C-formalism

The feature structures and feature structure admission of the previous section constitute an extremely credible candidate for the HPSG formalism [Pollard and Sag 1994] envisages. I call this formalism the C-formalism, and I call the variant of the LTFS formal language upon which it is based LTFS+. In the previous section I established a correlation between the K- and C-formalisms. Yet this correlation is genuinely surprising. The K-formalism is based upon the formal language of the SRL of [King 1989], whereas the C-formalism is based upon LTFS+, a variant of the formal language of the LTFS of [Carpenter 1992]. SRL is a logic of description, LTFS is a logic of partial information, and the appropriateness conditions of HPSG ought to prevent any correlation between such logics. In this section I solve this conundrum by showing that, despite its ancestry, LTFS+ does not share the partial-information hallmarks of LTFS, and is actually an instance of SRL. I occasionally assume a good knowledge of [Carpenter 1992] in this section.

LTFS+ is an adaptation of the formal language of LTFS to special automata and SRL descriptions, where a special automaton is a Moore automaton A over input alphabet 𝔄 and output alphabet 𝔖 such that

(1) for each σ_{1} ∈ 𝔖, each σ_{2} ∈ 𝔖, each α ∈ 𝔄, each state q_{1} of A and each state q_{2} of A,

if A transits from q_{1} to q_{2} on input α,

A outputs σ_{1} at q_{1}, and
A outputs σ_{2} at q_{2}

then σ_{2} ∈ 𝔉⟨σ_{1}, α⟩, and

(2) for each σ ∈ 𝔖, each α ∈ 𝔄 and each state q of A,

if A outputs σ at q, and 𝔉⟨σ, α⟩ is not empty

then A transits from q on input α. Let us suppose for the moment that special automata represent information. Conditions (1) and (2) have an extremely significant effect upon the kind of information a special automaton represents. As explained earlier, the appropriateness function 𝔉 encodes a relationship between the interpretations of species and attributes, and SRL encodes the HPSG appropriateness conditions in the appropriateness function. The definition of an interpretation enforces the relationship the appropriateness function encodes, and thus ensures every object in every universe exhaustively meets the appropriateness conditions. A special automaton that failed to meet condition (1) would represent species and attribute information that could only be about an ill-formed object, and adding species or attribute information to a special automaton that met condition (2) would yield a special automaton that failed to meet condition (1). Thus, conditions (1) and (2) ensure that a special automaton represents maximal species and attribute information that accords with the appropriateness conditions. However, a special automaton does not necessarily represent maximal information simpliciter, because a re-entrancy representing the information that two components of an object are identical can be added to a special automaton without contradicting condition (1) or (2). Subsumption supports all these intuitions: if a first special automaton subsumes a second then the only possible difference between the two is that the second has re-entrancies the first lacks. To summarise this first intuitive picture: a special automaton represents maximal species and attribute information, but partial equational information. It is as if one knows everything about species and attributes, but one can acquire information about equations.

I find this part maximal, part partial picture very unsatisfactory. The maximality of the species and attribute information is a deliberate consequence of conditions (1) and (2), but the partiality of the equational information is an accidental consequence of a representational limitation of the special automata. Though re-entrancy enables a special

Page 23

automaton to represent the information that two components of an object are identical, no mechanism enables a special automaton to represent the information that two components of an object are distinct. Faced with a similar limitation, [Carpenter 1992, chapter 7] added an anti-reflexive and symmetric “inequality relation” to the [Carpenter 1992] feature structures, took each pair of inequated states to represent the information that the relevant components of an object are distinct, and modified subsumption to prevent re-entrancies overriding inequations. I make a similar addition to the special automata. I assume that each pair of distinct states in a special automaton is tacitly inequated, and modify subsumption accordingly. Now, no information of any kind can be added to a special automaton. The modified subsumption supports this intuition: a first special automaton subsumes a second iff the second subsumes the first. Subsumption reduces to Moore automata isomorphism. To summarise this second intuitive picture: a special automaton represents information that cannot be elaborated. It is as if one knows everything. Such information is total, and is unlike partial information. For example, negation is classical in LTFS+, yet subsumption is monotonic.

There is yet another intuitive picture: the special automata are objects in an SRL interpretation. There is an initial problem in that the collection of special automata may be a proper class. However, predetermining a set from which the special automata draw their states solves this problem. Ensuring there are sufficient states only requires that the cardinality of the predetermined set be at least the cardinality of 𝔚. Let U be the set of all special automata (with states drawn from the predetermined set), let S be the total function from U to 𝔖 such that

S(u) = σ iff u outputs σ at its initial state, and let A be the total function from 𝔄 to the set of partial functions from U to U such that

A(α)(u) is defined iff u transits from its initial state on input α, and

if u transits from its initial state to state q on input α

then A(α)(u) is the q subautomaton of u. Clearly, ⟨U, S, A⟩ is an interpretation, and, by induction on the complexity of δ,

for each δ ∈ 𝔇 and each u ∈ U, u ∈ D_{I}(δ) iff u satisfies δ.

Thus, LTFS+ is an instance of SRL.

Acknowledgements

The research presented in this paper was sponsored by Teilprojekt B4 “Constraints on Grammar for Efficient Generation” of Sonderforschungsbereich 340 “Sprachtheoretische Grundlagen für die Computerlinguistik” of the Deutsche Forschungsgemeinschaft. This paper took a long time to write, and I have accumulated a huge debt of gratitude to a large number of people in writing it. As very partial repayment, I heartily thank Steve Abney, Dale Gerdemann, Thilo Götz, John Griffith, Erhard Hinrichs, Stephan Kepser, Jennifer King, Peter Krause, Detmar Meurers, Frank Morawietz, Drew Moshier, Larry Moss, Tsuneko Nakazawa, Stanley Peters, Carl Pollard, Sabine Reinhard and Ivan Sag for help, encouragement and advice concerning topics that range from finding IPA fonts in LaTEX to revealing the correspondence between morphs and feature structures. I can only humbly apologise to anyone whose help I have carelessly overlooked.

Page 24

References

[Carpenter 1992] Bob Carpenter. The logic of typed feature structures. Cambridge tracts in theoretical computer science, volume 32. Cambridge University Press, Cambridge, England. 1992.

[Carpenter 1993] Bob Carpenter. ALE: the attribute logic engine. User’s guide. Carnegie

Mellon University, Pittsburgh, Pennsylvania, USA. 1993. [Hopcroft and Ullman 1979] John E. Hopcroft and Jeffrey D. Ullman. Introduction to

automata theory, languages, and computation. Addison-Wesley series in computer science. Addison-Wesley Publishing Company, Reading, Massachusetts, USA. 1979.

[Johnson 1988] Mark Johnson. Attribute-value logic and the theory of grammar. CSLI

lecture notes, volume 16. CSLI, Stanford, California, USA. 1988. [Kaplan and Bresnan 1982] Ronald M. Kaplan and Joan Bresnan. “Lexical-functional

grammar: a formal system for grammatical representation.” Pages 173–281 of J. Bresnan (editor). The mental representation of grammatical relations. MIT Press, Cambridge, Massachusetts, USA. 1982

[King 1989] Paul J. King. A logical formalism for head-driven phrase structure grammar.

Doctoral dissertation. Manchester University, Manchester, England. 1989. [Langholm 1989] Tore Langholm. “How to say no with feature structures.” COSMOS

technical report, number 13. University of Oslo, Oslo, Norway. 1989. [Moore 1956] E. F. Moore. “Gedanken experiments on sequential machines.” Pages 129–

153 of Automata studies. Princeton University Press, Princeton, New Jersey, USA. 1956.

[Moshier 1988] M. Andrew Moshier. Extensions to unification grammars for the description of programming languages. Doctoral dissertation. University of Michigan, Ann Arbor, Michigan, USA. 1988.

[Moshier and Rounds 1987] M. Andrew Moshier and William C. Rounds. “A logic for partially specified data structures.” Pages 156–167 of Proceedings of the 14th ACM symposium on principles of programming languages. 1987.

[Nerode 1958] Anil Nerode. “Linear automaton transformations.” Pages 541–544 of Pro-

ceedings of the American Mathematical Society, volume 9. 1958. [Partee et al. 1990] Barbara H. Partee, Alice ter Meulen and Robert E. Wall. Mathemat-

ical methods in linguistics. Studies in linguistics and philosophy, volume 30. Kluwer Academic Publishers, Dordrecht, The Netherlands.

[Pollard 1989] Carl J. Pollard. “Sorts in unification-based grammar and what they mean.”

Unpublished manuscript. 1989. [Pollard and Moshier 1990] Carl J. Pollard and M. Andrew Moshier. “Unifying partial

descriptions of sets.” In P. Hanson (editor). Information, language and cognition. Vancouver studies in cognitive science, volume 1. University of British Columbia Press, Vancouver, British Columbia, Canada. 1990.

[Pollard and Sag 1987] Carl J. Pollard and Ivan A. Sag. Information-based syntax and

semantics. CSLI lecture notes, volume 13. CSLI, Stanford, California, USA. 1987. [Pollard and Sag 1994] Carl J. Pollard and Ivan A. Sag. Head-driven phrase structure

grammar. University of Chicago Press, Chicago, Illinois, USA. 1994. [Rounds and Kaspar 1986] William C. Rounds and Robert T. Kasper. “A complete log-

ical calculus for record structures representing linguistic information.” Pages 89–96 of Proceedings of the 25th annual conference of the Association for Computational Linguistics. 1986.

[Smolka 1988] Gert Smolka. “A feature logic with subsorts.” LILOG technical report, number 33. IBM Deutschland GmbH, Stuttgart, Germany. 1988.