{'fraction_non_alphanumeric': 0.03814703533259803, 'fraction_numerical': 0.005971171034115544, 'mean_word_length': 4.471077819392426, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Decidability and undecidability in stand-alone feature logics

This paper investigates the complexity of the satisfiability problem for feature logics strong enough to code entire grammars unaided. We show that feature logics capable of both enforcing re-entrancy and stating linguistic generalisations will have undecidable satisfiability problems even when most Boolean expressivity has been discarded. We exhibit a decidable fragment, but the restrictions imposed to ensure decidability render it unfit for stand-alone use. The import of these results is discussed, and we conclude that there is a need for feature logics that are less homogeneous in their treatment of linguistic structure.


Introduction
This paper investigates decidability and undecidability in stand-alone feature logics, that is, feature logics strong enough to express entire grammars without the assistance of a phrase-structure backbone. Our results are predominately negative and seem applicable to most existing stand-alone formalisms. We strengthen a result of [Blackburn andSpaan 1991, 1992] to show that the ability to express re-entraney and the ability to express generalisations about feature structures interact in ways that lead to undecidability even if most Boolean expressivity has been dropped from the logic. Even our positive results have a negative flavour. We exhibit a decidable fragment, but the restrictions imposed to attain decid-ability render it incapable of encoding interesting grammars unaided.
But what is the import of such results? This is the question we turn to in the last section of the paper. Basically, we regard such results as a sign that existing feature logics treat linguistic structure too homogeneously. What is needed are feature logics which are more sensitive to the fine structure of linguistic theorising.
The paper is relatively self contained, nonetheless the reader may find it helpful to have [Kasper andRounds 1986, 1990] and [Blackburn andSpaan 1991, 1992] to hand.

Preliminaries
Feature logics are abstractions from the unification based formalisms of computational linguistics. Originally feature logics embodied just one component of unification based formalisms. Early unification formalisms such as GPSG [Gazdar et al. 1985] and LFG [Kaplan and Bresnan 1982] have important phrase structure components in addition to their feature passing mechanisms, and the study of feature logic was originally intended to throw light only on the latter. These early unification formMisms are thus highly heterogeneous: they are architectures with roots in both formal language theory and logic.
In recent years this picture has changed. For example, in HPSG [Pollard and Sag 1987] the feature machinery has largely displaced the phrase structure component. Indeed in HPSG the residue of the phrase structure component is coded up as part of the feature system. Logic has swallowed formal language theory, and in effect the entire HPSG formal-ism is a powerful feature logic, a stand-alone formalism, capable of encoding complex grammars without the help of any other component. 1 In this paper we are going to investigate the computational complexity of the satisfiability problem for such stand-alone feature logics. This is an important problem to investigate. Natural language grammars are expressed as logical theories in stand-alone formalisms, and sentences are represented as wffs. This means that the problem of deciding whether or not a sentence is grammatical reduces to the problem of building a model of the sentence's logical representation that conforms to all the constraints imposed by the logical encoding of the grammar. In short, the complexity of the satisfiability problem is essentially the worst case complexity of the recognition problem for grammars expressed in the stand-alone formalism.
We will tackle this issue by investigating the complexity of the satisfiability problem for one particular stand-alone formalism, namely L KRo. This is the language of Kasper Rounds logic augmented with the strict implication operator. L KRm possesses two of the most fundamental properties of stand-alone formalisms: the ability to express re-entrancy, and the ability to express generalisations about feature structures. It is important to note that L KR~ is actually a fairly minimal language with these properties; many feature logics can express a lot more besides (for example, set values), thus the negative results for L KR=~ we present are rather strong: they extend straightforwardly to richer formalisms.
So let's begin by defining L KR~. By a signature (£, S) is meant a pair of non-empty sets L: and S, the set of arc labels and the set of sorts respectively. Syntactically, the language L KR=~ (of signature (£:, S)) contains the following items: an S indexed collection of propositional symbols (or sort symbols); all the standard Boolean operators; 2 an £ indexed collection of distinct unary modalities (that is, features); a binary modality ==~; and two special symbols 0 and ,~. We use ~., to make path equations: given any nonempty sequences A and B consisting of only unary modalities and O, then A ~ B is a path equation.
1 See [Johnson 1992] for further discussion of the distinction between stand-alone formalisms and formalisms with a phrase structure backbone.
2That is, we have the symbols True (constant true), False (constant false), ~ (negation), v (disjunction), A (conjunction), --* (material implication) and 4--* (material equivalence). For the purposes of the present paper it is sensible to assume that all these operators are primitives, as in general we will be working with various subsets of the full language and it would be tedious to have to pay attention to trivial issues involving the interdefinability of the Boolean operators in these weaker fragments.
Intuitively A ~ B says that making the sequence of feature transitions encoded by A leads to the same node as making the transition sequence coded by B. The symbol 0 is a name for the null transition. The strict implication operator =~ will enable us to express generalisations about feature structures.
We make the wffs of L KR~ as follows. First, all propositional symbols, all path equations and True and False are wffs. Second, if ¢ and ¢ are wits then so are all Boolean combinations of ¢ and ¢~ so is (1)¢ (for alll E £) and so is ¢ =~ ¢. Third, nothing else is a wff. If a wff of L KR:* does not contain any occurrences of ==~ then we say it is an L KR wff. Apart from trivial notational changes, the negation free fragment of L KR is the language defined and studied by Kasper and Rounds. 3 That is, the L KR wffs are essentially a way of writing the familiar Attribute Value Matrices (AVMs) in linear format. For example, the following L KR wff: is essentially the following AVM:

CASE nora or gen or acc
To interpret L KRo we use feature structures M of signature (/~,S). A feature structure is a triple (W, {Rt}tez:, V), where W is a non-empty set (the set of nodes); each Rz is a binary relation on W that is also a partial function; and V (the valuation) is a function which assigns each propositional symbol p E S a subset of W. Note that as we have defned them features structures are merely multimodal Kripke models, 4 and we often refer to feature structures as models in what follows. Now for the satisfaction definition. As the symbol 0 is to act as a name for the null transition, in what follows we shall assume without loss of generality that 0 ¢ £, and we will denote the identity relation on any set of nodes W by R0. This convention somewhat simplifies the statement of the satisfaction 3Computer scientists may have met L KR in another guise. The language of Kasper Rounds logic is a fragment of (deterministic) Propositional Dynamic Logic (PDL) with intel~ section (see [Harel 1984]). An L lea path equation A ,~ B is written as (An B) True in PDL with intersection. definition:
The key things to note about this language is that it has both the ability to express re-entrancy (the Kasper Rounds path equality ~ achieves this) and the ability to express generalisations about feature structures (note that ¢ ::~ ¢ means that at every node where ¢ is true, ~b must also be true). Thus L KR~ can certainly express many of the conditions we might want to impose on feature structures. For instance, we might want to impose a sort hierarchy. As a simple example, given sorts list and nelist (nonempty list) we might wish to insist that every node of sort nelist is also of sort list. The wff nelist ~ list forces this. As a second example, we might want to insist that any node from which it is possible to make a CONSTITUENT-STRUCTURE transition must be of sort phrasal. That is, if a node has constituent structure, it is a phrasal node. The wff (CONSTITUENT-STRUCTURE) True ~ phrasal forces this. Indeed quite complex demands can be imposed using L KR. For example the following wff embodies the essence of the constraint known as the head feature convention in HPSG:

phrasal ~ (HEAD) ~,~ (HEAD-DTR)(HEAD).
This wff says that at any node of sort phrasal in a feature structure, it is possible to make a ilEAl) transition and it is also possible to make a HEAD-DTR transition followed by a HEAD transition, and furthermore both transition sequences lead to the same node. In view of such examples it doesn't seem Wholly unrealistic to claim that L KR has the kind of expressive power a stand-alone feature logic needs.
However L TM has crossed a significant complexity boundary: it has an undecidable satisfiability problem. This was proved in [Blackburn andSpaan 1991, 1992] using a tiling argument, s Now, the result for the full L t':n=~ language is not particularly surprising (undecidability results for related feature logics, can be found in the literature; see [Carpenter 1992] for discussion) but it does lead to an important question: what can be salvaged? To put it another way, are there decidable fragments of L KR that are capable of functioning as stand-alone feature logics? The pages that follow explore this question and yield a largely negative response.

Decidability
To begin our search for decidable fragments we will take our cue from Kasper and Rounds' original work. Kasper and Rounds' system was negation free, so the first question to ask is: what happens if we simply remove negation from L KR:~? Of course, if this is all we do we trivialise the satisfiability problem: it is immediate by induction on the structure of negation free wffs ¢, that every negation free L KR~ wff is satisfied in the following model: M = ({w}, {Rt}tec, V) where Rz = {(w,w)} for all/E/~, and Y(p) = {w} for all propositional variables p. So we have regained decidability, but in a very uninteresting way. Now, what made the results of Kasper and Rounds interesting was that not only did they consider the negation free fragment (of LKR), they also imposed certain semantic restrictions. Only extensional models without constant-constant or constant-compound clashes were considered. 6 Will imposing any (or all) of these restrictions make it easier to find decidable fragments of L KR~ ? In fact demanding extensionality (that is, working only with models in which each atomic symbol is true at at most one node), does make it easy to find a decidable fragment.
The fragment is the following. We consider wffs of the following form: Here ¢ is a metavariable over L Kn wffs (that is, ¢ contains no occurrences of =¢,); the ai (1 < i < n) SThese papers take the universal modality [] as primitive rather that =¢,, as it is somewhat easier to work with unary modalities. In the presence of full Boolean expressivity I:3 and :=~ axe interdefmable: Elf is True :=~ ¢, and ::~ is 1:3(¢ --. ~b).
However in what follows we will work with fragments without enough Boolean expressivity to interdefine these operators. As :¢, is the operator we are really interested in we have chosen it as our primitive here. SAs Kasper and Rounds showed, introducing this limited form of negation failure results in an NP complete satisfiability problem.
are metavariables over combinations of sort symbols containing only V and A as logical operators; and the ai (1 < i < n) are metavariable over L KR wits.
Note the general form of the wffs of this fragment. We have an L KR wff ¢ conjoined with n general constraints o~i :2z tq. 7 The ¢ can be thought of as the AVM associated with some particular natural language sentence, while the wffs of the form c~i ::~ ~i can be thought of as encoding the generalisations embodied in our grammatical theory. Looking for a satisfying model for a wff from this fragment is thus like asking whether the analysis of some particular string of symbols is compatible with a grammar.
The proof that this fragment has a decidable satisfiability problem is straightforward. We're going to show that given any wff@ belonging to this fragment, there is an upper bound on the size of the models that need to be inspected to determine whether or not (I) is satisfiable. The fact that such an upper bound exists is a direct consequence of three lemmas which we will now prove.
The first lemma we need is extremely obvious, but will play a vital role.

Lemma 3.1 Let a be any wff containing no logical connectives apart from V and A. Then in any extensional model, c~ is satisfied at at most m nodes, where m is the number of distinct sort symbols in a.
Proof: By induction on the construction of a.
[] The importance of this lemma is that it gives us an upper bound on the number of nodes at which the antecedents ai of the constraints permitted in our fragment can be satisfied.
Next we need a similar result for the L KR wffs of the fragment; that is, for the ¢ and the consequents ~i of the constraints. As the next two lemmas establish, given any L KR wff C which is satisfiable at a node w in some model M, we can always manufacture a very small model MInodes(C , w) which also satisfies 4. How we go about defining MInodes(C, w) is suggested by the following observation: when evaluating a formula in some model, only certain of the model's nodes are relevant to the truth or falsity of the wff; all the irrelevant nodes can be thrown away. What the following two lemmas essentially tell us is that we can manufacture the small models we need by discarding nodes. The nodes that are relevant when evaluating an L KR wff C at a node w in a model M are the nodes selected by the function nodes : WFF x W , Pow(W) that satisfies the following conditions: ;'In what follows we refer to the cq as the antecedents of the constraints, and the ai as the consequents.

nodes((i)¢, ) = {w} u nodes(C,
One aspect of the definition of nodes may be bothering the reader: there is no clause for the path equations. In fact to give such a clause is rather messy, and it seems better to proceed as follows. Given a wff C of L Ks we define C* to be the result of replacing

.(lk)Tr e ^ (tl) • • • (i',) Tr e.
Clearly ¢ is satisfiable at any node in any model iff 4" is (all we've done is make the node existence demands encoded in the path equalities explicit). The usefulness of this transformation is simply that the two new conjuncts make available to the simple version of nodes defined above all the information hidden in the path equations. From now on we'll assume that all the L KR wffs we work with have been transformed in this fashion.
With these preliminaries out of the way we are ready to proceed. Given a model M, an L KR wff ¢ and a node w we form Mlnodes(C , w) in the obvious way: the nodes of the model are nodes(C, w), and the relations and valuation are the restriction of those of M to this subset. As the following simple lemma shows, nodes indeed picks out the correct nodes:

M ~ C[w] iff Mlnodes(¢, w) ~ ¢[u,].
Proof: By induction on the structure of ¢,. (Note that it follows from the definition of nodes that w E nodes (C,w). Once this is observed the induction is The selection lemma is a completely general fact about modal languages. It doesn't depend on any special assumptions made in this paper, and in particular it doesn't make any use of the fact that we are only working with models in which each of the Rt is a partial function. Once this additional fact is taken into account, however, we see that M[nodes(~,, w)is pleasingly small: there can only be one more node in M[nodes (¢, w) than there are occurrences of modalities in ¢. That is, we have:

Lemma 3.3 (Size Lemma) Let W be an L KR wff, and let mod(W) be the number of occurrences of modalities in W. Then for all models M and all nodes w in M we have that Inodes(W,w)\{w}l < ,nod(W).
Proof: By induction on the structure of ~b. Cl We now have all the pieces we need to establish the decidability result. Using these lemmas we can show that given any wff (I) of our fragment it is possible to place an upper bound on the size of models that need to be checked to determine whether or not (I) is satisfiable. So, suppose (b is a wff of the form to make a smaller model satisfying (I). The problem is that while this model certainly satisfies ~, in the course of selecting all the needed nodes we may be forced to select a node that verifies an antecedent ai of one of the general constraints, but we have no guarantee that we have selected all the nodes needed to make the matching consequent t¢i true.
But this is easy to fix. We must not only form Mlnodes(e~, w), but in addition, for all i (1 < i < n) we must form Mlnodes(cq ^ ai, s), where s ranges over all the nodes in M that satisfy c~i. More precisely, we define a new model M' by taking as nodes all the nodes in all these models (that is, we take the union of all the nodes in all these models) and we define the M' relations and valuation to be the restriction of the relations and valuation in M to this subset.
The new model M' has two nice properties. Firstly, it is clear that it makes ~ true at w and moreover, whenever it makes one of the ai true it makes the corresponding ~i true also. (This follows because of our choice of the nodes of M'; essentially we're making multiple use of the selection lemma here.) Secondly, it is clear that M' is finite, for its nodes were obtained as a finite union of finite sets. Indeed by making use of lemma 3.1 and the size lemma we can give an upper bound on the size of M' in terms of the number of symbols in (I). (This is just a matter of counting the number of general constraints in (I), the number of distinct propositional variables in the c~i, and the number of modal operators in the and tzi; we leave the details to the reader.) Thus the decidability result follows: given a wff if) of our fragment, bounded search through finite models suffices to determine whether or not (I) is satisfiable.
Alas, this is not a very powerful result. The fragment simply is not expressive enough to function as a stand-alone formalism. Its Achilles heel lies in the strong condition imposed on the ai. There are two problems. First, because the ai cannot contain occurrences of features or path equations, many important constraints that stand-alone feature might have to impose cannot be expressed. Second, it is far from clear that the restriction to extensional models is realistic for stand alone formalisms. Certainly if we were trying to capture the leading ideas of HPSG it would not be; the freedom to decorate different nodes with the same sortal information plays an important role in HPSG.
Can some of the restrictions on the ai be dropped? As the proof of the result shows, there is no obvious way to achieve this: as soon as we allow features or path equations in the (~i, the assumption of extensionality no longer helps us find an upper bound on the number of satisfying nodes, and the proof no longer goes through. Essentially what is needed is a way of strengthening lemma 3.1, but it is hard to find a useful way of doing this. Even imposing an acyclicity assumption on our models doesn't seem to help. As the results of the next section show, this is no accident. The combination of ~ and =* is intrinsically dangerous.

Undecidability
The starting point for this section is the undecidability result for the full L KR=~ language (see [Blackburn andSpaan 1991, 1992]) which was proved using reduction from a certain undecidable tiling problem.
We're going to strengthen this undecidability result, and we're going to do so by using further tiling arguments. As the use of tiling arguments seem to be something of a novelty in the computational linguistics literature, we include a little background discussion of the method.
Tiling arguments are a well known proof technique in computer science for establishing computability and complexity results. (In fact, tiling arguments are used to introduce the basic concepts of complexity, decidability and undecidability in [Lewis and Papadimitriou 1981], one of the standard introductions to theoretical computer science.) They are also a popular method for analysing the complexity of logics; both [Harel 1983] and[Hard 1986] are excellent guides to the versatility of the method for this application.
One of the most attractive aspects of tiling problems is that they are extremely simple to visualise. A tile T is just a 1 × 1 square, fixed in orientation, that has coloured edges right(T), left(T), up(T), and down(T) taken from some denumerable set. A tiling problem takes the following form: given a finite set 7" of tile types, can we cover a certain part of Z × Z (Z denotes the integers) using only tiles of this type, in such a way that adjacent tiles have the same colour on the common edge, and such that the tiling obeys certain constraints? For example, consider the following problem. Suppose 7-consists of the following four types of tile: Can an 8 by 4 rectangle be tiled with the fourth type of tile placed in the left hand corner? The answer is 'yes' --but we'll leave it to the reader to work out how to do it.
There exist complete tiling problems for many complexity classes. In the proof that follows we make use of a certain II ° complete tiling problem, namely the problem of tiling the entire positive quadrant of the plane, that is, the problem of tiling N × N where N is the set of natural numbers.
We begin with the following remark: by inspection of the undecidability proof for L KR~ in [Blackburn andSpaan 1991, 1992], it is immediate that we still have undecidability if we restrict the language to formulas that consist of a conjunction of formulas of the form ¢1 ::~ ~b2, where ¢1 and ¢2 are L KR formulas with negations applied to atoms only, and ¢2 is satisfiable. (The stipulation that ¢2 must be satisfiable prevents it from playing the role of False and thus smuggling in illicit negations.) Call this language L-. Let's see if we can strengthen this result further.
So, suppose we look at L-formulas with V as the only binary boolean connective in ¢1 and ¢2. In this case, we show that the corresponding satisfiability problem is still undecidable by constructing another reduction from N × N tiling.
Let 7-= {7"1,...,Tk} be a set of tiles. We construct a formula ¢ such that: First of all we will ensure that, if ¢ is satisfiable in a model M, then M contains a gridlike structure. The nodes of M (henceforth W), play the role of points in a grid, R, is the right successor relation, and Ru is the upward successor relation. Define: ¢9ri d = (TrUe ~ (,)(U) ~,~ (u)(r)).
Next we must tile the model. To do this we use propositional variables tl,.-., tk, such that ti is true at some node w, iff tile Ti is placed at w. To force a proper tiling, we need to satisfy the following three requirements: 1. There is exactly one tile placed at each node.

up(Ti)# down(T D
Let ¢ be earid A ¢1 A ¢2 A ¢3. It is not too difficult to prove that ¢ is satisfiable iff T tiles N x N, which implies that the satisfiability problem for our fragment of L-is undecidable. Are Are even weaker fragments undecidable? Yes: we can ensure that V occurs at most once in each clause. In fact we only have to rewrite part of ¢1 (namely, k True =~ Vi=l ti), for this is the only place in ¢ where V occurs. We use new variables b2 ..... bk-1 for this purpose and we ensure that bi is true iff [j is true for some j _< i. We do this as follows: (b2 =~ t~ vt2) A

(True =~ bk-1 V tk)
Clearly this has the desired effect.

Discussion
The results of this investigation are easy to summarise: the ability to express both re-entrancy and generalisations about feature structures lead to algorithmically unsolvable satisfiability problems even if most Boolean expressivity is dropped. What are the implications of these results? Stand-alone feature formalisms offer (elegant) expressive power in a way that is compatible with the lexically driven nature of much current linguistic theorising. One of their disadvantages (at least in their current incarnations) is that they tend to hide computationally useful information. For example, as [Johnson 1992] points out, it is difficult even to formulate such demands as offiine parsability for existing stand-alone formalisms; the configurational information required is difficult to isolate. The problem is that stand-alone formalisms tend to be too homogeneous. It is certainly elegant to treat information concerning complex categories and configurational information simply as 'features'; but unless this is done sensitively it runs the risk of 'reducing' a computationally easy problem to an uncomputable one.
Now, much current work on feature logic can be seen as attempts to overcome the computational bluntness of stand-alone formalisms by making visible computationally useful structure. For example, recent work on typed feature structures (see [Carpenter 1992]) explicitly introduces the type inheritance structure into the semantics; whereas in [Blackburn et al. 1993] composite entities consisting of trees fibered across feature structures are constrained using two distinct 'layers' of modal language. What is common to both these examples is the recognition that linguistic theories typically have subtle internal architectures. Only when feature logics become far more sensitive to the fine grain of linguistic architectures will it become realistic to hope for general decidability results.