Bericht Nr. 31, 1993

ISSN 0947-6954/93

Arbeitspapiere des Sonderforschungsbereichs 340

Sprachtheoretische Grundlagen für die Computer linguistik

Paul John King and Thilo Götz :

Eliminating the Feature Introduction Condition by Modifying Type Inference

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

Eliminating the Feature Introduction Condition by Modifying Type Inference^{∗}

Paul John King^{†} and Thilo Götz^{‡} Seminar für Sprachwissenschaft Eberhard-Karls-Universität Tübingen Wilhelmstraße 113 72074 Tübingen Germany

7th of May, 1993

Since their inception with Kay’s FUG^{1}, feature structures have found applications in fields as diverse as linguistics, knowledge representation and logic programming. As the applications have become ever more sophisticated, so the feature structures have become correspondingly ever more complicated, to the point that some applications require a formalism to regulate the feature structures. [Carpenter 1992] presents a logical formalism that comprises an algebra of feature structures and a syntax of descriptions. [Carpenter 1992] uses feature structures to model partial information about empirical objects, and interprets descriptions as true or false of feature structures. [Carpenter 1992] then presents a number of extensions to this formalism, and applies some of them to unification-based phrase structure grammars, definite clause programmes, and recursive type constraints. [Carpenter 1992] imposes a condition called feature introduction in order to well define a function called type inference. In our paper, we argue that the feature introduction condition is undesirable. We slightly modify [Carpenter 1992]’s type inference function so that we can well define type inference regardless of the feature introduction condition, and we show that if the feature introduction condition holds then our modified type inference function reduces to [Carpenter 1992]’s original. We structure our paper as follows. Section 1 retrospects, expands upon and illustrates those parts of [Carpenter 1992] relevant to our paper, section 2 criticises the feature introduction condition, and section 3 presents our type inference function. Appendix A contains the standard mathematical definitions and results needed for our paper.

∗The research presented in this paper was sponsored by Teilprojekt B4 “Constraints on Grammar for Efficient Generation” of the Sonderforschungsbereich 340 “Sprachtheoretische Grundlagen für die Computerlinguistik” of the Deutsche Forschungsgemeinschaft. The authors wish to thank Dale Gerdemann and Bob Carpenter for their help and advice. Of course, the authors are responsible for all remaining errors.

†Email: king@sns.neuphilologie.uni-tuebingen.de

‡Email: tg@sns.neuphilologie.uni-tuebingen.de

1Functional unification grammar. See [Kay 1979] and [Kay 1984].

1 Preliminaries

In this section, we do three things. Firstly, we review those parts of [Carpenter 1992] that are germane to our paper. Secondly, some of [Carpenter 1992]’s definitions are insufficiently formal for use in some of our proofs, and we provide more formal alternatives. Finally, we use an informal semantics distilled from those of [Smolka 1988], [King 1989] and [Pollard and Moshier 1990] to illustrate [Carpenter 1992]’s definitions.

1.1 Inheritance Hierarchies

1: Definition (inheritance hierarchy)^{2} An inheritance hierarchy is a pair ⟨Type, ⊑⟩ such that

⟨Type, ⊑⟩ is a finite bounded complete partial order. For facility, we henceforth assume that ⟨Type, ⊑⟩ is an inheritance hierarchy. A type is a symbol that one can interpret as true or false of an object. For example, one can interpret type married as true of each married person, type single as true of each unmarried person, and type person as true of each person. We say that object u is of type t iff t is interpreted as true of u. Thus, Paul John King is of type married since Paul is married to Jennifer, Thilo Götz is of type single since Thilo is (as yet!) unmarried, and both Paul and Thilo are of type person since both Paul and Thilo are people. We call the set of objects of which an interpreted type is true the denotation of that type. Thus, Paul is in the denotation of married, Thilo is in the denotation of single, and both are in the denotation of person. Type is a set of types. A consequence of definition 1 is that there are finitely many types. One often restricts the interpretation of two types so that the denotation of the first contains the denotation of the second. For example, the denotation of person contains the denotation of married since each married person is a person, and the denotation of person contains the denotation of single since each unmarried person is a person. We say that type t_{1} subsumes type t_{2} iff the denotation of t_{1} contains the denotation of t_{2}. Thus, person subsumes both married and single. t_{1} ⊑ t_{2} iff type t_{1} subsumes type t_{2}. Clearly, for each type t,

t subsumes t. Equally clearly, for all types t_{1}, t_{2} and t_{3},

t_{1} subsumes t_{2} and t_{2} subsumes t_{3}

⟹ the denotation of t_{1} contains the denotation of t_{2}, and the denotation of t_{2} contains the denotation of t_{3} ⟹ the denotation of t_{1} contains the denotation of t_{3} ⟹ t_{1} subsumes t_{3}.

Two consequences of definition 1 are that for all types t_{1} and t_{2},

if t_{1} and t_{2} subsume each other then t_{1} = t_{2}, and for all types t_{1} and t_{2},

if t_{1} and t_{2} both subsume some common type

then there is some type t such that for each type t′, t_{1} and t_{2} both subsume t′ iff t subsumes t′.

2Cf. [Carpenter 1992, definition 2.1].

1.2 Appropriateness Specifications

2: Definition (appropriateness specification)^{3} An appropriateness specification over ⟨Type, ⊑⟩ and finite set Feat is a partial function Approp : Feat × Type ⇀ Type^{4} such that for all t_{1} and t_{2} ∈ Type and each f ∈ Feat,

if Approp(f, t_{1}) is defined and t_{1} ⊑ t_{2}

then Approp(f, t_{2}) is defined and Approp(f, t_{1}) ⊑ Approp(f, t_{2}).

For facility, we henceforth assume that Approp is an appropriateness specification over ⟨Type, ⊑⟩ and Feat. A feature is a symbol that one can interpret as a partial function from objects to objects. For example, one can interpret feature spouse as the partial function that maps each person to their husband or wife, if they have one.^{5} Feat is a set of features. A consequence of definition 2 is that there are finitely many features. One often restricts the interpretation of a feature and a type so that the interpretation of the feature is defined on each object of the type. For example, the interpretation of spouse is defined on each object in the denotation of married since each married person has a spouse. We say that type t deserves feature f iff the interpretation of f is defined on each object in the denotation of t. Thus, married deserves spouse. Approp(f, t) is defined iff type t deserves feature f. Clearly, for all types t_{1} and t_{2} and each feature f,

t_{1} subsumes t_{2} and t_{1} deserves f

⟹ the denotation of t_{1} contains the denotation of t_{2}, and

the interpretation of f is defined on each object in the denotation of t_{1} ⟹ the interpretation of f is defined on each object in the denotation of t_{2} ⟹ t_{2} deserves f.

One often further restricts the interpretation of a feature and two types so that the first type deserves the feature and the interpretation of the feature maps each object of the first type to an object of the second type. For example, married deserves spouse and the interpretation of spouse maps each object in the denotation of married to an object in the denotation of married, since each married person has a spouse and that spouse must be a married person too. We say that type t′ is suitable for feature f on type t iff t deserves f and the interpretation of f maps each object in the denotation of t to an object in the denotation of t′. Thus, married is suitable for spouse on married. t′ ⊑ Approp(f, t) iff type t′ is suitable for feature f on type t (sic). Thus, Approp(f, t) is the most specific type (the type with the smallest denotation) that is suitable for f on t. Clearly, for all types t, t_{1} and t_{2} and each feature f,

t_{1} subsumes t_{2} and t is suitable for f on t_{1}

⟹ the denotation of t_{1} contains the denotation of t_{2}, and the interpretation of f maps each object in the denotation of t_{1} to an object in the denotation of t

⟹ the interpretation of f maps each object in the denotation of t_{2} to an

object in the denotation of t ⟹ t is suitable for f on t_{2}.

3Cf. [Carpenter 1992, definition 6.1].

4We write θ : X ⇀ Y for “θ is a partial function from X to Y ”.

5Solely for the purpose of constructing a simple example, we assume all marriages are monogamous!

1 PRELIMINARIES 4 Equally clearly, for all types t, t_{1} and t_{2} and each feature f,

t_{1} subsumes t_{2} and t_{2} is suitable for f on t

⟹ the denotation of t_{1} contains the denotation of t_{2}, and the interpretation of f maps each object in the denotation of t to an object in the denotation of t_{2}

⟹ the interpretation of f maps each object in the denotation of t to an object

in the denotation of t_{1}. ⟹ t_{1} is suitable for f on t.

1.3 Depicting an Inheritance Hierarchy and an Appropriateness Specification

If t is a type and ⟨f_{1}, …, f_{n}⟩ is an ordering of the features t deserves then we usually depict that part of Approp relevent to t as the matrix M_{t}, where

M_{t} = [ \begin{matrix}t \\ f_{1} & Approp(f_{1}, t) \\ ⋮ & ⋮ \\ f_{n} & Approp(f_{n}, t) \end{matrix} ].

We usually depict ⟨Type, ⊑⟩ and Approp as a finite directed graph G, where M_{t} is a node in G iff t is a type, and there is an arc from node M_{t_{1}} to node M_{t_{2}} in G iff t_{1} subsumes t_{2}.

For example, figure 1 depicts our example ⟨Type, ⊑⟩ and Approp.

[figure: \left[{married \atop spouse married}\right]; [ single ]; [ person ]]

Figure 1

1.4 The Feature Introduction Condition

3: Definition (feature introduction function)^{6} A feature introduction function is a total function Intro : Feat → Type^{7} such that for each t ∈ Type and each f ∈ Feat,

Approp(f, t) is defined iff Intro(f) ⊑ t. If Intro is a feature introduction function then Intro(f) is the least specific type (the type with the largest denotation) that deserves f.

6Cf. [Carpenter 1992, definition 6.1].

7We write θ : X → Y for “θ is a total function from X to Y ”.

1 PRELIMINARIES 5 The feature introduction condition of [Carpenter 1992, definition 6.1] deems the existence of a feature introduction function compulsory. However, the purpose of our paper is to show that the feature introduction condition is unnecessary, and we accordingly deem the existence of a feature introduction function optional. We criticise the feature introduction condition in section 2.

1.5 Feature Structures and Subsumption

4: Definition (feature structure)^{8} A feature structure is a quadruple ⟨Q, \overline{q}, θ, δ⟩ such that

Q is a finite set,

\overline{q} ∈ Q,

θ : Q → Type,

δ : Feat × Q ⇀ Q, and

if q ∈ Q then for some n ∈ IN, some q_{0}, …, q_{n} ∈ Q, and some f_{1}, …, f_{n} ∈ Feat

q_{0} = \overline{q},
q_{n} = q, and
for each i < n, δ(f_{i+1}, q_{i}) is defined and δ(f_{i+1}, q_{i}) = q_{i+1}.

We write F for the class of feature structures. If F = ⟨Q, \overline{q}, θ, δ⟩ is a feature structure then we usually depict F as a finite and rooted directed graph with labelled nodes and edges, where

q is a node iff q ∈ Q \overline{q} is the root node type t labels node q iff θ(q) = t, and feature f labels an arc from node q to node q′ iff δ(f, q) = q′.

We indicate the root node with a double circle. For example, if figure 2 depicts ⟨Type, ⊑⟩

[figure: [ \begin{matrix}married \\ spouse & married \\ best-friend & person \end{matrix} ]; \left[{single \atop best-friend person}\right]; \left[{person \atop best-friend person}\right]]

Figure 2

and Approp then figure 3 depicts a feature structure. [Carpenter 1992] applies feature structures to several diverse fields. It is therefore unsurprising that [Carpenter 1992] cannot commit itself to a fixed interpretation of a feature structure. However, it seems fair to say that [Carpenter 1992] uses the modelling convention of [Pollard and Moshier 1990] to interpret a feature structure as information about objects.

8Cf. [Carpenter 1992, definition 3.1].

[figure: \overline{q}; person; q_{1}; married; q_{2}; single; spouse; best-friend; spouse; best-friend]

Figure 3

“the way in which feature structures are used to model partial information about empirical objects is made specific by the so-called modeling convention. According to this convention, the nodes of a feature structure are taken to represent objects, and we assume that every node is labeled with a type symbol which represents the most specific conceptual class to which the object is known to belong. Furthermore, arcs come labeled with feature symbols, and an arc between two nodes indicates that the object represented by the source node has a feature, represented by a feature symbol, which has a value represented by the target node. Structure sharing is taken to model identity. That is, two arcs pointing to the same node indicate that the objects represented by the sources of the arcs have identical values for the feature represented by the arcs.”

[Carpenter 1992, pages 34 and 35]

Thus, the interpretation of our example feature structure is the information that the object is a person, the object has a spouse and a best friend, the object’s spouse is a married person, the object’s best friend is a single person, the object’s spouse has a spouse and a best friend, the object’s spouse’s spouse is the object, and the object’s spouse’s best friend is the object’s best friend.

Suppose Thilo is the best friend of both Paul and Jennifer. Then the interpretation of our example feature structure is true of Paul and Jennifer, but not of Thilo. (Recall that Paul and Jennifer are a married couple, but Thilo is single.) Stealing terminology from our account of types, we call the set of objects of which an interpreted feature structure is true the denotation of that feature structure. Thus, Paul and Jennifer are in the denotation of our example feature structure, but Thilo is not. 5: Definition (feature structure morphism)^{9} A feature structure morphism from feature structure ⟨Q_{1}, \overline{q}_{1}, θ_{1}, δ_{1}⟩ to feature structure 1 PRELIMINARIES 7 ⟨Q_{2}, \overline{q}_{2}, θ_{2}, δ_{2}⟩ is a total function h : Q_{1} → Q_{2} such that

9Cf. [Carpenter 1992, definition 3.4].

h(\overline{q}_{1}) = \overline{q}_{2},

for each q ∈ Q_{1}, θ_{1}(q) ⊑ θ_{2}(h(q)), and for each f ∈ Feat and each q ∈ Q_{1}, if δ_{1}(f, q) is defined

then δ_{2}(f, h(q)) is defined and δ_{2}(f, h(q)) = h(δ_{1}(f, q)).

6: Definition (subsumption)^{9} ⊑ is the binary relation on F such that for all F_{1} and F_{2} ∈ F,

F_{1} ⊑ F_{2} iff there is a feature structure morphism from F_{1} to F_{2}. One can sometimes compare the explicitness of the interpretations of a pair of feature structures. For example, if figure 4 depicts feature structure F and figure 5 depicts feature

[figure: \overline{q}; married; q_{1}; person; q_{2}; person; q_{3}; person; spouse; best-friend; best-friend]

Figure 4

structure F′ then the interpretation of F is less explicit than the interpretation of F′. We say that feature structure F_{1} subsumes feature structure F_{2} iff the interpretation of F_{1} is at most as explicit as the interpretation of F_{2}. Thus, F subsumes F′. F_{1} ⊑ F_{2} iff feature structure F_{1} subsumes feature structure F_{2}. 7: Definition (proper subsumption) ⊏ is the binary relation on F such that for each F_{1} and F_{2} ∈ F,

F_{1} ⊏ F_{2} iff F_{1} ⊑ F_{2} and F_{2} ⋢ F_{1}. If a first feature structure subsumes a second feature structure but the second does not subsume the first then the interpretation of the first is strictly less explicit than the

[figure: \overline{q}; married; q_{1}; married; q_{2}; person; q_{3}; person; spouse; best-friend; best-friend; spouse]

Figure 5

interpretation of the second. We say that feature structure F_{1} properly subsumes feature structure F_{2} iff F_{1} subsumes F_{2} but F_{2} does not subsume F_{1}. Thus, F properly subsumes F′. F_{1} ⊏ F_{2} iff feature structure F_{1} properly subsumes feature structure F_{2}. 8: Proposition^{10} ⟨F, ⊑⟩ is a preorder. Proof Firstly, for each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F,

the identity function on Q is a feature structure morphism from F to F. Thus, for each F ∈ F,

F ⊑ F. … (1) Secondly, for all F_{1}, F_{2} and F_{3} ∈ F

F_{1} ⊑ F_{2} and F_{2} ⊑ F_{3}

⟹ there is a feature structure morphism h_{1} from F_{1} to F_{2}, and there is a feature structure morphism h_{2} from F_{2} to F_{3} ⟹ h_{2} ∘ h_{1} is a feature structure morphism from F_{1} to F_{3}^{11} ⟹ F_{1} ⊑ F_{3}. … (2)

By (1) and (2), 1 PRELIMINARIES 9

10Cf. [Carpenter 1992, lemma 3.5].

11If θ : X ⇀ Y and φ : Y ⇀ Z then φ ∘ θ : X ⇀ Z such that φ ∘ θ(x) is defined iff θ(x) and φ(θ(x))

are defined, and if φ ∘ θ(x) is defined then φ ∘ θ(x) = φ(θ(x)).

⟨F, ⊑⟩ is a preorder. □ ⟨F, ⊑⟩ is not a partial order. For example, if feature structure F is

[figure: q_{1}; person]

and feature structure F′ is

[figure: q_{2}; person]

then

F ⊑ F′ and F′ ⊑ F

but

F ≠ F′. 9: Definition (alphabetic variance)^{12} ∼ is the binary relation on F such that for each F_{1} and F_{2} ∈ F,

F_{1} ∼ F_{2} iff F_{1} ⊑ F_{2} and F_{2} ⊑ F_{1}. If two feature structures mutually subsume each other then the interpretations of the two are equally explicit. [Carpenter 1992] says that feature structures F_{1} and F_{2} are alphabetic variants iff F_{1} and F_{2} mutually subsume each other. Thus, F and F′ are alphabetic variants. F_{1} ∼ F_{2} iff feature structures F_{1} and F_{2} are alphabetic variants. We complete this subsection with two useful lemmata. The first shows that if two feature structures differ only in the types that label their nodes then the only possible feature structure morphism between them is the identity function. The second shows that though subsumption does not partially order the class of feature structures, it does partially order certain finite sets of feature structures. 10: Lemma If h is a feature structure morphism from ⟨Q, \overline{q}, θ_{1}, δ⟩ ∈ F to ⟨Q, \overline{q}, θ_{2}, δ⟩ ∈ F then

for each q ∈ Q, h(q) = q. Proof Suppose

q ∈ Q. Thus, for some n ∈ IN, some q_{0}, …, q_{n} ∈ Q, and some f_{1}, …, f_{n} ∈ Feat,

q_{0} = \overline{q},

q_{n} = q, and
for each i < n, δ(f_{i+1}, q_{i}) is defined and δ(f_{i+1}, q_{i}) = q_{i+1}.

Thus,

h(q_{0}) = h(\overline{q}) = \overline{q} = q_{0},

and, for each i < n, h(q_{i}) = q_{i} ⟹ h(q_{i}) = q_{i}, δ(f_{i+1}, q_{i}) is defined, δ(f_{i+1}, q_{i}) = q_{i+1},

δ(f_{i+1}, h(q_{i})) is defined and δ(f_{i+1}, h(q_{i})) = h(q_{i+1})

12Cf. [Carpenter 1992, definition 3.6].

1 PRELIMINARIES 10 ⟹ δ(f_{i+1}, q_{i}) is defined, δ(f_{i+1}, q_{i}) = q_{i+1} and δ(f_{i+1}, q_{i}) = h(q_{i+1}) ⟹ h(q_{i+1}) = q_{i+1}.

Thus, by induction on i, for each i ≤ n,

h(q_{i}) = q_{i}. Thus,

h(q) = q. □ 11: Lemma If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then

⟨\{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\}, ⊑⟩ is a finite partial order. Proof Firstly,

Q is finite and

Type is finite. Thus,

\{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\} is a finite preorder. … (1) Secondly, for all θ_{1} and θ_{2} : Q → Type,

⟨Q, \overline{q}, θ_{1}, δ⟩ ⊑ ⟨Q, \overline{q}, θ_{2}, δ⟩ ⟹ there is a feature structure homomorphism from ⟨Q, \overline{q}, θ_{1}, δ⟩ to ⟨Q, \overline{q}, θ_{2}, δ⟩ ⟹ for some h : Q → Q,

for each q ∈ Q, h(q) = q, and by lemma 10 for each q ∈ Q, θ_{1}(q) ⊑ θ_{2}(h(q))

⟹ for each q ∈ Q, θ_{1}(q) ⊑ θ_{2}(q). Thus, for all θ_{1} and θ_{2} : Q → Type,

⟨Q, \overline{q}, θ_{1}, δ⟩ ⊑ ⟨Q, \overline{q}, θ_{2}, δ⟩ and ⟨Q, \overline{q}, θ_{2}, δ⟩ ⊑ ⟨Q, \overline{q}, θ_{1}, δ⟩ ⟹ for each q ∈ Q, θ_{1}(q) ⊑ θ_{2}(q) and θ_{2}(q) ⊑ θ_{1}(q) ⟹ for each q ∈ Q, θ_{1}(q) = θ_{2}(q) since ⟨Type, ⊑⟩ is a partial order ⟹ θ_{1} = θ_{2} ⟹ ⟨Q, \overline{q}, θ_{1}, δ⟩ = ⟨Q, \overline{q}, θ_{2}, δ⟩. … (2)

By (1) and (2),

⟨\{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\}, ⊑⟩ is a finite partial order. □

1.6 Well-typed Feature Structures and Type Inference

Suppose figure 6 depicts ⟨Type, ⊑⟩ and Approp, feature structure F_{1} is

[figure: q_{0}; f; q_{1}; f; q_{2}; f; x; y]

feature structure F_{2} is

[figure: \left[{a \atop x b}\right]; \left[{b \atop y d}\right]; \left[{c \atop y d}\right]; [ d ]; \left[{e \atop y f}\right]; [ f ]]

Figure 6

[figure: q_{0}; a; q_{1}; e; q_{2}; f; x; y]

and feature structure F_{3} is

[figure: q_{0}; a; q_{1}; b; q_{2}; d; x; y]

Clearly,

F_{1} ⊏ F_{2} ⊏ F_{3}. However, the interpretations of F_{1}, F_{2} and F_{3} are equally informative. We can use ⟨Type, ⊑⟩ and Approp to infer all the information in the interpretation of F_{2} from the information in the interpretation of F_{1}, and infer all the information in the interpretation of F_{3} from the information in the interpretation of F_{2}. 12: Definition (semi-well-typed feature structure) A semi-well-typed feature feature structure is a feature structure ⟨Q, \overline{q}, θ, δ⟩ such that for each f ∈ Feat and q ∈ Q,

if δ(f, q) is defined then Approp(f, θ(q)) is defined. For example, F_{2} and F_{3} are semi-well-typed feature structures, whereas F_{1} is not. We write STF for the class of semi-well-typed feature structures. 13: Definition (well-typed feature structure)^{13} A well-typed feature feature structure is a feature structure ⟨Q, \overline{q}, θ, δ⟩ such that for each f ∈ Feat and q ∈ Q,

if δ(f, q) is defined

then Approp(f, θ(q)) is defined and Approp(f, θ(q)) ⊑ θ(δ(f, q)). For example, F_{3} is a well-typed feature structure, whereas F_{1} and F_{2} are not. We write TF for the class of well-typed feature structures. The following proposition follows immediately. 14: Proposition TF ⊆ STF.

13Cf. [Carpenter 1992, definition 6.2].

1 PRELIMINARIES 12 The proof of [Carpenter 1992, Theorem 6.3] defines a partial function TypInf as the composition of partial functions TypDom and TypRan, where for each feature structure F,

TypDom(F) is the least explicit semi-well-typed feature structure (up to alphabetic variance) subsumed by F,

and for each semi-well-typed feature structure F′, TypRan(F′) is the least explicit well-typed feature structure (up to alphabetic variance) subsumed by F′.

Thus, by proposition 14, for each feature structure F, TypInf(F) is the least explicit well-typed feature structure (up to alphabetic variance) subsumed by F.

Thus, using our illustrative feature structures, TypDom(F_{1}) ∼ F_{2},

TypRan(F_{2}) ∼ F_{3}, and
TypInf(F_{1}) ∼ F_{3}.

[Carpenter 1992] calls TypInf type inference. [Carpenter 1992] defines TypDom using a feature introduction function. Therefore, [Carpenter 1992] imposes the feature introduction condition to well-define TypDom. However, the purpose of our paper is to show that the feature introduction condition is unnecessary, and we therefore redefine TypDom in section 3. [Carpenter 1992] defines TypRan without using a feature introduction function, and we use this definition. However, to show unequivocally that [Carpenter 1992] defines TypRan without using a feature introduction function, we subdivide the remainder of this subsection into three parts. These subdivisions present [Carpenter 1992]’s definitions of TypDom, TypRan and TypInf respectively, but we assume the feature introduction condition in the first and last subdivisions only.

1.6.1 A Definition of TypDom

Warning! Throughout 1.6.1 we assume the existence of a feature introduction function Intro : Feat → Type. 15: Definition (Φ_{F}) If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then Φ_{F} : Q ⇀ Type such that

Φ_{F} (q) is defined iff θ(q) ⊔ (⨆{Intro(f) | δ(f, q) is defined}) is defined, and if Φ_{F} (q) is defined then Φ_{F} (q) = θ(q) ⊔ (⨆{Intro(f) | δ(f, q) is defined}).

16: Definition (TypDom) TypDom : F ⇀ STF such that for each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F,

TypDom(F) is defined iff for each q ∈ Q, Φ_{F} (q) is defined, and if TypDom(F) is defined then TypDom(F) = ⟨Q, \overline{q}, Φ_{F} , δ⟩.

17: Proposition TypDom is well-defined. Proof TypDom is clearly a partial function with domain F, but it remains to be shown that the range of TypDom is STF.

1 PRELIMINARIES 13 For each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F,

TypDom(F) is defined ⟹ TypDom(F) is defined and for each q ∈ Q, Φ_{F} (q) is defined ⟹ TypDom(F) is defined and for each f ∈ Feat and each q ∈ Q,

δ(f, q) is defined ⟹ Intro(f) ⊑ Φ_{F} (q) ⟹ Approp(f, Φ_{F} (q)) is defined

⟹ TypDom(F) ∈ STF. □ 18: Proposition If F ∈ F and TypDom(F) is defined then

F ⊑ TypDom(F). Proof Suppose

F = ⟨Q, \overline{q}, θ, δ⟩, and h is the identity function on Q.

Thus, for each q ∈ Q,

Φ_{F} (q) is defined and θ(q) ⊑ Φ_{F} (q). Thus,

h is a feature structure morphism from F to TypDom(F). Thus,

F ⊑ TypDom(F). □ 19: Proposition If F ∈ F and F′ ∈ STF then

F ⊑ F′ iff TypDom(F) is defined and TypDom(F) ⊑ F′. Proof Part 1. From left to right. Suppose

F = ⟨Q, \overline{q}, θ, δ⟩, F′ = ⟨Q′, \overline{q}′, θ′, δ′⟩, and h is a feature structure morphism from F to F′.

Thus, for each q ∈ Q,

θ(q) ⊑ θ′(h(q)), and for each f ∈ Feat and each q ∈ Q,

δ(f, q) is defined ⟹ δ′(f, h(q)) is defined ⟹ Approp(f, θ′(h(q))) is defined since F′ ∈ STF ⟹ Intro(f) ⊑ θ′(h(q)).

Thus, for each q ∈ Q, Φ_{F} (q) is defined and Φ_{F} (q) ⊑ θ′(h(q)).

1 PRELIMINARIES 14 Thus,

TypDom(F) is defined, and

h is a feature structure morphism from TypDom(F) to F′. Thus,

TypDom(F) is defined and TypDom(F) ⊑ F′. Part 2. From right to left.

TypDom(F) is defined and TypDom(F) ⊑ F′

⟹ F ⊑ TypDom(F) and TypDom(F) ⊑ F′ by proposition 18 ⟹ F ⊑ F′.

□

1.6.2 A Definition of TypRan

20: Definition (π_{F}) If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ STF then π_{F} : Q → Pow(Type) such that

π_{F} (q) = {Approp(f, θ(q′)) | δ(f, q′) is defined and δ(f, q′) = q}. 21: Definition (Π_{F}) If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ STF then Π_{F} : Q ⇀ Type such that

Π_{F} (q) is defined iff θ(q) ⊔ (⨆ π_{F} (q)) is defined, and if Π_{F} (q) is defined then Π_{F} (q) = θ(q) ⊔ (⨆ π_{F} (q)).

22: Definition (TypProg) TypProg : STF ⇀ STF such that for each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ STF,

TypProg(F) is defined iff for each q ∈ Q, Π_{F} (q) is defined, and if TypProg(F) is defined then TypProg(F) = ⟨Q, \overline{q}, Π_{F} , δ⟩.

23: Proposition TypProg is well-defined. Proof TypProg is clearly a partial function with domain STF, but it remains to be shown that the range of TypProg is STF. For each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ STF,

TypProg(F) is defined

⟹ TypProg(F) is defined and for each q ∈ Q, Π_{F} (q) is defined ⟹ TypProg(F) is defined and for each f ∈ Feat and each q ∈ Q,

δ(f, q) is defined

⟹ Approp(f, θ(q)) is defined since F ∈ STF ⟹ Approp(f, θ(q)) is defined and θ(q) ⊑ Π_{F} (q) ⟹ Approp(f, Π_{F} (q)) is defined

⟹ TypProg(F) ∈ STF. □ 24: Proposition If F ∈ STF and TypProg(F) is defined then

F ⊑ TypProg(F).

1 PRELIMINARIES 15 Proof Suppose

F = ⟨Q, \overline{q}, θ, δ⟩, and h is the identity function on Q.

Thus, for each q ∈ Q,

Π_{F} (q) is defined and θ(q) ⊑ Π_{F} (q). Thus,

h is a feature structure morphism form F to TypProg(F). Thus,

F ⊑ TypProg(F). □ 25: Proposition If F ∈ STF and F′ ∈ TF then

F ⊑ F′ iff TypProg(F) is defined and TypProg(F) ⊑ F′. Proof Part 1. From left to right. Suppose

F = ⟨Q, \overline{q}, θ, δ⟩, F′ = ⟨Q′, \overline{q}′, θ′, δ′⟩, and h is a feature structure morphism from F to F′.

Thus, for each q ∈ Q,

θ(q) ⊑ θ′(h(q)), and for each f ∈ Feat and all q and q′ ∈ Q,

δ(f, q′) is defined and δ(f, q′) = q ⟹ Approp(f, θ(q′)) is defined, since F′ ∈ STF

δ′(f, h(q′)) is defined, and

δ′(f, h(q′)) = h(q)

⟹ Approp(f, θ(q′)) is defined, Approp(f, θ′(h(q′))) is defined, since F′ ∈ TF

Approp(f, θ(q′)) ⊑ Approp(f, θ′(h(q′))), and

Approp(f, θ′(h(q′))) ⊑ θ′(h(q)) since F′ ∈ TF ⟹ Approp(f, θ(q′)) is defined and Approp(f, θ(q′)) ⊑ θ′(h(q))

Thus, for each q ∈ Q,

Π_{F} (q) is defined and Π_{F} (q) ⊑ θ′(h(q′)). Thus,

TypProg(F) is defined, and h is a feature structure morphism from TypProg(F) to F′.

Thus,

TypProg(F) is defined and TypProg(F) ⊑ F′. Part 2. From right to left.

TypProg(F) is defined and TypProg(F) ⊑ F′ ⟹ F ⊑ TypProg(F) and TypProg(F) ⊑ F′ by proposition 24 ⟹ F ⊑ F′.

□ The range of TypProg is not TF. Suppose F is a semi-well-typed feature structure. Suppose feature f labels an arc from node q_{1} to node q_{2}, type t_{1} labels node q_{1} and type t_{2} labels node q_{2} in F. Suppose TypProg(F) is defined. Feature f still labels an arc from node q_{1} to node q_{2} in TypProg(F). Suppose type t′_{1} labels node q_{1} and type t′_{2} labels node q_{2} in TypProg(F). The definition of TypProg ensures that type Approp(f, t_{1}) subsumes type t′_{2}, but it does not ensure that type Approp(f, t′_{1}) subsumes type t′_{2}. Loosely speaking, TypProg ‘improves’ a feature structure by labelling each target node with a type at least as specific as the most specific type suitable for the feature labelling each arc entering that node on the type labelling the source node of that arc in the original feature structure. However, a source node can itself be a target node, and by relabelling the target node of a first arc, TypProg may relabel the source node of a second arc. Thus, TypProg may not label each node with a type at least as specific as the most specific type suitable for the feature labelling each arc entering that node on the type labelling the source node of that arc in the improved feature structure. For example, recall the semi-well-typed feature structure F_{2} of page 10. F_{2} is

[figure: q_{0}; a; q_{1}; e; q_{2}; f; x; y]

and TypProg(F_{2}) is

[figure: q_{0}; a; q_{1}; b; q_{2}; f; x; y]

TypProg(F_{2}) is not well-typed. Type e labels node q_{1} in F_{2}, and TypProg certainly ensures that type Approp(y, e) subsumes type f. However, type b labels node q_{1} in TypProg(F_{2}), and TypProg does not ensure that type Approp(y, b) subsumes type f. If F is a semi-well-typed feature structure then we apply TypProg iteratively to F until a fixed point is reached in order to obtain TypRan(F). 26: Lemma If F ∈ STF, TypProg(F) is defined and TypProg(F) = F then

F ∈ TF. Proof For each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ STF,

TypProg(F) is defined and TypProg(F) = F

⟹ for each q ∈ Q, Π_{F} (q) is defined and Π_{F} (q) = θ(q)

⟹ for each f ∈ Feat and each q ∈ Q, δ(f, q) is defined ⟹ Approp(f, θ(q)) is defined and δ(f, q) is defined since F ∈ STF ⟹ Approp(f, θ(q)) is defined and Approp(f, θ(q)) ∈ π_{F} (δ(f, q)) ⟹ Approp(f, θ(q)) is defined, and Approp(f, θ(q)) ⊑ Π_{F} (δ(f, q))

⟹ Approp(f, θ(q)) is defined and Approp(f, θ(q)) ⊑ θ(δ(f, q))

1 PRELIMINARIES 17

⟹ F ∈ TF. □ 27: Lemma If F ∈ STF and for each n ∈ IN, TypProg^{n}(F) is defined^{14} then

⟨{TypProg^{n}(F) | n ∈ IN}, ⊑⟩ has a unique maximal member. Proof By lemmata 11 and 69,

⟨{TypProg^{n}(F) | n ∈ IN}, ⊑⟩ is an upward Noetherian partial order, and by proposition 24,

for each n ∈ IN, TypProg^{n}(F) ⊑ TypProg^{n+1}(F). Thus, by lemma 70,

⟨{TypProg^{n}(F) | n ∈ IN}, ⊑⟩ has a unique maximal member. □ 28: Definition (TypRan) TypRan : STF ⇀ TF such that

TypRan(F) is defined iff for each n ∈ IN, TypProg^{n}(F) is defined, and

if TypRan(F) is defined

then TypRan(F) is the maximal member of ⟨{TypProg^{n}(F) | n ∈ IN}, ⊑⟩. 29: Proposition TypRan is well-defined. Proof By lemma 27, TypRan is a partial function with domain STF, but it remains to be shown that the range of TypRan is TF. For each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ STF,

TypRan(F) is defined ⟹ TypRan(F) is defined, TypRan(F) ∈ STF, TypProg(TypRan(F)) is defined TypRan(F) ⊑ TypProg(TypRan(F)), and by proposition 24 TypProg(TypRan(F)) ⊑ TypRan(F)

since TypRan(F) is the maximal member of ⟨{TypProg^{n}(F) | n ∈ IN}, ⊑⟩

⟹ TypRan(F) is defined, TypRan(F) ∈ STF, TypProg(TypRan(F)) is defined, and TypProg(TypRan(F)) = TypRan(F) by lemma 11 ⟹ TypRan(F) ∈ TF. by lemma 26

□ 30: Proposition If F ∈ STF and TypRan(F) is defined then

F ⊑ TypRan(F).

14If θ : X ⇀ X then θ^{0} is the identity function on X, and θ^{n+1} is θ ∘ θ^{n}.

1 PRELIMINARIES 18 Proof Proposition 30 follows immediately from proposition 24 □ 31: Proposition If F ∈ STF and F′ ∈ TF then

F ⊑ F′ iff TypRan(F) is defined and TypRan(F) ⊑ F′. Proof

F ⊑ F′

⟹ for each n ∈ IN, TypProg^{n}(F) is defined and TypProg^{n}(F) ⊑ F′

by proposition 25

⟹ TypRan(F) is defined and TypRan(F) ⊑ F′ and

TypRan(F) is defined and TypRan(F) ⊑ F′

⟹ F ⊑ TypRan(F) and TypRan(F) ⊑ F′ by proposition 30 ⟹ F ⊑ F′.

□

1.6.3 A Definition of TypInf

Warning! Throughout 1.6.3 we assume the existence of a feature introduction function Intro : Feat → Type. 32: Definition (TypInf) TypInf : F ⇀ TF such that

TypInf = TypRan ∘ TypDom. 33: Proposition If F ∈ F and TypInf(F) is defined then

F ⊑ TypInf(F). Proof For each F ∈ F,

TypInf(F) is defined

⟹ TypRan ∘ TypDom(F) is defined, and TypInf(F) = TypRan ∘ TypDom(F)

⟹ TypDom(F) is defined, TypRan(TypDom(F)) is defined, and TypInf(F) = TypRan(TypDom(F))

⟹ F ⊑ TypDom(F), by proposition 18 TypDom(F) ⊑ TypRan(TypDom(F)), and by proposition 30 TypInf(F) = TypRan(TypDom(F))

⟹ F ⊑ TypInf(F). □ 34: Proposition If F ∈ F and F′ ∈ TF then

F ⊑ F′ iff TypInf(F) is defined and TypInf(F) ⊑ F′.

Proof F ⊑ F′ ⟺ TypDom(F) is defined and TypDom(F) ⊑ F′ by propositions 14 and 19 ⟺ TypRan(TypDom(F)) is defined and TypRan(TypDom(F)) ⊑ F′

by proposition 31

⟺ TypRan ∘ TypDom(F) is defined and TypRan ∘ TypDom(F) ⊑ F′

⟺ TypInf(F) is defined and TypInf(F) ⊑ F′. □

2 Criticism

Subsection 1.4 said [Carpenter 1992] imposes a feature introduction condition that obligates the existence of a feature introduction function Intro : Feat → Type such that for each feature f, Intro(f) is the least specific type that deserves f. [Carpenter 1992] claims that the feature introduction condition is imposed in order to

“ensure that type inference … is well defined”

[Carpenter 1992, page 86]

and subsection 1.6 showed that [Carpenter 1992]’s definition of type inference requires the existence of a feature introduction function. However, to the best of our knowledge, only [Carpenter 1992] imposes the feature introduction condition, and several popular typed unification formalisms do not meet it. For example, HPSG^{15} is a grammar with an underlying typed unification formalism. HPSG uses arbitrary length lists of objects to account for certain aspects of natural language, and the underlying formalism uses the “first/rest” method of the programming languages LISP and Prolog to represent such lists. The “first/rest” method introduces three types, list, empty-list and proper-list, and two features, first and rest. The denotation of list is the collection of all lists, the denotation of empty-list is the collection of all lists with no members, and the denotation of proper-list is the collection of all lists with some members. list and empty-list deserve no features, but proper-list deserves features first and rest. The interpretation of first maps proper list l to the first member of l, and the interpretation of rest maps proper list l to l with its first member removed. Figure 7 depicts this inheritance hierarchy and appropriateness specification. However, rather than lists of objects of arbitrary type, HPSG uses different kinds of list, where each kind of list comprises objects of a specific type. Thus, for each type τ, HPSG incorporates the fragment in figure 8 into the inheritance hierarchy and appropriateness specification, where the denotation of list-of-τ is the collection of all lists whose members are of type τ, and the denotation of proper-list-of-τ is the collection of all non empty lists whose members are of type τ. HPSG does not generate list types from list types: if τ is empty-list, list-of-τ′ or proper-list-of-τ′ then HPSG does not generate list-of-τ or proper-list-of-τ. Thus, the inheritance hierarchy remains finite. If figure 9 depicts HPSG’s unexpanded inheritance hierarchy and appropriateness specification then figure 10 depicts HPSG’s expanded inheritance hierarchy and appropriateness specification.^{16} Notice that there is no Intro(first) or Intro(rest). HPSG’s underlying

15Head-driven phrase structure grammar. See [Pollard and Sag 1987] and [Pollard and Sag 1993].

16This is an extreme simplification of HPSG’s inheritance hierarchy and appropriateness specification, but it is sufficient to illustrate our point. See [Pollard and Sag 1993] for HPSG’s true inheritance

[figure: [ empty-list ]; [ \begin{matrix}proper-list \\ first & ⊥ \\ rest & list \end{matrix} ]; [ list ]; [ ⊥ ]]

Figure 7

[figure: [ empty-list ]; [ \begin{matrix}proper-list-of-τ \\ first & τ \\ rest & list \end{matrix} ]; [ list-of-τ ]; [ ⊥ ]]

Figure 8

[figure: [ sign ]; [ synsem ]; [ ⊥ ]]

Figure 9

formalism does not meet the feature introduction condition. There are two obvious ways to amend HPSG’s underlying formalism to meet the feature introduction condition. The first amends HPSG’s inheritance hierarchy. The second amends HPSG’s appropriateness specification.

hierarchy and appropriateness specification.

[figure: [ empty-list ]; [ \begin{matrix}proper-list-of-sign \\ first & sign \\ rest & list-of-sign \end{matrix} ]; [ \begin{matrix}proper-list-of-⊥ \\ first & ⊥ \\ rest & list-of-⊥ \end{matrix} ]; [ \begin{matrix}proper-list-of-synsem \\ first & synsem \\ rest & list-of-synsem \end{matrix} ]; [ list-of-sign ]; [ list-of-⊥ ]; [ list-of-synsem ]; [ sign ]; [ ⊥ ]; [ synsem ]]

Figure 10

Amend HPSG’s inheritance hierarchy to let

proper-list-of-⊥ ⊑ proper-list-of-sign and

proper-list-of-⊥ ⊑ proper-list-of-synsem To maintain an appropriateness specification, one must also amend HPSG’s inheritance hierarchy to let

list-of-⊥ ⊑ list-of-sign and

list-of-⊥ ⊑ list-of-synsem. Figure 11 depicts HPSG’s ammended inheritance hierarchy and appropriateness specifica-

[figure: [ empty-list ]; [ \begin{matrix}proper-list-of-sign \\ first & sign \\ rest & list-of-sign \end{matrix} ]; [ \begin{matrix}proper-list-of-⊥ \\ first & ⊥ \\ rest & list-of-⊥ \end{matrix} ]; [ \begin{matrix}proper-list-of-synsem \\ first & synsem \\ rest & list-of-synsem \end{matrix} ]; [ list-of-sign ]; [ list-of-⊥ ]; [ list-of-synsem ]; [ sign ]; [ ⊥ ]; [ synsem ]]

Figure 11

tion. Clearly, HPSG’s underlying formalism now meets the feature introduction condition. However, this amendment has unforseen consequences. For example, if figure 12 depicts feature structure F then F is now well-typed, whereas formerly it was not. Alternatively, ammend HPSG’s set of features and appropriateness specification so that for each τ ∈ {⊥, sign, synsem}, proper-list-of-τ deserve features first_{τ} and rest_{τ} instead of first and rest. Figure 13 depicts HPSG’s reammended inheritance hierarchy and appropriateness specification. Again, HPSG’s underlying formalism now meets the feature

[figure: \overline{q}; proper-list-of-⊥; q_{1}; sign; q_{2}; proper-list-of-synsem; first; rest]

Figure 12

[figure: [ empty-list ]; [ \begin{matrix}proper-list-of-sign \\ first_{sign} & sign \\ rest_{sign} & list-of-sign \end{matrix} ]; [ \begin{matrix}proper-list-of-⊥ \\ first_{⊥} & ⊥ \\ rest_{⊥} & list-of-⊥ \end{matrix} ]; [ \begin{matrix}proper-list-of-synsem \\ first_{synsem} & synsem \\ rest_{synsem} & list-of-synsem \end{matrix} ]; [ list-of-sign ]; [ list-of-⊥ ]; [ list-of-synsem ]; [ sign ]; [ ⊥ ]; [ synsem ]]

Figure 13

introduction specification. Further, the second amendment avoids the pitfalls of the first amendment concerning well-typed feature structures. However, the second amendment obliges the authors of an HPSG inheritance hierarchy and appropriateness specification to differentiate features they might otherwise not want to differentiate. To summarize, [Carpenter 1992] imposes the feature introduction condition to enable type inference. However, the condition at worst interferes with well-typedness, and at best unnaturally complicates an inheritance hierarchy and appropriateness specification. Clearly, it would be better if one could eliminate the feature introduction condition, and section 3 shows that one can eliminate the feature introduction condition.

3 Modification

Suppose figure 14 depicts ⟨Type, ⊑⟩ and Approp. There is no least specific type that deserves feature x. Thus, the feature introduction condition does not hold, and TypDom is undefined. Suppose feature structure F_{a} is

[figure: \left[{a \atop x d}\right]; \left[{b \atop x d}\right]; \left[{c \atop x d}\right]; [ d ]]

Figure 14

[figure: q_{0}; a; q_{1}; d; x]

feature structure F_{b} is

[figure: q_{0}; b; q_{1}; d; x]

feature structure F_{c}

[figure: q_{0}; c; q_{1}; d; x]

and feature structure F_{d} is

[figure: q_{0}; d; q_{1}; d; x]

F_{d} is not a semi-well-typed feature structure, but it subsumes semi-well-typed feature structures F_{a}, F_{b} and F_{c}. However, there is no least explicit semi-well-typed feature structure subsumed by F_{d}. That is, there is no semi-well-typed feature structure F such that for each semi-well-typed feature structure F′,

F_{d} ⊑ F′ iff F ⊑ F′. [Carpenter 1992] invokes the feature introduction condition expressly to avoid this situation. However, there is a finite set of least explicit semi-well-typed feature structures subsumed by F. That is, there is a set P of semi-well-typed feature structures such that

⟨P, ⊑⟩ is a finite and pairwise incomparable preorder, and for each semi-well-typed feature structure F′, F_{d} ⊑ F′ iff for some F ∈ P, F ⊑ F′.

Simply, P = {F_{a}, F_{c}}.

3 MODIFICATION 24 This section modifies TypDom and TypInf to give functions TypDom^{∗} and TypInf^{∗} such that TypDom^{∗}(F) is the finite set of least explicit semi-well-typed feature structures and TypInf^{∗}(F) is the finite set of least explicit well-typed feature structures subsumed by feature structure F. Both TypDom^{∗} and TypInf^{∗} are well defined regardless of the feature introduction condition, but if the feature introduction condition does hold then TypInf^{∗} reduces to TypInf in that for each feature structure F,

TypInf^{∗}(F) = \{ \begin{matrix}\{TypInf(F)\} & if TypInf(F) is defined \\ ∅ & if TypInf(F) is undefined. \end{matrix}

3.1 Preliminary Definitions

35: Definition (Pow^{∗}) If ⟨P, ⪯⟩ is a preorder then

Pow^{∗}(⟨P, ⪯⟩) = {S ⊆ P | ⟨S, ⪯⟩ is finite and pairwise incomparable}. For convenience, we write Pow^{∗}(STF) for Pow^{∗}(⟨STF, ⊑⟩), and we write Pow^{∗}(TF) for Pow^{∗}(⟨TF, ⊑⟩).^{17} 36: Definition (Min) If ⟨P, ⪯⟩ is a preorder then

Min(⟨P, ⪯⟩) = {p ∈ P | p is a minimal member of ⟨P, ⪯⟩}. For convenience, if P ⊆ Type or P ⊆ F then we write Min(P) for Min(⟨P, ⊑⟩). 37: Lemma If ⟨P, ⪯⟩ is a partial order then

Min(⟨P, ⪯⟩) is pairwise incomparable. Proof For each p_{1} and p_{2} ∈ Min(⟨P, ⪯⟩),

p_{1} ⪯ p_{2}

⟹ p_{1} ⪯ p_{2}, p_{1} ∈ P and p_{2} is a minimal member of ⟨P, ⪯⟩
⟹ p_{1} ⪯ p_{2} and p_{2} ⪯ p_{1}

⟹ p_{1} = p_{2}. since ⟨P, ⪯⟩ is a partial order Thus,

Min(⟨P, ⪯⟩) is pairwise incomparable. □ 38: Lemma If ⟨P, ⪯⟩ is a downward Noetherian preorder then for each p ∈ P,

for some p′ ∈ Min(⟨P, ⪯⟩), p′ ⪯ p. Proof For each p ∈ P, suppose

S_{p} = {s ∈ P | s ⪯ p}.

17Strictly, we may not be able to apply Pow^{∗} to ⟨STF, ⊑⟩ or ⟨TF, ⊑⟩. If ⟨Q, \overline{q}, θ, δ⟩ is a feature structure then Q is a finite set. The members of Q are taken from an unspecified class C. C may not be a set. Thus, F, STF and TF may not be sets. Thus, ⟨F, ⊑⟩, ⟨STF, ⊑⟩ and ⟨TF, ⊑⟩ may not be preorders.

However, we have two solutions to this problem. Either redefine a preorder as a pair ⟨P, ⪯⟩ such that P is a class, or insist that C be a set.

3 MODIFICATION 25 Thus,

p ∈ P

⟹ S_{p} ⊆ P and S_{p} ≠ ∅

⟹ ⟨S_{p}, ⪯⟩ has a minimal member. since ⟨P, ⪯⟩ is downward Noetherian For each p ∈ P, suppose

p̃ is a minimal member of ⟨S_{p}, ⪯⟩. Firstly, for each p ∈ P,

p̃ ⪯ p. … (1) Secondly, for each p and p′ ∈ P,

p′ ⪯ p̃

⟹ p′ ⪯ p̃ and p̃ ⪯ p
⟹ p′ ⪯ p and p′ ⪯ p̃
⟹ p′ ∈ S_{p} and p′ ⪯ p̃

⟹ p̃ ⪯ p′. since p̃ is a minimal member of ⟨S_{p}, ⪯⟩ Thus, for each p ∈ P,

p̃ ∈ Min(⟨P, ⪯⟩). … (2) By (1) and (2), for each p ∈ P,

for some p′ ∈ Min(⟨P, ⪯⟩), p′ ⪯ p. □ 39: Definition (Choice) If X and Y are sets and θ : X → Pow(Y ) is a total function then

Choice(θ) = {φ : X → Y | for each x ∈ X, φ(x) ∈ θ(x)}.

3.2 A Modification of TypDom

40: Definition (ψ_{F}) If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then ψ_{F} : Q → Pow(Type) such that for each t ∈ Type and each q ∈ Q,

t ∈ ψ_{F} (q)

iff θ(q) ⊑ t and for each f ∈ Feat,

if δ(f, q) is defined then Approp(f, t) is defined.

41: Definition (Ψ_{F}) If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then Ψ_{F} : Q → Pow(Type) such that

Ψ_{F} (q) = Min(ψ_{F} (q)). 42: Lemma If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then for each q ∈ Q,

⟨Ψ_{F} (q), ⊑⟩ is pairwise incomparable. Proof For each q ∈ Q,

⟨ψ_{F} (q), ⊑⟩ is a partial order.

3 MODIFICATION 26 Thus, by lemma 37, for each q ∈ Q,

⟨Ψ_{F} (q), ⊑⟩ is pairwise incomparable. □ 43: Lemma If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F and q ∈ Q then for each t ∈ ψ_{F} (q),

for some t′ ∈ Ψ_{F} (q), t′ ⊑ t. Proof By lemma 69, if q ∈ Q then

⟨ψ_{F} (q), ⊑⟩ is a downward Noetherian preorder. Thus, by lemma 38, if q ∈ Q then for each t ∈ ψ_{F} (q),

for some t′ ∈ Ψ_{F} (q), t′ ⊑ t. □ 44: Definition (TypDom^{∗}) TypDom^{∗} : F → Pow^{∗}(STF) such that for each F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F,

TypDom^{∗}(F) = \{⟨Q, \overline{q}, θ′, δ⟩ | θ′ ∈ Choice(Ψ_{F})\}. 45: Proposition TypDom^{∗} is well defined. Proof TypDom^{∗} is clearly a total function with domain F, but it remains to be shown that the range of TypDom^{∗} is Pow^{∗}(STF). Firstly,

F ∈ F and F′ ∈ TypDom^{∗}(F)

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ′ ∈ Choice(Ψ_{F}), F′ = ⟨Q, \overline{q}, θ′, δ⟩
⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ′ : Q → Type,
F′ = ⟨Q, \overline{q}, θ′, δ⟩ and for each f ∈ Feat and each q ∈ Q,

δ(f, q) is defined

⟹ for each t ∈ ψ_{F} (q), Approp(f, t) is defined ⟹ for each t ∈ Ψ_{F} (q), Approp(f, t) is defined ⟹ Approp(f, θ′(q)) is defined.

⟹ F′ ∈ STF. Thus, for each F ∈ F,

TypDom^{∗}(F) ⊆ STF. … (1) Secondly,

F ∈ F

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for each q ∈ Q, Ψ_{F} (q) is finite since Type is finite ⟹ Choice(Ψ_{F}) is finite since Q is finite ⟹ TypDom^{∗}(F) is finite.

Thus, for each F ∈ F,

⟨TypDom^{∗}(F), ⊑⟩ is finite. … (2) Thirdly,

F ∈ F, F_{1} ∈ TypDom^{∗}(F), F_{2} ∈ TypDom^{∗} and F_{1} ⊑ F_{2} 3 MODIFICATION 27

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ_{1} and θ_{2} ∈ Choice(Ψ_{F}), F_{1} = ⟨Q, \overline{q}, θ_{1}, δ⟩,

F_{2} = ⟨Q, \overline{q}, θ_{2}, δ⟩, and
for some h : Q → Q,

h is a feature structure morphism from F_{1} to F_{2}

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ_{1} and θ_{2} ∈ Choice(Ψ_{F}), F_{1} = ⟨Q, \overline{q}, θ_{1}, δ⟩,

F_{2} = ⟨Q, \overline{q}, θ_{2}, δ⟩, and

for each q ∈ Q, θ_{1}(q) ⊑ θ_{2}(q) by lemma 10

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ_{1} and θ_{2} : Q → Type, F_{1} = ⟨Q, \overline{q}, θ_{1}, δ⟩,

F_{2} = ⟨Q, \overline{q}, θ_{2}, δ⟩, and
for each q ∈ Q,
θ_{1}(q) ⊑ θ_{2}(q), θ_{1}(q) ∈ Ψ_{F} (q) and θ_{2}(q) ∈ Ψ_{F} (q)

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ_{1} and θ_{2} : Q → Type, F_{1} = ⟨Q, \overline{q}, θ_{1}, δ⟩,

F_{2} = ⟨Q, \overline{q}, θ_{2}, δ⟩, and

for each q ∈ Q, θ_{1}(q) = θ_{2}(q) by lemma 42

⟹ F_{1} = F_{2}. Thus, for each F ∈ F,

⟨TypDom^{∗}(F), ⊑⟩ is pairwise incomparable. … (3) By (1), (2) and (3), for each F ∈ F,

TypDom^{∗}(F) ∈ Pow^{∗}(STF). □ 46: Proposition If F ∈ F and F′ ∈ TypDom^{∗}(F) then

F ⊑ F′. Proof

F ∈ F and F′ ∈ TypDom^{∗}(F) ⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ′ ∈ Choice(Ψ_{F}), F′ = ⟨Q, \overline{q}, θ′, δ⟩ ⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ′ : Q → Type,

F′ = ⟨Q, \overline{q}, θ′, δ⟩ and for each q ∈ Q, θ′(q) ∈ Ψ_{F} (q)

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and for some θ′ : Q → Type,

F′ = ⟨Q, \overline{q}, θ′, δ⟩ and for each q ∈ Q, θ(q) ⊑ θ′(q)

⟹ F = ⟨Q, \overline{q}, θ, δ⟩, and

the identity function on Q is a feature structure morphism from F to F′ ⟹ F ⊑ F′.

□ 47: Proposition If F ∈ F and F′′ ∈ STF then

F ⊑ F′′ iff for some F′ ∈ TypDom^{∗}(F), F′ ⊑ F′′.

3 MODIFICATION 28 Proof Part 1. From left to right. Suppose

F = ⟨Q, \overline{q}, θ, δ⟩,

F′′ = ⟨Q′′, \overline{q}′′, θ′′, δ′′⟩, and

h is a feature structure morphism from F to F′. Thus, for each q ∈ Q

θ(q) ⊑ θ′′(h(q)), and for each f ∈ Feat and each q ∈ Q,

δ(f, q) is defined

⟹ δ′′(f, h(q)) is defined

⟹ Approp(f, θ′′(h(q))) is defined since F′′ ∈ STF Thus, for each q ∈ Q,

θ′′(h(q)) ∈ ψ_{F} (q). Thus, for each q ∈ Q,

for some t ∈ Ψ_{F} (q), t ⊑ θ′′(h(q)). by lemma 43 Thus, for some θ′ ∈ Choice(Ψ_{F}),

for each q ∈ Q, θ′(q) ⊑ θ′′(h(q)). Thus, for some θ′ ∈ Choice(Ψ_{F}),

h is a feature structure morphism from ⟨Q, \overline{q}, θ′, δ⟩ to F′′. Thus, for some F′ ∈ TypDom^{∗}(F),

h is a feature structure morphism from F′ to F′′. Thus, for some F′ ∈ TypDom^{∗}(F),

F′ ⊑ F′′. Part 2. From right to left.

for some F′ ∈ TypDom^{∗}(F), F′ ⊑ F′′

⟹ for some F′ ∈ TypDom^{∗}(F), F ⊑ F′ and F′ ⊑ F′′ by proposition 46

⟹ F ⊑ F′′.

□

3.3 A Modification of TypInf

48: Definition (Θ) Θ : F → Pow(F) such that

Θ(F) = {TypRan(F′) | F′ ∈ TypDom^{∗}(F) and TypRan(F′) is defined}. 49: Definition (TypInf^{∗}) Let TypInf^{∗} : F → Pow^{∗}(TF) by

TypInf^{∗}(F) = Min(Θ(F)). 50: Proposition TypInf^{∗} is well defined.

3 MODIFICATION 29 Proof TypInf^{∗} is clearly a total function with domain F, but it remains to be shown that the range of TypInf^{∗} is Pow^{∗}(TF). Firstly,

F ∈ F and F′′ ∈ TypInf^{∗}(F) ⟹ F ∈ F and F′′ ∈ Θ(F) ⟹ F ∈ F and for some F′ ∈ TypDom^{∗}(F),

TypRan(F′) is defined and F′′ = TypRan(F′)

⟹ for some F′ ∈ STF, TypRan(F′) is defined and F′′ = TypRan(F′) ⟹ F′′ ∈ TF.

Thus, for each F ∈ F,

TypInf^{∗}(F) ⊆ TF. … (1) Secondly,

F ∈ F ⟹ TypDom^{∗}(F) is finite ⟹ Θ(F) is finite ⟹ TypInf^{∗}(F) is finite.

Thus, for each F ∈ F,

⟨TypInf^{∗}(F), ⊑⟩ is finite. … (2) Thirdly,

F ∈ F ⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and TypDom^{∗}(F) ⊆ \{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\} ⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and Θ(F) ⊆ \{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\} ⟹ ⟨Θ(F), ⊑⟩ is a partial order by lemma 11 ⟹ ⟨TypInf^{∗}(F), ⊑⟩ is pairwise incomparable. by lemma 37

Thus, for each F ∈ F,

⟨TypInf^{∗}(F), ⊑⟩ is pairwise incomparable. … (3) By (1), (2) and (3), for each F ∈ F,

TypInf^{∗}(F) ∈ Pow^{∗}(TF). □ If F is a feature structure then ⟨Θ(F), ⊑⟩ need not be pairwise incomparable. For example, suppose figure 15 depicts ⟨Type, ⊑⟩ and Approp, and feature structure F is

[figure: q_{0}; d; q_{1}; e; q_{2}; f; x; y]

Then TypDom^{∗}(F) is

[figure: q_{0}; d; q_{1}; b; q_{2}; f; x; y]

[figure: q_{0}; d; q_{1}; c; q_{2}; f; x; y]

[figure: \left[{a \atop y f}\right]; \left[{b \atop y f}\right]; \left[{c \atop y f}\right]; \left[{d \atop x b}\right]; [ e ]; [ f ]]

Figure 15

and Θ(F) is

[figure: q_{0}; d; q_{1}; b; q_{2}; f; x; y]

[figure: q_{0}; d; q_{1}; a; q_{2}; f; x; y]

⟨Θ(F), ⊑⟩ is not pairwise incomparable. By defining TypInf^{∗}(F) as Min(⟨Θ(F), ⊑⟩), we ensure that if F is a feature structure then ⟨TypInf^{∗}(F), ⊑⟩ is pairwise incomparable. 51: Lemma If F ∈ F then for each F′′ ∈ Θ(F),

for some F′ ∈ TypInf^{∗}(F), F′ ⊑ F′′. Proof

F ∈ F

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and TypDom^{∗}(F) ⊆ \{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\}

⟹ F = ⟨Q, \overline{q}, θ, δ⟩ and Θ(F) ⊆ \{⟨Q, \overline{q}, θ′, δ⟩ | θ′ : Q → Type\}

⟹ ⟨Θ(F), ⊑⟩ is a downward Noetherian preorder by lemmata 11 and 69 ⟹ for each F′′ ∈ Θ(F), for some F′ ∈ TypInf^{∗}(F), F′ ⊑ F′′. by lemma 38

□ 52: Proposition If F ∈ F and F′′ ∈ TypInf^{∗}(F) then

F ⊑ F′′. Proof

F ∈ F and F′′ ∈ TypInf^{∗}(F)
⟹ F ∈ F and F′′ ∈ Θ(F)

3 MODIFICATION 31

⟹ F ∈ F and for some F′ ∈ TypDom^{∗}(F),

TypRan(F′) is defined and F′′ = TypRan(F′)

⟹ for some F′ ∈ STF, F ⊑ F′ and F′ ⊑ F′′ by propositions 46 and 30

⟹ F ⊑ F′′.

□ 53: Proposition If F ∈ F and F′′ ∈ TF then

F ⊑ F′′ iff for some F′ ∈ TypInf^{∗}(F), F′ ⊑ F′′. Proof

F ⊑ F′′

⟺ for some F^{∗} ∈ TypDom^{∗}(F), F^{∗} ⊑ F′′ by propositions 14 and 47

⟺ for some F^{∗} ∈ TypDom^{∗}(F),

TypRan(F^{∗}) is defined and TypRan(F^{∗}) ⊑ F′′ by proposition 31

⟺ for some F^{∗∗} ∈ Θ(F), F^{∗∗} ⊑ F′′

⟺ for some F′ ∈ TypInf^{∗}(F), F′ ⊑ F′′. by lemma 51 □

3.4 Relating TypInf and TypInf^{∗}

This subsection shows that if the feature introduction condition holds then TypDom^{∗} and TypInf^{∗} reduce to TypDom and TypInf. Warning! Throughout 3.4 we assume the existence of a feature introduction function Intro : Feat → Type. 54: Lemma If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then for each q ∈ Q and each t ∈ Type,

t ∈ ψ_{F} (q) iff Φ_{F} (q) is defined and Φ_{F} (q) ⊑ t. Proof For each q ∈ Q and each t ∈ Type,

t ∈ ψ_{F} (q)

⟺ θ(q) ⊑ t and for each f ∈ Feat,

if δ(f, q) is defined then Approp(f, t) is defined

⟺ θ(q) ⊑ t and for each f ∈ Feat, if δ(f, q) is defined then Intro(f) ⊑ t ⟺ Φ_{F} (q) is defined and Φ_{F} (q) ⊑ t.

□ 55: Lemma If F = ⟨Q, \overline{q}, θ, δ⟩ ∈ F then for each q ∈ Q,

Ψ_{F} (q) = \{ \begin{matrix}\{Φ_{F} (q)\} & if Φ_{F} (q) is defined \\ ∅ & if Φ_{F} (q) is undefined. \end{matrix}

Proof Firstly, for each q ∈ Q,

Φ_{F} (q) is defined

⟹ Φ_{F} (q) ∈ ψ_{F} (q) and for each t ∈ ψ_{F} (q), Φ_{F} (q) ⊑ t by lemma 54 3 MODIFICATION 32

⟹ Φ_{F} (q) ∈ Ψ_{F} (q) and for each t ∈ Ψ_{F} (q), Φ_{F} (q) ⊑ t ⟹ Φ_{F} (q) ∈ Ψ_{F} (q) and for each t ∈ Ψ_{F} (q), Φ_{F} (q) = t by lemma 42 ⟹ Ψ_{F} (q) = {Φ_{F} (q)}. … (1)

Secondly, for each q ∈ Q, Φ_{F} (q) is undefined ⟹ ψ_{F} (q) = ∅ by lemma 54 ⟹ Ψ_{F} (q) = ∅. … (2)

By (1) and (2), for each q ∈ Q,

Ψ_{F} (q) = \{ \begin{matrix}\{Φ_{F} (q)\} & if Φ_{F} (q) is defined \\ ∅ & if Φ_{F} (q) is undefined. \end{matrix} □ 56: Proposition If F ∈ F then

TypDom^{∗}(F) = \{ \begin{matrix}\{T ypDom(F)\} & if TypDom(F) is defined \\ ∅ & if TypDom(F) is undefined. \end{matrix}

Proof Suppose

F = ⟨Q, \overline{q}, θ, δ⟩. Firstly,

TypDom(F) is defined ⟹ for each q ∈ Q, Φ_{F} (q) is defined ⟹ for each q ∈ Q, Ψ_{F} (q) = {Φ_{F} (q)} by lemma 55 ⟹ Choice(Ψ_{F}) = {Φ_{F} } ⟹ TypDom^{∗}(F) = {TypDom(F)}. … (1)

Secondly, TypDom(F) is undefined ⟹ for some q ∈ Q, Φ_{F} (q) is undefined ⟹ for each q ∈ Q, Ψ_{F} (q) = ∅ by lemma 55 ⟹ Choice(Ψ_{F}) = ∅ ⟹ TypDom^{∗}(F) = ∅. … (2)

By (1) and (2),

TypDom^{∗}(F) = \{ \begin{matrix}\{T ypDom(F)\} & if TypDom(F) is defined \\ ∅ & if TypDom(F) is undefined. \end{matrix} □ 57: Proposition If F ∈ F then

TypInf^{∗}(F) = \{ \begin{matrix}\{T ypInf(F)\} & if TypInf(F) is defined \\ ∅ & if TypInf(F) is undefined. \end{matrix}

Proof Firstly,

TypInf(F) is defined ⟹ TypDom(F) is defined and TypRan(TypDom(F)) is defined A APPENDIX 33

⟹ TypDom^{∗}(F) = {TypDom(F)} and TypRan(TypDom(F)) is defined

by proposition 56

⟹ Θ(F) = {TypInf(F)} ⟹ TypInf^{∗}(F) = {TypInf(F)}. … (1)

Secondly, TypInf(F) is undefined ⟹ TypDom(F) is undefined, or

TypDom(F) is defined and TypRan(TypDom(F)) is undefined ⟹ TypDom^{∗}(F) = ∅, or

TypDom^{∗}(F) = {TypDom(F)} and TypRan(TypDom(F)) is undefined,

by proposition 56

⟹ TypInf^{∗}(F) = ∅. … (2) By (1) and (2),

TypInf^{∗}(F) = \{ \begin{matrix}\{T ypInf(F)\} & if TypInf(F) is defined \\ ∅ & if TypInf(F) is undefined. \end{matrix} □

A Appendix

This appendix contains the standard mathematical definitions and results concerning preorders that the reader needs to understand our paper. 58: Definition (preorder) A preorder is a pair ⟨P, ⪯⟩ such that

P is a set, ⪯ is a binary relation, for each p ∈ P, p ⪯ p, and for each p_{1}, p_{2}, p_{3} ∈ P, if p_{1} ⪯ p_{2} and p_{2} ⪯ p_{3} then p_{1} ⪯ p_{3}.

59: Definition (finite preorder) A finite preorder is a pair ⟨P, ⪯⟩ such that

⟨P, ⪯⟩ is a preorder, and P is finite.

60: Definition (pairwise incomparable preorder) A pairwise incomparable preorder is a pair ⟨P, ⪯⟩ such that

⟨P, ⪯⟩ is a preorder, and for each p_{1}, p_{2} ∈ P, if p_{1} ⪯ p_{2} then p_{1} = p_{2}.

61: Definition (partial order) A partial order is a pair ⟨P, ⪯⟩ such that

⟨P, ⪯⟩ is a preorder, and for each p_{1}, p_{2} ∈ P, if p_{1} ⪯ p_{2} and p_{2} ⪯ p_{1} then p_{1} = p_{2}.

62: Definition (upper bound) If ⟨P, ⪯⟩ is a preorder and S ⊆ P then an upper bound of S in ⟨P, ⪯⟩ is an entity p such that A APPENDIX 34

p ∈ P, and for each s ∈ S, s ⪯ p.

63: Definition (least upper bound) If ⟨P, ⪯⟩ is a preorder and S ⊆ P then a least upper bound of S in ⟨P, ⪯⟩ is an entity p such that

p is an upper bound of S in ⟨P, ⪯⟩, and if p′ is an upper bound of S in ⟨P, ⪯⟩ then p ⪯ p′.

64: Definition (bounded complete preorder) A bounded complete preorder is a pair ⟨P, ⪯⟩ such that

⟨P, ⪯⟩ is a preorder, and for each S ⊆ P,

if S has an upper bound in ⟨P, ⪯⟩

then S has a least upper bound in ⟨P, ⪯⟩.

65: Definition (minimal member) If ⟨P, ⪯⟩ is a preorder then a minimal member of ⟨P, ⪯⟩ is an entity p such that

p ∈ P, and for each p′ ∈ P, if p′ ⪯ p then p ⪯ p′.

66: Definition (maximal member) If ⟨P, ⪯⟩ is a preorder then a maximal member of ⟨P, ⪯⟩ is an entity p such that

p ∈ P, and for each p′ ∈ P, if p ⪯ p′ then p′ ⪯ p.

67: Definition (upward Noetherian preorder) An upward Noetherian preorder is a pair ⟨P, ⪯⟩ such that

⟨P, ⪯⟩ is a preorder, and for each S ⊆ P, if S ≠ ∅ then ⟨S, ⪯⟩ has a maximal member.

68: Definition (downward Noetherian preorder) A downward Noetherian preorder is a pair ⟨P, ⪯⟩ such that

⟨P, ⪯⟩ is a preorder, and for each S ⊆ P, if S ≠ ∅ then ⟨S, ⪯⟩ has a minimal member.

69: Lemma If ⟨P, ⪯⟩ is a finite preorder then

⟨P, ⪯⟩ is an upward Noetherian preorder, and ⟨P, ⪯⟩ is a downward Noetherian preorder.

Proof For each preorder ⟨P, ⪯⟩,

⟨P, ⪯⟩ is not upward Noetherian ⟹ for some S ⊆ P, S ≠ ∅ and ⟨S, ⪯⟩ has no maximal member ⟹ for some S ⊆ P,

S ≠ ∅ and for each s ∈ S, for some s′ ∈ S, s ⪯ s′ and s′ ⪯̸ s.

⟹ for some {s_{i} | i ∈ IN} ⊆ P, for each i ∈ IN, s_{i} ⪯ s_{i+1} and s_{i+1} ⪯̸ s_{i}.

B REFERENCES 35

⟹ for some {s_{i} | i ∈ IN} ⊆ P, for all i and j ∈ IN, i < j and s_{i} = s_{j} ⟹ i + 1 ≤ j and s_{i} = s_{j} ⟹ s_{i+1} ⪯ s_{j} and s_{i} = s_{j} ⟹ s_{i+1} ⪯ s_{i} ⟹ contradiction

⟹ for some {s_{i} | i ∈ IN} ⊆ P, for all i and j ∈ IN, if i ≠ j then s_{i} ≠ s_{j} ⟹ for some {s_{i} | i ∈ IN} ⊆ P, {s_{i} | i ∈ IN} is infinite ⟹ P is infinite ⟹ ⟨P, ⪯⟩ is not finite.

Thus,

if ⟨P, ⪯⟩ is a finite preorder then ⟨P, ⪯⟩ is an upward Noetherian preorder. Similarly, for each preorder ⟨P, ⪯⟩,

if ⟨P, ⪯⟩ is not downward Noetherian then ⟨P, ⪯⟩ is not finite. Thus,

if ⟨P, ⪯⟩ is a finite preorder then ⟨P, ⪯⟩ is a downward Noetherian preorder. □ 70: Lemma If ⟨{p_{n} | n ∈ IN}, ⪯⟩ is an upward Noetherian partial order and for each n ∈ IN, p_{n} ⪯ p_{n+1} then

⟨{p_{n} | n ∈ IN}, ⪯⟩ has a unique maximal member. Proof Firstly, since ⟨{p_{n} | n ∈ IN}, ⪯⟩ is an upward Noetherian preorder,

⟨{p_{n} | n ∈ IN}, ⪯⟩ has a maximal member. Secondly, for each i and j ∈ IN,

p_{i} and p_{j} are maximal members of ⟨{p_{n} | n ∈ IN}, ⪯⟩ ⟹^{wlog} p_{i} and p_{j} are maximal members of ⟨{p_{n} | n ∈ IN}, ⪯⟩ and i ≤ j ⟹ p_{i} and p_{j} are maximal members of ⟨{p_{n} | n ∈ IN}, ⪯⟩ and p_{i} ⪯ p_{j} ⟹ p_{i} ⪯ p_{j} and p_{j} ⪯ p_{i} ⟹ p_{i} = p_{j}. since ⟨{p_{n} | n ∈ IN}, ⪯⟩ is a partial order

Thus,

⟨{p_{n} | n ∈ IN}, ⪯⟩ has a unique maximal member. □

B References

[Carpenter 1992]. Bob Carpenter. The Logic of Typed Feature Structures. Volume 32 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. Cambridge, Massachusetts, USA. 1992.

[Kay 1979]. Martin Kay. “Functional Grammar”. In (pages 142-158): C. Chiarello et. al. (editors). The Proceedings of the 5th Annual Meeting of the Berkeley Linguistics Society. Berkeley Linguistics Society. Berkeley, California, USA. 1979.

[Kay 1984]. Martin Kay. “Functional Unification Grammar: a Formalism for Machine Translation”. In (pages 75-78): The Proceedings of the 10th International Conference on Computational Linguistics. North-Holland. Amsterdam, The Netherlands. 1984.

[King 1989]. Paul J. King. A Logical Formalism for Head-driven Phrase Structure

Grammar. Ph. D. Thesis. Manchester University. Manchester, England. 1989. [Pollard and Moshier 1990]. Carl J. Pollard and M. Drew Moshier. “Unifying

Partial Descriptions of Sets”. In: P. Hanson (editor). Information, Language and Cognition. Volume 1 of Vancouver Studies in Cognitive Science. 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 (Volume 1: Fundamentals). Number 13 of CSLI Lecture Notes. CSLI Publications. Stanford, California, USA. 1987.

[Pollard and Sag 1993]. Carl J. Pollard and Ivan A. Sag. Head-driven Phrase Structure Grammar. University of Chicago Press and CSLI Publications. Chicago, Illinois, USA. 1993.

[Smolka 1988]. Gert Smolka. A Feature Logic with Subsorts. LILOG-Report 33. IBM Deutschland GmbH. Stuttgart, Germany. 1988.