Off-Line Parsability and the Well-Foundedness of Subsumption.
Typed feature structures are used extensively for the specification of linguistic information in many formalisms. The subsumption relation orders TFSs by their information content. We prove that subsumption of acyclic TFSs is well founded, whereas in the presence of cycles general TFS subsumption is not well founded. We show an application of this result for parsing, where the well-foundedness of subsumption is used to guarantee termination for grammars that are off-line parsable. We define a new version of off-line parsability that is less strict than the existing one; thus termination is guaranteed for parsing with a larger set of grammars.
Introduction
Feature structures serve as a means for the specification of linguistic information in current
linguistic formalisms such as LFG (Kaplan and Bresnan, 1982), HPSG (Pollard and Sag,
1994) or (some versions of) Categorial Grammar (Haddock, Klein, and Morill, 1987). This
paper focuses on typed feature structures (TFSs) that are a generalization of their untyped
counterparts. TFSs are related by subsumption (see (Carpenter, 1992b)) according to their
Journal of Logic, Language and Information, accepted for publication
information content. We show that the subsumption relation is well-founded for acyclic TFSs,
but not for cyclic ones. We use this result to prove that parsing is terminating for grammars
that are off-line parsable: this proposition is cited, but not proved, in (Shieber, 1992). We
also suggest a less strict definition for off-line parsability that guarantees termination in the
case of acyclic TFSs.
This work has originated out of our interest in the theoretical aspects of parsing with
grammars that are based on TFSs (see (Wintner and Francez, 1995b)). While the results
presented here are basically theoretical, we have implemented a system for efficient processing
of such grammars, based on abstract machine techniques; this work is presented in (Wintner
and Francez, 1995a). The rest of this paper is organized as follows: section 2 outlines the
theory of TFSs of (Carpenter, 1992b). In section 3 we discuss the well-foundedness of TFS
subsumption. We sketch a theory of parsing in section 4 and discuss off-line parsability of
TFS-based grammars in section 5.
2 Theory of feature structures
This section summarizes some preliminary notions along the lines of (Carpenter, 1992b).
While we use the terminology of typed feature structures, all the results are valid for untyped
structures, that are a special case of TFSs. (Carpenter, 1992b) defines well-typed and totally
well-typed feature structures that are subsets of the set of TFSs; for generality, we assume
nothing about the well-typedness of TFSs below. However, the larger context of our work is
done in a setup where features are assigned to types through an appropriateness specification,
and hence we retain the term typed feature structures rather than sorted ones. For the
following discussion we fix non-empty, finite, disjoint sets Types and Feats of types and
features, respectively, and an infinite set Nodes of nodes, disjoint of Types and Feats,
each member of which is assigned a type from Types through a fixed typing function
Nodes ! Types. The set Nodes is 'rich' in the sense that for every t 2 Types, the set
Below, the meta-variable T ranges over subsets of Types, t - over types, f - over features
and q - over nodes. For a partial function F , 'F (x)#' means that F is defined for the value
x. Whenever the result of an application of a partial function is used as an operand, it is
meant that the function is defined for its arguments. IN denotes the set of natural numbers.
A partial order v over Types is a type hierarchy if it is bounded complete, i.e., if every
up-bounded subset T of Types has a (unique) least upper bound, tT . If t v t 0 , t is said to
be more general than t 0 , which is more specific than t. t 0 is a subtype of t. is the
most general tTypes is the most specific, inconsistent type. All occurrences of ?
are identified.
A feature structure (over the parameters Nodes, Types and Feats) is a directed,
connected, labeled graph consisting of a finite, nonempty set of nodes Q ' Nodes, a root
Q, and a partial function specifying the arcs, such that every node
accessible from - q. A; B (with or without subscripts) range over feature structures
and Q; -
(with the same subscripts) over their constituents. 1 Let TFSs be the set of all
typed feature structures (over the fixed parameters Nodes, Types and Feats).
A path is a finite sequence of features, and the set Feats   is the collection of
paths. ffl is the empty path. -; ff (with or without subscripts) range over paths. The definition
of ffi is extended to paths in the natural way: ffi(q; -). The
paths of a feature structure A are -)#g. Note that for
every TFS A, \Pi(A) 6= OE since ffl 2 \Pi(A) for every A.
A feature structure
q; ffi) is cyclic if there exist a non-empty path ff 2 Paths
and a node q 2 Q such that ffi(q; q. It is acyclic otherwise. Let ATFSs be the set of all
acyclic TFSs (over the fixed parameters). A feature structure
q; ffi) is reentrant iff
there exist two different paths
Definition 2.1 (Subsumption) A
exists a total function subsumption morphism) such that
ffl for every q 2
ffl for every q 2 Q 1 and for every f such that
Untyped feature structures can be modeled by TFSs: consider a particular type hierarchy in which the set
of types is the set of atoms, plus the types complex and ?, ? subsumes every other type, and the rest of the
types are incomparable. All features are appropriate for the type complex only, with ? as their appropriate
value. Atomic nodes are labeled by an atom, non-atomic nodes - by complex and variables - by ?.
The symbol 'v' is overloaded to denote subsumption (in addition to the subtype relation).
The morphism h associates with every node in Q 1 a node in Q 2 with at least as specific a
moreover, if an arc labeled f connects q with q 0 in A 1 , then such an arc connects h(q)
with h(q 0 ) in A 2 . Two properties follow directly from the definition: If A v B then every
path defined in A is defined in B, and if two paths are reentrant in A they are reentrant in
B.
If two feature structures subsume each other then they have exactly the same structure.
The only thing that distinguishes between them is the identity of the nodes. This information
is usually irrelevant, and thus an isomorphism is defined over TFSs as follows: A and B are
alphabetic variants (denoted A - B) iff A v B and B v A. A strictly subsumes B
If A strictly subsumes B then one of following cases must hold: either B contains paths
that A doesn't; or there is a path in B that ends in a node with a type that is greater than
its counterpart in A; or B contains 'more reentrancies': paths that lead to the same node in
B lead to different nodes in A.
Lemma 2.2 If A ! B (through the subsumption morphism h) then at least one of the following
conditions holds:
1. There exists a path - 2 \Pi(B) n \Pi(A)
2. There exists a node q 2 QA such that '(q) ! '(h(q)),
3. There exist paths
Well-foundedness
In this section we discuss the well-foundedness of TFS subsumption. A partial order - on a set
D is well-founded iff there does not exist an infinite decreasing sequence d 0 - d 1 - d
of elements of D. We prove that subsumption of acyclic TFSs is well-founded, and show an
example of general (cyclic) TFSs for which subsumption is not well-founded. While these
results are not surprising, and in fact might be deduced from works such as, e.g., (Moshier
and Rounds, 1987) or (Shieber, 1992), they were not, to the best of our knowledge, spelled
out explicitly before.
Lemma 3.1 A TFS A is acyclic iff \Pi(A) is finite.
Proof: If A is cyclic, there exists a node q 2 Q and a non-empty path ff that ffi(q;
Since q is accessible, let - be the path from the root to q: ffi( -
q. The infinite set of
paths contained in \Pi(A).
If A is acyclic then for every non-empty path ff 2 Paths and every q 2 Q, ffi(q; ff) 6= q. Q
is finite, and so is Feats, so the out-degree of every node is finite. Therefore the number of
different paths leaving -
q is bounded, and hence \Pi(A) is finite. 2
Definition 3.2 (Rank) Let r : Types ! IN be a total function such that r(t) ! r(t 0 ) if
. For an acyclic TFS A, let
IN be defined by \Delta(A).
By lemma 3.1, rank is well defined for acyclic TFSs. \Delta(A) can be thought of as the 'number
of reentrancies' in A: every node q 2 QA contributes to \Delta(A). For every
acyclic TFS A, \Delta(A) - 0 (clearly
Lemma 3.3 If A ! B and both are acyclic then
Proof: Since A v B, \Pi(A) ' \Pi(B). Consider the two possible cases:
ffl If
by the definitions of \Theta and subsumption;
by the definition of subsumption, since every reentrancy in A is a
reentrancy in B;
- By lemma 2.2, either case (2) holds), or \Delta(A) ! \Delta(B) (if case
(3) holds).
Hence
ffl If \Pi(A) ae \Pi(B) then
it might be the case that jQA j ! jQB j. But for every node q 2 QB that is not
the image of any node in QA , there exists a path - such that
Hence
Theorem 3.4 Subsumption of acyclic TFSs is well-founded.
Proof: For every acyclic TFS A,
rank(B). If an infinite decreasing sequence of acyclic TFSs existed, rank would have mapped
them to an infinite decreasing sequence in IN , which is a contradiction. Hence subsumption
is well-founded for acyclic TFSs. 2
Theorem 3.5 Subsumption of TFSs is not well-founded.
Proof: Consider the infinite sequence of TFSs A depicted graphically in figure 1.
For every i - 0, A to see that consider the morphism h i that maps - q i+1 to -
(i.e., the first i nodes of A i+1 are mapped to
the first i nodes of A i , and the additional node of A i+1 is mapped to the last node of A i ).
Clearly, for every i - 0, h i is a subsumption morphism. Hence, for every i - 0; A i w A i+1 .
To show strictness, assume a subsumption morphism
. By the third requirement of subsumption (h commuting with ffi), the first
nodes in A i have to be mapped by h 0 to the first i nodes in A i+1 . However, if q is
the 1-th node of A i , then ffi i (q) leads back to q, while ffi i+1 leads to the last node
of A i+1 (the cyclic node), and hence h 0 does not commute with ffi, a contradiction. Hence,
Thus, there exists a strictly decreasing infinite sequence of cyclic TFSs and therefore subsumption
is not well-founded. 2
To conclude this section, note that specification, which is the inverse relation to subsump-
tion, is not well-founded even when cyclic feature structures are ruled out. This fact can
easily be seen by considering the sequence of feature structures
f
f
f
f
f
f
f
f
f
A3

Figure

1: An infinite decreasing sequence of TFSs
of nodes, the first i of which are labeled t and the last - ?, and an f-arc leads from
every node to its successor. Clearly, and the sequence is infinite.
This is true whether or not appropriateness constraints are imposed on the feature structures
involved.
In the general case, then, given a feature structure A it might be possible to construct,
starting from A, both an infinite decreasing sequence of TFSs (by expanding cycles) and an
infinite increasing sequence (by adding paths).
Parsing
Parsing is the process of determining whether a given string belongs to the language defined
by a given grammar, and assigning a structure to the permissible strings. A large variety
of parsing algorithms exists for various classes of grammars (for a detailed treatment of the
theory of parsing with grammars that are based on feature structures, refer to (Shieber,
1992; Sikkel, 1993; Wintner and Francez, 1995b)). We define below a simple algorithm for
grammars that are based on TFSs, but it must be emphasized that the results presented in
this paper are independent of the particular algorithm; they hold for a wide range of different
algorithms.
To be able to represent complex linguistic information, such as phrase structure, the
notion of feature structures is usually extended. There are two different approaches for
representing phrase structure in feature structures: by adding special, designated features to
the FSs themselves; or by defining an extended notion of FSs. The first approach is employed
by HPSG: special features, such as DTRS (daughters), encode trees in TFSs as lists. This
makes it impossible to directly access a particular daughter. (Shieber, 1992) uses a variant
of this approach, where a denumerable set of special features, namely 0; are added to
encode the order of daughters in a tree. In a typed system such as ours, this method would
necessitate the addition of special types as well; in general, no bound can be placed on the
number of features and types necessary to state rules (see (Carpenter, 1992b, p. 194)).
We adopt below the other approach: a new notion of multi-rooted feature structures,
suggested by (Sikkel, 1993) and (Wintner and Francez, 1995b), is being used.
Definition 4.1 (Multi-rooted structures) A multi-rooted feature structure (MRS)
is a pair h -
is a finite, directed, labeled graph consisting of a set
Nodes of nodes and a partial function specifying the arcs, and -
Q is
an ordered (repetition-free) set of distinguished nodes in Q called roots. G is not necessarily
connected, but the union of all the nodes reachable from all the roots in -
Q is required to yield
exactly Q. The length of a MRS is the number of its roots, j -
Qj. - denotes the empty MRS
(where
is cyclic under the same conditions a TFS is. A
MRS is reentrant if it contains a node that can be reached either from two different roots
or through two different paths.
Meta-variables oe; ae range over MRSs, and ffi; Q; -
constituents. If
Q; Gi
is a MRS and -
q i is a root in -
naturally induces a feature structure A
is the set of nodes reachable from -
Thus oe can be viewed as an
ordered sequence hA necessarily disjoint) feature structures. We use the two
views of MRSs interchangeably.
Not only can nodes be shared by more than one element of the sequence; paths that start
in one root can reach a different root. In particular, cycles can involve more than one root.
Still, it is possible to define sub-structures of MRSs by considering only the sub-graph that
is accessible from a sub-sequence of the roots.
Definition 4.2 (Sub-structure) The sub-structure of induced by the
pair hi; ji and denoted oe i:::j , is hA use oe i for oe i:::i .
Definition 4.3 (Subsumption of multi-rooted structures) A MRS
Q; Gi subsumes
a MRS oe
(denoted by oe v oe 0
there exists a total
ffl for every root -
ffl for every q 2 Q, '(q) v '(h(q))
ffl for every q 2 Q and f 2 Feats, if ffi(q; f)# then h(ffi(q;
Many of the properties of TFSs are easily adaptable to MRSs. Let
q is the i-th root in -
-)#g. Then it is easy to show that if oe v ae then
every reentrancy in oe is a reentrancy in ae. Moreover, if oe ! ae (strictly)
then at least one of the three conditions listed in lemma 2.2 holds.
The well-foundedness result of the previous section are easily extended to MRSs as well.
and the same rank function
of TFSs can be used to show the well-foundedness of (acyclic) MRSs. The reverse direction
is immediate: in the presence of cycles, duplicate the example of the previous section k times
and an infinite decreasing sequence of MRSs of length k is obtained, for any k ? 0. For a
detailed discussion of the properties of MRSs, refer to (Wintner and Francez, 1995b).
Rules and grammars are defined over an additional parameter, a fixed, finite set Words
of words (in addition to the parameters Nodes, Feats and Types). The lexicon associates
with every word w a feature structure Cat(w), its category. 2 The categories are assumed to
be disjoint. The input for the parser, therefore, is a sequence of (disjoint) TFSs rather than
a string of words.
Definition 4.4 (Pre-terminals) Let defined iff
case it is the MRS hCat(w j ); Cat(w j+1
PTw (j;
2 For the sake of simplicity, we assume that lexical entries are not ambiguous. In the case of ambiguity,
Cat(w) is a set of TFSs. While the definitions become more cumbersome, all the results still obtain.
If a single word occurs more than once in the input (that is, w its category
is copied (with remaned nodes) more than once in PT .
Definition 4.5 (Grammars) A rule is an MRS of length greater than or equal to 1 with
a designated (first) element, the head of the rule. The rest of the elements form the rule's
body (which may be empty). A grammar G = (R; A s ) is a finite set of rules R and a start
A s that is a TFS.

Figure

2 depicts an example grammar (we use AVM notation for this rule; tags such as 1
denote reentrancy). The type hierarchy on which the grammar is based is omitted here.
Initial
phrase
s
Lexicon:
John her loves6 6 6 6 6 6 6 4
word
\Theta

AGR :4
agr
\Theta
3rd

\Theta
sg
sem
\Theta
john

word
\Theta
acc

AGR :4
agr
\Theta
3rd

\Theta
sg
sem
\Theta
she

word
\Theta

AGR :4
agr
\Theta
3rd

\Theta
sg
sem
\Theta
love

phrase
\Theta
s

sem
sign
\Theta
nom

sem
sign
\Theta

phrase
\Theta

sem
\Gamma!6 6 4
sign
\Theta

sign
\Theta
acc

sem

Figure

2: An example grammar
In what follows we define the notion of derivation (or rewriting) with respect to TFS-based
grammars. Informally, this relation (denoted ';') is defined over MRSs such that oe ; ae iff
ae can be obtained from oe by successive application of grammar rules. The reader is referred
to, e.g., (Sikkel, 1993; Shieber, Schabes, and Pereira, 1994; Wintner and Francez, 1995b) for
a detailed formulation of this concept for a variety of formalisms.
To define derivations we first define immediate derivation. Informally, two MRSs A and
are related by immediate derivation if there exists some grammar rule ae that licenses the
derivation. ae can license a derivation by some MRS R that it subsumes; the head of R must
be identified with some element i in A, and the body of R must be identified with a sub-structure
of B, starting from i. The parts of A prior to and following i remain intact in B.
Note that R might carry reentrancies from A to B: if a path - 2 leaving the i-th element of
A is reentrant with some path - 1 leaving the a-th element, and - 2 , starting from the head of
R, is reentrant with - 3 in some element b in R, then - 1 and - 3 are reentrant in B, starting
from the elements in B that correspond to a and b, respectively.
Definition 4.6 A MRS immediately derives a MRS
(denoted A ! B) iff there exist a rule ae 2 R of length n and a MRS R w ae, such that:
ffl R's head is identified with some element i of A: R
ffl R's body is identified with a sub-structure of B: R
ffl The first are identical: A
ffl The last k \Gamma i elements of A and B are identical: A
The reflexive transitive closure of '!', denoted '
!', is defined as follows: A
or if there exists A 0 such that A ! A 0 and A 0
A 00 .
Definition 4.7 A MRS A derives a MRS (denoted A ; B) iff there exist MRSs A
such that A v A 0 ,
Immediate derivation is based on the more traditional notion of substituting some symbol
which constitutes the head of some rule with the body of the rule, leaving the context intact.
However, as our rules are based on TFSs, the context of the "symbol" to be substituted might
be affected by the substitution. To this end we require identity, and not only unifiability, of
the contexts. MRSs related by derivations should be viewed as being "as specific as needed",
i.e., containing all the information that is added by the rule that licenses the derivation. This
is also the reason for the weaker conditions on the ';' relation: it allows an MRS A to derive
an MRS B if there is a sequence of immediate derivations that starts with a sepcification of
A and ends in a specification of B.

Figure

3 depicts a derivation of the string "John loves her" with respect to the example
grammar. The scope of reentrancy tags should be limited to one MRS, but we use the same
tags across different MRSs to emphasize the flow of information during derivation.6 6 6 6 6 6 6 6 6 6 6 6 4
phrase
\Theta
s

agr
\Theta
3rd

\Theta
sg
sem
\Theta
love

\Theta
john

\Theta
she
(1)
sign
\Theta
nom

agr
\Theta
3rd

\Theta
sg
sem
\Theta
john

sign
\Theta

sem
\Theta
love

(2)
word
\Theta
nom

agr
\Theta
3rd

\Theta
sg
sem
\Theta
john

word
\Theta

agr
\Theta
3rd

\Theta
sg
sem
\Theta
love

word
\Theta
acc

AGR :4
agr
\Theta
3rd

\Theta
sg
sem
\Theta
she

John loves her

Figure

3: A leftmost derivation
Definition 4.8 (Language) The language of a grammar G is
n)g.
The derivation example of figure 3 shows that the sentence "John loves her" is in the language
of the example grammar, since the derivation starts with a TFS that is more specific than
the initial symbol and ends in a specification of the lexical entries of the sentences' words.
Parsing is a computational process triggered by some input string of words
of length n - 0. For the following discussion we fix a particular grammar
particular input string w of length n. A state of the computation consists of a set of items.
Definition 4.9 (Items) An item is a tuple [i; oe; j; k], where oe is an MRS
joej. an item is active if k ! joej, otherwise it is complete. Items is the
collection of all items.
If [i; oe; j; k] is an item, oe 1:::k is said to span the input from position position j (the
parsing invariant below motivates this term). oe and k can be seen as a representation of
a dotted rule, or edge: during parsing all generated items are such that oe is (possibly more
specific than) some grammar rule. k is a position in oe, indicating the location of the dot.
The part of oe prior to the dot was already seen; the part following the dot is still expected.
When the entire body of oe is seen, the edge becomes complete.
A computation amounts to successively generating items; we assume that item generation
is done through a finite set of deterministic operations that create an item on the basis of
previously generated (zero or more) items. Also, if an item was generated on the basis of some
existing items, those items are not used again by the same operation. This assumption is
realized by an important class of parsing algorithms known as chart parsers. A computation
is terminating if and when no new items can be generated. A computation is successful if,
upon termination, a complete item that spans the entire input and contains the initial symbol
was generated: the final state of the computation should contain the item [0; oe; n; 1], where
A - A s and n is the input's length. Different algorithms assign different meanings to items,
and generate them in various orders (see, e.g., (Shieber, Schabes, and Pereira, 1994; Sikkel,
1993)). To be as general as possible, we only assume that the following invariant holds:
Parsing invariant In a computation triggered by w, if an item [i; oe; j; k] is generated then
One immediate consequence of the invariant is that for all the items [i; oe; j; k] generated when
parsing
A parsing algorithm is required to be correct:
Correctness A computation triggered by w is successful iff w 2 L(G).
Although (Shieber, 1992) uses a different notation than (Wintner and Francez, 1995b), this
property is proven by both.
5 Termination of parsing
It is well-known (see, e.g., (Pereira and Warren, 1983; Johnson, 1988)) that unification-based
grammar formalisms are Turing-equivalent, and therefore the parsing problem is undecidable
in the general case. However, for grammars that satisfy a certain restriction, termination of
the computation can be guaranteed. We make use of the well-foundedness of subsumption
(section to prove that parsing is terminating for off-line parsable grammars.
To assure efficient computation and avoid maintenance of redundant items, many parsing
algorithms employ a mechanism called subsumption check (see, e.g., (Shieber, 1992;
Sikkel, 1993)) to filter out certain generated items. Define a (partial) order over items:
. The subsumption
filter is realized by preserving an item x only if no item x 0 such that x 0 - x was generated
previously. Thus, for all items that span the same substring, only the most general one
is maintained. (Shieber, 1992; Wintner and Francez, 1995b) prove that by admitting the
subsumption check, the correctness of the computation is preserved.
Off-line parsability was introduced by (Kaplan and Bresnan, 1982) and was adopted
by (Pereira and Warren, 1983), according to which "A grammar is off-line parsable if its
context-free skeleton is not infinitely ambiguous". As (Johnson, 1988) points out, this restriction
(which he defines in slightly different terms) "ensures that the number of constituent
structures that have a given string as their yield is bounded by a computable function of the
length of that string". The problem with this definition is demonstrated by (Haas, 1989):
"Not every natural unification grammar has a context-free backbone".
A context-free backbone is inherent in LFG, due to the separation of c-structure from f-structure
and the explicit demand that the c-structure be context-free. However, this notion
is not well-defined in HPSG, where phrase structure is encoded within feature structures
(indeed, HPSG itself is not well-defined in the formal language sense). Such a backbone
is certainly missing in Categorial Grammar, as there might be infinitely many categories.
(Shieber, 1992) generalizes the concept of off-line parsability but doesn't prove that parsing
with off-line parsable grammars is terminating. We use an adaptation of his definition below
and provide a proof.
Definition 5.1 (Finite-range decreasing functions) A total function F : D ! D, where
D is a partially-ordered set, is finite-range decreasing (FRD) iff the range of F is finite
and for every d 2 D;F (d) - d.
Definition 5.2 (Strong off-line parsability) A grammar is strongly off-line parsable
iff there exists an FRD-function F from MRSs to MRSs (partially ordered by subsumption)
such that for every string w and different MRSs oe; ae such that oe ; ae, if oe ; PTw (i
Strong off-line parsability guarantees that any particular sub-string of the input can only be
spanned by a finite number of MRSs: if a grammar is strongly off-line parsable, there can not
exist an infinite set S of MRSs, such that for some
S. If such a set existed, F would have mapped its elements to the set fF
This set is infinite since S is infinite and F doesn't map two different items to the same
image, and thus the finite range assumption on F is contradicted.
As (Shieber, 1992) points out, "there are non-off-line-parsable grammars for which termination
holds". We use below a more general notion of this restriction: we require that F
produce a different output on oe and ae only if they are incomparable with respect to subsump-
tion. We thereby extend the class of grammars for which parsing is guaranteed to terminate
(although there still remain decidable grammars for which even the weaker restriction doesn't
hold).
Definition 5.3 (Weak off-line parsability) A grammar G is weakly off-line parsable
iff there exists an FRD-function F from MRSs to MRSs (partially ordered by subsumption)
such that for every string w and different MRSs oe; ae such that oe ; ae, if oe ; PTw (i
ae and ae 6v oe, then F (oe) 6= F (ae).
Clearly, strong off-line parsability implies weak off-line parsability. However, as we show
below, the inverse implication does not hold.
We now prove that weakly off-line parsable grammars guarantee termination of parsing
in the presence of acyclic MRSs. We prove that if these conditions hold, only a finite number
of different items can be generated during a computation. The main idea is the following:
if an infinite number of different items were generated, then an infinite number of different
items must span the same sub-string of the input (since the input is fixed and finite). By
the parsing invariant, this would mean that an infinite number of MRSs derive the same
sub-string of the input. This, in turn, contradicts the weak off-line parsability constraint.
Theorem 5.4 If G is weakly off-line parsable and MRSs are acyclic then every computation
terminates.
Proof: Fix a computation triggered by w of length n. By the consequence of the parsing
invariant, the indices that determine the span of items are limited (0 - n), as are
the dot positions (0 ! k - joej). It remains to show that for every selection of i, j and k,
only a finite number of MRSs are generated. Let be a generated item. Suppose
another item is generated where only the MRS is different: x
x 0 will not be preserved because of the subsumption test. If ae v oe, x can be replaced by
x 0 . There is only a finite number of such replacements, since subsumption is well-founded for
acyclic MRSs. Now suppose oe 6v ae and ae 6v oe. By the parsing invariant, oe 1:::k ; PTw (i+1;
and ae 1:::k ; PTw (i
the range of F is finite, there are only finitely many items with equal span that are pairwise
incomparable. Since only a finite number of items can be generated and the computation
uses a finite number of operations, every computation ends within a finite number of steps.The above proof relies on the well-foundedness of subsumption, and indeed termination
of parsing is not guaranteed by weak off-line parsability for grammars based on cyclic TFSs.
Obviously, cycles can occur during unification even if the unificands are acyclic. However,
it is possible (albeit costly, from a practical point of view) to spot them during parsing.
Indeed, many implementations of logic programming languages, as well as of unification-based
grammars (e.g., ALE (Carpenter, 1992a)) do not check for cycles. If cyclic TFSs are
allowed, the more strict notion of strong off-line parsability is needed. Under the strong
condition the above proof is applicable for the case of non-well-founded subsumption as well.
To exemplify the difference between strong and weak off-line parsability, consider a grammar
G that contains the following single rule:6 4
and the single lexical entry, w 1 , whose category is:
This lexical entry can be derived by an infinite number of TFSs:
It is easy to see that no FRD-function can distinguish (in pairs) among these TFSs, and
hence the grammar is not strongly off-line parsable. The grammar is, however, weakly off-line
parsable: since the TFSs that derive each lexical entry form a subsumption chain, the
antecedent of the implication in the definition for weak off-line parsability never holds; even
trivial functions such as the function that returns the empty TFS for every input are appropriate
FRD-functions. Thus parsing is guaranteed to terminate with this grammar.
It might be claimed that the example rule is not a part of any grammar for a natural
language. It is unclear whether the distinction between weak and strong off-line parsability
is relevant when "natural" grammars are concerned. Still, it is important when the formal,
mathematical and computational properties of grammars are concerned. We believe that
a better understanding of formal properties leads to a better understanding of "natural"
grammars as well. Furthermore, what might be seem un-natural today can be common
practice in the future.

Acknowledgments

This work is supported by a grant from the Israeli Ministry of Science: "Programming Languages
Induced Computational Linguistics". The work of the second author was also partially
supported by the Fund for the Promotion of Research in the Technion. We wish to thank
the anonymous referees for their enlightening comments.



--R


The Logic of Typed Feature Structures.
A parsing algorithm for unification grammar.
Categorial Grammar

Lexical functional grammar: A formal system for grammatical representation.
A logic for partially specified data struc- tures
Parsing as deduction.



Parsing Schemata.
An abstract machine for typed feature struc- tures
Parsing with typed feature structures.
--TR

--CTR
Efrat Jaeger , Nissim Francez , Shuly Wintner, Unification Grammars and Off-Line Parsability, Journal of Logic, Language and Information, v.14 n.2, p.199-234, March     2005
Shuly Wintner, Compositional semantics for linguistic formalisms, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.96-103, June 20-26, 1999, College Park, Maryland
parsing;computational linguistics;feature structures;unification