TYPED FEATURE STRUCTURES AS DESCRIPTIONS

Paul John King^{∗}

Seminar für Sprachwissenschaft, Eberhard-Karls-Universität^{†}

ABSTRACT

A description is an entity that can be interpreted as true or false of an object, and using feature structures as descriptions accrues several computational benefits. In this paper, I create an explicit interpretation of a typed feature structure used as a description, define the notion of a satisfiable feature structure, and create a simple and effective algorithm to decide if a feature structure is satisfiable.

1. INTRODUCTION

Describing objects is one of several purposes for which linguists use feature structures. A description is an entity that can be interpreted as true or false of an object. For example, the conventional interpretation of the description ‘it is black’ is true of a soot particle, but false of a snowflake. Therefore, any use of a feature structure to describe an object demands that the feature structure can be interpreted as true or false of the object. In this paper, I tailor the semantics of [King 1989] to suit the typed feature structures of [Carpenter 1992], and so create an explicit interpretation of a typed feature structure used as a description. I then use this interpretation to define the notion of a satisfiable feature structure. Though no feature structure algebra provides descriptions as expressive as those provided by a feature logic, using feature structures to describe objects profits from a large stock of available computational techniques to represent, test and process feature structures. In this paper, I demonstrate the computational benefits of marrying a tractable syntax and an explicit semantics by creating a simple and effective algorithm to decide the satisfiability of a feature structure. Gerdemann and Götz’s Troll type resolution system implements both the semantics and an efficient refinement of the satisfiability algorithm I present here (see [Götz 1993], [Gerdemann and King 1994] and [Gerdemann (fc)]).

2. A FEATURE STRUCTURE SEMANTICS

A signature provides the symbols from which to construct typed feature structures, and an interpretation gives those symbols meaning. Definition 1. Σ is a signature iff Σ is a sextuple ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩, 𝔔 is a set, ⟨𝔗, ⪯⟩ is a partial order,

𝔖 = \{σ ∈ 𝔗 |\begin{matrix}for each τ ∈ 𝔗, \\ if σ ⪯ τ then σ = τ \end{matrix} \},

𝔄 is a set,

𝔉 is a partial function from the Cartesian product of 𝔗 and 𝔄 to 𝔗, and for each τ ∈ 𝔗, each τ′ ∈ 𝔗 and each α ∈ 𝔄,

if 𝔉(τ, α) is defined and τ ⪯ τ′ then 𝔉(τ′, α) is defined, and 𝔉(τ, α) ⪯ 𝔉(τ′, α).

Henceforth, I tacitly work with a signature ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩. I call members of 𝔔 states, members of 𝔗 types, ⪯ subsumption, members of 𝔖 species, members of 𝔄 attributes, and 𝔉 appropriateness. Definition 2. 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(u), α) is defined, and

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

Suppose that I is an interpretation ⟨U, S, A⟩. I call each member of U an object in I.

∗The research presented in this paper was sponsored by Teilprojekt B4 “Constraints on Grammar for Efficient Generation” of the Sonderforschungsbereich 340 of the Deutsche Forschungsgemeinschaft. I also wish to thank Bob Carpenter, Dale Gerdemann, Thilo Götz and Jennifer King for their invaluable help with this paper.

†Wilhelmstr. 113, 72074 Tübingen, Germany.

Email: king@sfs.nphil.uni-tuebingen.de.

Each type denotes a set of objects in I. The denotations of the species partition U, and S assigns each object in I the unique species whose denotation contains the object: object u is in the denotation of species σ iff σ = S(u). Subsumption encodes a relationship between the denotations of species and types: object u is in the denotation of type τ iff τ ⪯ S(u). So, if τ_{1} ⪯ τ_{2} then the denotation of type τ_{1} contains the denotation of type τ_{2}. Each attribute denotes a partial function from the objects in I to the objects in I, and A assigns each attribute the partial function it denotes. Appropriateness encodes a relationship between the denotations of species and attributes: if 𝔉⟨σ, α⟩ is defined then the denotation of attribute α acts upon each object in the denotation of species σ to yield an object in the denotation of type 𝔉⟨σ, α⟩, but if 𝔉⟨σ, α⟩ is undefined then the denotation of attribute α acts upon no object in the denotation of species σ. So, if 𝔉⟨τ, α⟩ is defined then the denotation of attribute α acts upon each object in the denotation of type τ to yield an object in the denotation of type 𝔉⟨τ, α⟩. I call a finite sequence of attributes a path, and write 𝔓 for the set of paths. Definition 3. P is the path interpretation function under I iff

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

P is a total function from 𝔓 to the set of partial functions from U to U, and for each ⟨α_{1}, …, α_{n}⟩ ∈ 𝔓,

P ⟨α_{1}, …, α_{n}⟩ is the functional composition of A(α_{1}), …, A(α_{n}).

I write P_{I} for the path interpretation function under I. Definition 4. F is a feature structure iff

F is a quadruple ⟨Q, q, δ, θ⟩,

Q is a finite subset of 𝔔,

q ∈ Q,

δ is a finite partial function from the Cartesian product of Q and 𝔄 to Q, θ is a total function from Q to 𝔗, and for each q′ ∈ Q,

for some π ∈ 𝔓, π runs to q′ in F, where ⟨α_{1}, …, α_{n}⟩ runs to q′ in F iff

⟨α_{1}, …, α_{n}⟩ ∈ 𝔓,

q′ ∈ Q, and

for some {q_{0}, …, q_{n}} ⊆ Q, q = q_{0}, for each i < n,

δ(q_{i}, α_{i+1}) is defined, and
δ(q_{i}, α_{i+1}) = q_{i+1}, and

q_{n} = q′. Each feature structure is a connected Moore machine (see [Moore 1956]) with finitely many states, input alphabet 𝔄, and output alphabet 𝔗. Definition 5. F is true of u under I iff F is a feature structure ⟨Q, q, δ, θ⟩, I is an interpretation ⟨U, S, A⟩, u is an object in I, and for each π_{1} ∈ 𝔓, each π_{2} ∈ 𝔓 and each q′ ∈ Q,

if π_{1} runs to q′ in F, and

π_{2} runs to q′ in F

then P_{I}(π_{1})(u) is defined,

P_{I}(π_{2})(u) is defined,
P_{I}(π_{1})(u) = P_{I}(π_{2})(u), and
θ(q′) ⪯ S(P_{I}(π_{1})(u)).

Definition 6. F is a satisfiable feature structure iff

F is a feature structure, and

for some interpretation I and some object u in I, F is true of u under I.

3. MORPHS

The abundance of interpretations seems to preclude an effective algorithm to decide if a feature structure is satisfiable. However, I insert morphs between feature structures and objects to yield an interpretation free characterisation of a satisfiable feature structure. Definition 7. M is a semi-morph iff

M is a triple ⟨Δ, Γ, Λ⟩,

Δ is a nonempty subset of 𝔓,

Γ 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}), and for each α ∈ 𝔄 and each π ∈ 𝔓,

if πα ∈ Δ

then π ∈ Δ, 𝔉(Λ(π), α) is defined, and

𝔉(Λ(π), α) ⪯ Λ(πα). Definition 8. M is a morph iff M is a semi-morph ⟨Δ, Γ, Λ⟩, and for each α ∈ 𝔄 and each π ∈ 𝔓,

if π ∈ Δ and 𝔉(Λ(π), α) is defined then πα ∈ Δ.

Each morph is the Moshier abstraction (see [Moshier 1988]) of a connected and totally well-typed (see [Carpenter 1992]) Moore machine with possibly infinitely many states, input alphabet 𝔄, and output alphabet 𝔖.

Definition 9. M abstracts u under I iff M is a morph ⟨Δ, Γ, Λ⟩, I is an interpretation ⟨U, S, A⟩, u is an object in I, for each π_{1} ∈ 𝔓 and each π_{2} ∈ 𝔓,

⟨π_{1}, π_{2}⟩ ∈ Γ iff P_{I}(π_{1})(u) is defined,

P_{I}(π_{2})(u) is defined, and P_{I}(π_{1})(u) = P_{I}(π_{2})(u), and

for each σ ∈ 𝔖 and each π ∈ 𝔓, ⟨π, σ⟩ ∈ Λ iff P_{I}(π)(u) is defined, and

σ = S(P_{I}(π)(u)). Proposition 10. For each interpretation I and each object u in I,

some unique morph abstracts u under I. I thus write of the abstraction of u under I. Definition 11. 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, write S̃ for the total function from Ũ to 𝔖, where

for each σ ∈ 𝔖 and each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ, S̃⟨Δ, Γ, Λ, E⟩ = σ iff for some π ∈ E, Λ(π) = σ,

and write Ã for the total function from 𝔄 to the set of partial functions from Ũ to Ũ, where

for each α ∈ 𝔄, each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ and each ⟨Δ′, Γ′, Λ′, E′⟩ ∈ Ũ,

Ã(α)⟨Δ, Γ, Λ, E⟩ is defined, and Ã(α)⟨Δ, Γ, Λ, E⟩ = ⟨Δ′, Γ′, Λ′, E′⟩ iff ⟨Δ, Γ, Λ⟩ = ⟨Δ′, Γ′, Λ′⟩, and

for some π ∈ E, πα ∈ E′. Lemma 12. ⟨Ũ, S̃, Ã⟩ is an interpretation. I write Ĩ for ⟨Ũ, S̃, Ã⟩. Lemma 13. For each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ, each ⟨Δ′, Γ′, Λ′, E′⟩ ∈ Ũ and each π ∈ 𝔓,

P_{I}(π)⟨Δ, Γ, Λ, E⟩ is defined, and

P_{I}(π)⟨Δ, Γ, Λ, E⟩ = ⟨Δ′, Γ′, Λ′, E′⟩

iff ⟨Δ, Γ, Λ⟩ = ⟨Δ′, Γ′, Λ′⟩, and

for some π′ ∈ E, π′π ∈ E′. Proof. By induction on the length of π. Lemma 14. For each ⟨Δ, Γ, Λ, E⟩ ∈ Ũ,

if E is the equivalence class of the empty

path under Γ then the abstraction of ⟨Δ, Γ, Λ, E⟩ under Ĩ

is ⟨Δ, Γ, Λ⟩. Proposition 15. For each morph M,

for some interpretation I and some object u in I,

M is the abstraction of u under I.

Definition 16. F approximates M iff F is a feature structure ⟨Q, q, δ, θ⟩, M is a morph ⟨Δ, Γ, Λ⟩, and for each π_{1} ∈ 𝔓, each π_{2} ∈ 𝔓 and each q′ ∈ Q,

if π_{1} runs to q′ in F, and

π_{2} runs to q′ in F

then ⟨π_{1}, π_{2}⟩ ∈ Γ, and

θ(q′) ⪯ Λ(π_{1}).

A feature structure approximates a morph iff the Moshier abstraction of the feature structure abstractly subsumes (see [Carpenter 1992]) the morph. Proposition 17. For each interpretation I, each object u in I and each feature structure F,

F is true of u under I

iff F approximates the abstraction of u

under I. Theorem 18. For each feature structure F,

F is satisfiable iff F approximates some morph.

Proof. From propositions 15 and 17.

4. RESOLVED FEATURE STRUCTURES

Though theorem 18 gives an interpretation free characterisation of a satisfiable feature structure, the characterisation still seems to admit of no effective algorithm to decide if a feature structure is satisfiable. However, I use theorem 18 and resolved feature structures to yield a less general interpretation free characterisation of a satisfiable feature structure that admits of such an algorithm. Definition 19. R is a resolved feature structure iff

R is a feature structure ⟨Q, q, δ, ρ⟩,

ρ is a total function from Q to 𝔖, and for each α ∈ 𝔄 and each q′ ∈ Q,

if δ(q′, α) is defined

then 𝔉(ρ(q′), α) is defined, and 𝔉(ρ(q′), α) ⪯ ρ(δ(q′, α)).

Each resolved feature structure is a well-typed (see [Carpenter 1992]) feature structure with output alphabet 𝔖. Definition 20. R is a resolvant of F iff

R is a resolved feature structure ⟨Q, q, δ, ρ⟩, F is a feature structure ⟨Q, q, δ, θ⟩, and for each q′ ∈ Q, θ(q′) ⪯ ρ(q′).

Proposition 21. For each interpretation I, each object u in I and each feature structure F,

F is true of u under I

iff some resolvant of F is true of u under I.

Definition 22. ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is rational iff for each σ ∈ 𝔖 and each α ∈ 𝔄,

if 𝔉(σ, α) is defined

then for some σ′ ∈ 𝔖, 𝔉(σ, α) ⪯ σ′. Proposition 23. If ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is rational then for each resolved feature structure R, R is satisfiable. Proof. Suppose that R = ⟨Q, q, δ, ρ⟩ and β is a bijection from ordinal ζ to 𝔖. Let

Δ_{0} = \{π |\begin{matrix}for some q′ ∈ Q, \\ π runs to q′ in R \end{matrix}\},

Γ_{0} = \{⟨π_{1}, π_{2}⟩ |\begin{matrix}for some q′ ∈ Q, \\ π_{1} runs to q′ in R, and \\ π_{2} runs to q′ in R \end{matrix}\},

and

Λ_{0} = \{⟨π, σ⟩ |\begin{matrix}for some q′ ∈ Q, \\ π runs to q′ in R, and \\ σ = ρ(q′) \end{matrix}\}.

For each n ∈ IN, let Δ_{n+1} =

Δ_{n} ∪ \{πα |\begin{matrix}α ∈ 𝔄, \\ π ∈ Δ_{n}, and \\ 𝔉(Λ_{n}(π), α) is defined \end{matrix}\},

Γ_{n+1} =

Γ_{n} ∪ \{⟨π_{1}α, π_{2}α⟩ |\begin{matrix}α ∈ 𝔄, \\ π_{1}α ∈ Δ_{n+1}, \\ π_{2}α ∈ Δ_{n+1}, and \\ ⟨π_{1}, π_{2}⟩ ∈ Γ_{n}, \end{matrix}\}, and

Λ_{n+1} =

Λ_{n} ∪ \{⟨πα, β(ξ)⟩ |\begin{matrix}α ∈ 𝔄, \\ π ∈ Δ_{n}, \\ πα ∈ Δ_{n+1} \ Δ_{n}, and \\ ξ is the least ordinal \\ in ζ such that \\ 𝔉(Λ_{n}(π), α) ⪯ β(ξ) \end{matrix}\}.

For each n ∈ IN, ⟨Δ_{n}, Γ_{n}, Λ_{n}⟩ is a semi-morph. Let

Δ = ⋃{Δ_{n} | n ∈ IN},

Γ = ⋃{Γ_{n} | n ∈ IN}, and

Λ = ⋃{Λ_{n} | n ∈ IN}. ⟨Δ, Γ, Λ⟩ is a morph that R approximates. By theorem 18, R is satisfiable. Theorem 24. If ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is rational then for each feature structure F,

F is satisfiable iff F has a resolvant. Proof. From propositions 21 and 23.

5. A SATISFIABILITY ALGORITHM

In this section, I use theorem 24 to show how – given a rational signature that meets reasonable computational conditions – to construct an effective algorithm to decide if a feature structure is satisfiable.

Definition 25. ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is computable iff

𝔔, 𝔗 and 𝔄 are countable,

𝔖 is finite,

for some effective function SUB, for each τ_{1} ∈ 𝔗 and each τ_{2} ∈ 𝔗,

if τ_{1} ⪯ τ_{2}
then SUB(τ_{1}, τ_{2}) = ‘true’
otherwise SUB(τ_{1}, τ_{2}) = ‘false’, and

for some effective function APP, for each τ ∈ 𝔗 and each α ∈ 𝔄,

if 𝔉(τ, α) is defined then APP(τ, α) = 𝔉(τ, α) otherwise APP(τ, α) =‘undefined’. Proposition 26. If ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is computable then for some effective function RES,

for each feature structure F,

RES(F) = a list of the resolvants of F. Proof. Since ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is computable, for some effective function GEN,

for each finite Q ⊆ 𝔔, GEN(Q) = a list of the total functions from Q to 𝔖,

for some effective function TEST_{1}, for each finite set Q, each finite partial function δ from the Cartesian product of Q and 𝔄 to Q, and each total function θ from Q to 𝔗,

if for each ⟨q, α⟩ in the domain of δ, 𝔉(θ(q), α) is defined, and 𝔉(θ(q), α) ⪯ θ(δ(q, α))

then TEST_{1}(δ, θ) = ‘true’

otherwise TEST_{1}(δ, θ) = ‘false’, and for some effective function TEST_{2},

for each finite set Q, each total function θ_{1} from Q to 𝔗 and each total function θ_{2} from Q to 𝔗,

if for each q ∈ Q, θ_{1}(q) ⪯ θ_{2}(q) then TEST_{2}(θ_{1}, θ_{2}) = ‘true’ otherwise TEST_{2}(θ_{1}, θ_{2}) = ‘false’.

Construct RES as follows:

for each feature structure ⟨Q, q, δ, θ⟩, set Σ_{in} = GEN(Q) and Σ_{out} = ⟨⟩ while Σ_{in} = ⟨ρ, ρ_{1}, …, ρ_{i}⟩ is not empty do set Σ_{in} = ⟨ρ_{1}, …, ρ_{i}⟩

if TEST_{1}(δ, ρ) = ‘true’,
TEST_{2}(θ, ρ) = ‘true’, and
Σ_{out} = ⟨ρ′_{1}, …, ρ′_{j}⟩
then set Σ_{out} = ⟨ρ, ρ′_{1}, …, ρ′_{j}⟩

if Σ_{out} = ⟨ρ_{1}, …, ρ_{n}⟩

then output ⟨⟨Q, q, δ, ρ_{1}⟩,..., ⟨Q, q, δ, ρ_{n}⟩⟩. RES is an effective algorithm, and for each feature structure F,

RES(F) = a list of the resolvants of F.

Theorem 27. If ⟨𝔔, 𝔗, ⪯, 𝔖, 𝔄, 𝔉⟩ is rational and computable then for some effective function SAT,

for each feature structure F, if F is satisfiable then SAT(F) = ‘true otherwise SAT(F) = ‘false’.

Proof. From theorem 24 and proposition 26.

Gerdemann and Götz’s Troll system (see [Götz 1993], [Gerdemann and King 1994] and [Gerdemann (fc)]) employs an efficient refinement of RES to test the satisfiability of feature structures. In fact, Troll represents each feature structure as a disjunction of the resolvants of the feature structure. Loosely speaking, the resolvants of a feature structure have the same underlying finite state automaton as the feature structure, and differ only in their output function. Troll exploits this property to represent each feature structure as a finite state automaton and a set of output functions. The Troll unifier is closed on these representations. Thus, though RES is computationally expensive, Troll uses RES only during compilation, never during run time.

References

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

[Gerdemann (fc)] Dale Gerdemann. Troll: type resolution system, user’s guide. Sonderforschungsbereich 340 technical report. Eberhard-Karls-Universität, Tübingen, Germany. Forthcoming.

[Gerdemann and King (1994)] Dale Gerdemann and Paul John King. The correct and efficient implementation of appropriateness specifications for typed feature structures. In these proceedings.

[Götz 1993] Thilo Götz. A normal form for typed feature structures. Master’s thesis. Eberhard-Karls-Universität, Tübingen, Germany. 1993.

[King 1989] Paul John King. A logical formalism for head-driven phrase structure grammar. Doctoral thesis. The University of Manchester, Manchester, England. 1989.

[Moore 1956] E. F. Moore. ‘Gedanken experiments on sequential machines’. In Automata Studies. Princeton University Press, Princeton, New Jersey, USA. 1956.

[Moshier 1988] Michael Andrew Moshier. Extensions to unification grammar for the description of programming languages. Doctoral thesis. The University of Michigan, Ann Arbor, Michigan, USA. 1988.