Arbeitspapiere des SFB 340

Bericht Nr. 00, Xxxx 19??

MONADIC SECOND-ORDER LOGIC, TREE AUTOMATA AND CONSTRAINT LOGIC PROGRAMMING

FRANK MORAWIETZ

Abstract. In this paper we present a first step toward the development of a constraint logic programming (CLP) language R(MSO) based on monadic second-order (MSO) logic. We apply the scheme proposed by Höhfeld and Smolka (1988) to obtain a relational extension of MSO logic with a corresponding sound and complete operational semantics. The solutions to constraints expressed in monadic second-order logic are represented by tree automata recognizing the variable assignments satisfying the formulas. Since this allows a compact and efficient representation of constraints, we use the tree automata as a constraint store and MSO theorem provers as constraint solvers for the CLP interpreter. Building on the detailed investigation of MSO logic as a tree description language in the Principles and Parameter (P&P) paradigm in Rogers (To appear), we present as motivation and applications details from the realm of P&P-based parsing.

1. Introduction

Model-theoretic techniques are the underlying principle of a number of grammar formalisms for natural language. In this paper, we focus on the use of monadic second-order (MSO) logic for formalizations of Principle and Parameter (P&P) approaches in the Government and Binding tradition (Chomsky, 1981). The suitability of this formalism for P&P grammars has been shown in a recent monograph by Rogers (To appear).

The research presented in this report was sponsored by Teilprojekt A8 of the SFB 340 of the DFG. I want to thank Tom Cornell, Laura Kallmeyer, Hans-Peter Kolb, Uwe Mönnich, Stefan Riezler and Jim Rogers for helpful discussion. Needless to say, all errors and infelicities that remain are my own.

ISSN 0947-6954/?? \begin{matrix}c \\ ◯ \end{matrix} 19?? Der Autor

Constraint-based formalisms characterize objects with logical description languages declaratively., i.e., without the specification of how to generate admissible structures. To be able to use them in applications, computational linguistics has to provide a connection between model theory and theorem proving on the one hand, and natural language processing on the other. We can bridge the gap between the two by exploiting the connection between constraints in MSO logic on trees and tree automata.

Our purpose in this paper is twofold. Firstly we discuss the operational interpretations of MSO logic. Since the solutions to constraints expressed in MSO logic are represented by tree automata which recognize the assignment trees satisfying the formulas, we can directly use the automata as the operational interpretation of our formalism; the aim of the paper being the exploitation of Rogers’ formalization in relation to tree automata. And secondly we discuss possible extensions of MSO logic via the addition of inductive definitions with respect to both the operational interpretation and the generative capacity, since MSO logic characterizes only the context-free languages, but natural languages are generally believed to be higher in the Chomsky hierarchy.

More concretely, since inductive definitions can be seen as special cases of constraint logic programming (CLP) clauses and the specification of a CLP interpreter re-introduces the operational concept of derivations, we propose the embedding of MSO logic into the constraint logic programming scheme of Höhfeld and Smolka (1988) to define an even more powerful and flexible language. This CLP language allows a stepwise compilation of tree automata guided by appropriate programs and dependent on an initial goal.

The paper is organized as follows. In the first section we review the results on MSO logic and tree automata briefly discussing advantages and disadvantages of the formalism. The next section is centered on constraint logic programming. We apply the Höhfeld and Smolka scheme to derive a relational extension, discuss its properties and present some examples. In the last section, we argue for the usefulness of the approach with examples from P&P-based parsing.

2. Trees, Tree Automata, and MSO Logic

2.1. Trees and Tree Automata. For convenience, we present short definitions of (binary) trees and tree automata here. A proper introduction to tree automata can be found in Gécseg and Steinby (1997).

We actually give two definitions here, suitable for different aspects of the following discussions. Assume an alphabet Σ = Σ_{0}∪Σ_{2} with Σ_{0} = {λ} 𝔄 = ⟨{a_{0}, a_{1}}, {A, B}, a_{0}, {a_{0}}, α⟩

α(a_{0}, a_{0}, A) = a_{0} α(a_{0}, a_{1}, A) = a_{1} α(a_{1}, a_{0}, A) = a_{1} α(a_{1}, a_{1}, A) = a_{1} α(a_{0}, a_{0}, B) = a_{1} α(a_{0}, a_{1}, B) = a_{1} α(a_{1}, a_{0}, B) = a_{1} α(a_{1}, a_{1}, B) = a_{1}

Figure 1. A simple tree automaton

and i the arity of the elements in Σ_{i}. The set of binary trees T_{Σ} over Σ is the set of terms built by letting λ denote the empty tree and by letting σ(t_{1}, t_{2}), σ ∈ Σ_{2}, t_{1}, t_{2} ∈ T_{Σ} denote the tree with label σ and subtrees t_{1}, t_{2}. This algebraic perspective facilitates the automata theory. In the model theory underlying MSO logics it is more convenient to assume a tree t to be a function from the addresses of a binary tree domain T_{2} to labels Σ. Intuitively a tree domain is a way to canonically label the nodes in an infinite tree. More formally, a tree domain T is a subset of strings over a linearly ordered set which is closed under prefix and left sister. T_{2} results from an alphabet of strings over, for example, \{\underline{0}, \underline{1}\}.

A deterministic (bottom-up) tree automaton 𝔄 on binary trees is a tuple ⟨A, Σ, a_{0}, F, α⟩ with A the (finite) set of states, Σ as defined above, a_{0} ∈ A the initial state, F ⊆ A the final states and α : (A × A × Σ_{2}) → A the transition function. We omit the transitions on Σ_{0} here and in the following. Instead, we just designate the initial state. Formally we would need a transition α(λ) = a_{0}. We can extend the transition function homomorphically to trees by inductively defining h_{α}(λ) = a_{0} and h_{α}(σ(t_{1}, t_{2})) = α(h_{α}(t_{1}), h_{α}(t_{2}), σ), t_{1}, t_{2} ∈ T_{Σ}, σ ∈ Σ_{2}. An automaton 𝔄 accepts a tree t ∈ T_{Σ} iff h_{α}(t) ∈ F. The language recognized by 𝔄 is denoted by T (𝔄) = {t | h_{α}(t) ∈ F }. Emptiness of the language T (𝔄) is decidable by a fixpoint construction on the reachable states. Intuitively, the automaton creeps up the tree from the frontier to the root using the labels as symbols for the transitions and assigning a state to each subtree. Recognition of a given tree t is just trivially achieved by running an automaton on an input tree, i.e., computing h_{α}(t).

As an example, the automaton in Fig. 1 recognizes trees from an alphabet with Σ_{2} = {A}. This admittedly very simple tree automaton recognizes all binary trees whose interior nodes are labeled with A by staying in the initial and, at the same time, final state a_{0}. As soon as we encounter a node labeled B, we go into a sink state (a_{1}). We will eliminate the transitions to the sink state in the remainder of the paper since they do not contribute knowledge on acceptable structures.

Bottom-up tree automata are closed under complementation, conjunction, disjunction, projection and cylindrification of alphabets, determinization and minimization. Most of the constructions are adaptions from the corresponding ones on finite state automata. We will use the constructions during the compilation from formulas to automata to parallel connectives and quantifiers in MSO formulas. More details on both the specification and implementation of tree automata and their constructions can be found in Morawietz and Cornell (1997) and Klarlund (1998).

2.2. MSO Logic on Trees. We choose MSO logic on trees since it is decidable, flexible and has a direct operational interpretation via its decidability proof. Both theorem proving and inductive definitions are well defined. Furthermore, MSO logic has a descriptive complexity result: it characterizes exactly the trees whose yields are context-free languages.

An MSO logical language is like predicate logic extended with variables ranging over sets and quantifiers ranging over these MSO variables. More specifically, it has a syntax of both first and (monadic) second-order quantification, all the usual logical connectives, first-order variables ranging over nodes and a (countably infinite) set of monadic second-order variables ranging over finite sets. Terms and formulas are built as usual.

The techniques we are using come originally from an old result in logic, namely that the weak MSO theory of two successor functions (WS2S) is decidable (Thatcher and Wright, 1968; Doner, 1970). A “weak” secondorder theory is one in which the set variables are allowed to range only over finite sets. There is a more powerful result available: it has been shown by Rabin (1969) that the strong second-order theory (variables range over infinite sets) of even countably many successor functions is decidable. However, in our linguistic applications we need only to quantify over finite sets, so the weaker theory is enough, and the techniques correspondingly simpler. In fact, since we are interested in using the technique of the decidability proof for natural language processing and the proof works by showing a correspondence between formulas in the language of WS2S and tree automata and there does not exist an efficient minimization algorithm for the corresponding class of Rabin automata on infinite sets, using strong SnS is not an option open to us. All of these are generalizations to trees of a result on strings originally due to Büchi (1960). The applications we mention here could be adapted to strings with finite-state automata replacing tree automata.

Informally, we create a tree description logic by fixing the domain of the interpretation to “trees” and adding binary relations to the syntax which will be interpreted as the successor functions. So, for the structure of WS2S, we are going to assume a tree domain with the extension of (at least) the two successor relations. These correspond intuitively to the relations of left and right daughter and are used to navigate through the tree. And the structure can be extended with interpretations of other definable relations we may want to use. We will call this basic structure of WS2S N_{2}.

Definition 2.1. The structure of WS2S (N_{2}) is a tuple ⟨T_{2}, ε, s_{0}, s_{1}⟩ such that T_{2} is a binary tree domain with root ε and s_{0}, s_{1} the left and right successor relations respectively.

We will overload the term WS2S to mean the structure of two successor functions as well as its MSO language.

Intuitively, MSO predicates, i.e., monadic second-order variables, pick out sets of nodes. We can think of the predicates as features labeling the nodes. A tree, then, is just a rooted, dominance connected subset T of the domain of N_{2}. A labeled tree is a k + 1-tuple ⟨T, F_{1}, …, F_{k}⟩ of the tree T and k features. Therefore, MSO formulas with the underlying interpretation on N_{2} are constraints on trees. And a grammar in this setting becomes just the specification of a k + 1-ary relation picking out the well-formed trees.

Formally, each MSO formula represents a constraint on the valuation of its free variables which is determined by the assignment of the variables to (sets of) nodes.

Definition 2.2. Let T be a tree domain and VAR a set of (MSO) variables. A variable assignment is a total function α : VAR → ℘(T ). We call the set of all those mappings ASS.

Obviously, satisfaction is relative to these assignments. We will write satisfaction as N_{2} ⊧ ϕ[α] for ϕ an MSO formula, α a variable assignment. Since these assignments are such that they map variables to nodes in a tree, i.e., the assignments together with the domain of interpretation form a (labeled) tree, we will also speak of assignment trees.

Since the proofs of the decidability results are inductive on the structure of MSO formulas, we can choose our particular tree description language rather freely, knowing (a) that the resulting logic will be decidable and (b) that the translation to automata will go through as long as the atomic formulas of the language represent relations which can be translated (by hand if necessary) to tree automata recognizing the “right” assignments to their free variables. We will see how this is done in the next section. Note that it requires further proof that these languages have the full power of WS2S, though.

Therefore, the use of the decidability result is not fixed to a particular area of natural language formalisms. For example, Ayari et al. (1998) have investigated the usefulness of these techniques in dealing with record-like feature trees which unfold feature structures; there the attributes of an attribute-value term are translated to distinct successor functions. On the other hand, Rogers (To appear) has developed a language rich in longdistance relations (dominance and precedence) which is more appropriate for work in GB theory. Compact automata can be easily constructed to represent dominance and precedence relations. One can imagine other possibilities as well: as we will see in Sec. 2.3, the automaton for Kaynestyle asymmetric, precedence-restricted c-command (Kayne, 1994) is also very compact, and makes a suitable primitive for a description language along the lines developed by Frank and Vijay-Shanker (1998).

2.2.1. An Example Language: L_{K,P}^{2} . In this paper, we draw our examples from tree description logics used in the P&P paradigm. In particular L_{K,P}^{2} , the logic proposed in Rogers (To appear), will serve as our main source. Note that L_{K,P}^{2} has been demonstrated to offer concise and well founded formalizations of concepts involved in P&P approaches. In fact, Rogers encodes in his monograph most of the proposals made in Relativized Minimality by Rizzi (1990). Although Rogers has shown that L_{K,P}^{2} is intertranslatable with SnS and therefore not limited to either binary or finite trees, we use it only in the weak sense over finite binary trees.

The language of L_{K,P}^{2} is designed to express relationships between nodes in trees representing linguistic structures. There are local relations on nodes such as the immediate dominance relation as well as nonlocal ones such as the reflexive closure of immediate dominance, simply called dominance. Various other theory independent relations for reasoning about relations between nodes can be defined in WS2S and added, e.g., proper precedence to express ordering information. We parameterize the language with both individual and predicate constants.

Example 2.3. Let L_{K,P}^{2} be defined by a set K of countably many individual constants; a set P of countably many predicate constants; a countably infinite set X = X_{0} ∪ X_{1} of first-order and monadic second-order variables; ∧, ∨, ¬ – logical connectives; ∀, ∃ – quantifiers; (,), [,] – brackets; ◁, ◁^{∗}, ◁^{+} – immediate, reflexive, and proper dominance; ≺ – proper precedence; and ∈, ≈ – set membership and equality.

In the remainder of the paper we will mostly use L_{∅,∅}^{2} and refer to it as L^{2}. The change does not limit the power of the language since both the predicate and individual constants correspond to free (global) variables. In fact, if one uses a tool to compile the automata from the formulas, one must use free variables since the compilation process cannot handle constants. We deviate slightly from Rogers’ definition of the language in that we include ∈ explicitly and use X(x) and x ∈ X interchangeably.

We will freely use appropriate symbols for standard combinations of the boolean operators (for example ⇒, ≉, ⇔, …), uppercase letters to denote set variables and lowercase ones to denote individual ones. As an example for relations definable in this language, take the subset relation in (1), the constraint for a set to contain exactly one member in (2) and, more linguistically motivated, the formula denoting the relation of directed asymmetric c-command^{1} in the sense of Kayne (1994), see (3).

(1)  X ⊆ Y ⟺^{def} (∀x)[x ∈ X ⇒ x ∈ Y]

\begin{aligned}Sing(X) ⟺^{def} & (∀Y, Z)[Y ⊆ X ⇒ (X ⊆ Y ∨ Y ⊆ Z)] ∧ \\ & (∃Y)[X ⊈ Y] \end{aligned} (2)

\begin{aligned}AC-Com(x, y) ⟺^{def} & x ≺ y \\ & ∧ (∀z)[z ◁^{+} x ⇒ z ◁^{+} y] ∧ ¬(x ◁^{∗} y) \\ & ∧ ¬((∀z)[z ◁^{+} y ⇒ z ◁^{+} x] ∧ ¬(y ◁^{∗} x)) \end{aligned} (3)

The formula in (1) is simple enough to be self-explanatory, whereas the one in (2) demonstrates how to use second-order quantification. Therefore we will explain it briefly. A set is a singleton iff all its subsets are either equal to it or the empty set and it itself is nonempty. The definition in (3) specifies that two nodes asymmetrically c-command each other from “leftto-right” iff x c-commands y, y does not c-command x and x precedes y. We depict an example tree in Fig. 2. The dashed arrow represents the c-command relation. Note that x also c-commands a and b, but does not asymmetrically c-command a.

1This relation is not monadic, but reducible via syntactic substitution to an MSO signature. We can define and use these explicitly definable relations freely, but we

\begin{aligned}& z \\ x & & a \\ & b & & y \end{aligned}

Figure 2. An example for asymmetric directed c-command

A structure for L_{K,P}^{2} consists of an appropriate set of nodes – a tree domain – with relations interpreting the elements from the signature. We limit the structure to dominance, parent and precedence since proper dominance can be defined in terms of them. This structure is a more specific alternative for the one given in Def. 2.1.

Example 2.4. A model for L_{K,P}^{2} is a tuple ⟨T , I, P, D, L, R_{p}⟩_{p∈P} with:

T  a nonempty tree domain
I  a function from K to T
P, D, L binary relations on T which interpret ◁, ◁^{∗} and ≺
R_{p}  are relations of appropriate arity on T interpreting p ∈ P.

A model for L^{2} is then just a tuple ⟨T , P, D, L⟩.

We will use this type of models whenever we speak of L^{2} or L_{K,P}^{2} and the more general one of N_{2} otherwise.

2.3. Representing MSO Formulas with Tree Automata. In this section we take a closer look at the connection between MSO formulas and tree automata. It should be pointed out immediately that the translation from formulas to automata, while effective, is of non-elementary complexity. In the worst case, the number of states can be given as a function of the number of free variables in the input formula with a stack of exponents as tall as the number of the formula’s quantifier alternations. However, there is a growing body of work in the computer science literature on computer hardware and system verification (e.g., Kelb et al. (1997), Klarlund (1998), Basin and Klarlund (To appear)) suggesting that in practical cases the extreme explosiveness of this technique can be effectively controlled, and our own experiments suggest that this should be the case in most linguistic applications as well. Experiences with a software tool are documented in Morawietz and Cornell (To appear).

cannot quantify over them. A relation r is explicitly MSO-definable iff there exists an MSO formula ϕ such that r(X_{1}, …, X_{n}) ⟺ ϕ(X_{1}, …, X_{n}).

The attraction of the proposed approach is obvious: the connection allows the linguist the specification of ideas about natural language in a concise manner in logic and at the same time provides a representation of the constraints which can be efficiently used for processing.

The decidability proof works by showing a correspondence between formulas in the language of WS2S and tree automata, developed in such a way that the formula is satisfiable iff the set of trees accepted by the corresponding automaton is nonempty.

More specifically, Doner (1970) and Thatcher and Wright (1968) show that each formula in MSO logic can be represented by a tree automaton which recognizes the relevant assignment trees. One step in the proof is to encode the variable assignments as the inverse of the labeling function, another the inductive construction of automata. Then WS2S is decidable since the emptiness problem for tree automata is decidable.

Remember that assignment functions map first order variables to nodes and second-order variables to sets of nodes in N_{2}. The labeling functions on the trees the automaton accepts do the converse: they map nodes to the set of free variables to which that node is assigned. Concretely, we can think of nodes as being labeled with bit-strings such that bit i is on at node n if and only if n is to be assigned to variable X_{i}.

More formally, let again N_{2} be the structure of WS2S and ϕ(X⃗) a formula with free variables X⃗. We can safely ignore individual variables since they can be encoded as properly constrained set variables with the formula for Sing given in (2). For each relation r(X⃗) from the signature of the MSO logic, we have to define a tree automaton 𝔄^{r} recognizing the proper assignment trees. Then we can inductively build a tree automaton 𝔄^{ϕ} for each MSO formula ϕ(X⃗), such that

N_{2} ⊧ ϕ[τ] ⟺ t ∈ T (𝔄^{ϕ}) (4)

where τ assigns sets of nodes to the variables X⃗ and t is the corresponding assignment tree. The automaton compactly represents the (potentially infinite) number of valuations, i.e., the solutions to constraints.

Consider as an example the tree automaton corresponding to Kayne’s asymmetric c-command relation from (3), see Fig. 3. For readability, we denote the alphabet of node labels as tuples indicating for each free variable whether a node is assigned to it or not. In this case we have only free variables x and y, so the alphabet consists of the tuples ⟨x, y⟩, ⟨¬x, y⟩, ⟨x, ¬y⟩ and ⟨¬x, ¬y⟩.

On closer examination of the transitions, we note that we just percolate the initial state as long as we find nodes which are neither x nor y. From

𝔄 = ⟨A, Σ, a_{0}, F, α⟩,

A = {a_{0}, a_{1}, a_{2}, a_{3}, a_{4}, a_{5}},

Σ = {⟨x, y⟩, ⟨x, ¬y⟩, ⟨¬x, y⟩, ⟨¬x, ¬y⟩}
F = {a_{4}},
α(a_{0}, a_{0}, ⟨¬x, ¬y⟩) = a_{0} α(a_{0}, a_{0}, ⟨ x, ¬y⟩) = a_{3}
α(a_{0}, a_{0}, ⟨¬x, y⟩) = a_{1} α(a_{0}, a_{1}, ⟨¬x, ¬y⟩) = a_{2}
α(a_{0}, a_{2}, ⟨¬x, ¬y⟩) = a_{2} α(a_{0}, a_{4}, ⟨¬x, ¬y⟩) = a_{4}
α(a_{1}, a_{0}, ⟨¬x, ¬y⟩) = a_{2} α(a_{2}, a_{0}, ⟨¬x, ¬y⟩) = a_{2}
α(a_{3}, a_{2}, ⟨¬x, ¬y⟩) = a_{4} α(a_{4}, a_{0}, ⟨¬x, ¬y⟩) = a_{4}

all other transitions are to a_{5}

Figure 3. The automaton for AC-Com(x, y)

the initial state on both the left and the right subtree we can either go to the state denoting “found x” (a_{3}) if we read symbol ⟨x, ¬y⟩ or to the state denoting “found y” (a_{1}) if we read symbol ⟨¬x, y⟩. After finding a dominating node while being in a_{1} – which switches the state to a_{2} – we can percolate a_{2} as long as the other branch does not immediately dominate x. If we come into the situation that we have a_{3} on the left subtree and a_{2} on the right one, we go to the final state a_{4} which again can be percolated as long as empty symbols are read. Clearly, the automaton recognizes all trees which have the desired c-command relation between the two nodes. But in addition to the arbitrary number of intermediate nodes, we can also have an arbitrary number of ⟨¬x, ¬y⟩ labeled nodes dominating the constellation or being dominated by it such that we recognize the closure of the (AC-Com) relation in the sense of Doner. The relation can now serve as a new primitive in further MSO formulas.

To keep the automata as small as possible, we employ the suitably adapted minimization of finite state automata. The minimization procedure also gives us an alternative way to decide emptiness since the canonical empty automaton has only one state which is initial but not final.

The non-elementary complexity is caused by alternation between quantifier blocks. Quantification results in nondeterministic automata, but negation needs deterministic ones as input. So for each universal quantifier followed by an existential one, we need the subset construction which has an exponential worst case complexity: the number of states can grow according to a function with a stack of exponents whose height is determined by the number of ∀−∃ quantifier alternations.

2.4. Automata-based Theorem Proving. Automated theorem proving is the standard approach to processing with constraint-based grammars. The decidability proof gives us a procedure to do theorem proving since the compilation produces an automaton recognizing the empty language iff the formula is unsatisfiable. Practically this means that a formula is satisfiable if the resulting automaton has a non-empty set of final states and valid if the resulting automaton has exactly one state which is initial and final such that all assignments are recognized. So, theorem proving and compilation are in fact one and the same process.

An obvious goal for the use of the discussed approach is the (offline) generation of a tree automaton representing an entire grammar. Then parsing would be just proving that the grammar implies the input. Unfortunately, as mentioned above, the problem to generate the tree automata from arbitrary MSO formulas is highly exponential because of the necessary determinization. And even worse: the alphabet space is an additional source for combinatorial explosion. Features are free variables and therefore alphabet symbols for the automata. Since there is no a priori limit on any combination not occurring, we have to represent all their permutations. In extreme cases, this dominates even the state space. As an example, consider a naïve specification of the lexicon:

Lexicon(x) ⟺^{def} (Sees(x) ∧ V (x) ∧ 3rd(x) ∧ …) ; ∨ (Jan(x) ∧ N(x) ∧ Masc(x) ∧ …) ; ∨ (Lena(x) ∧ N(x) ∧ F em(x) ∧ …) ; ⋮ (5)

We have defined a relation called Lexicon via a disjunctive specification of lexical labels, realized as for example the second-order variable Sees, and the appropriate combination of features, e.g., V. The way we presented it, Lexicon looks like a monadic predicate with just one argument. But considering the automaton to be generated from the formula, one has to know that the alphabet of the automata has to contain every free variable to encode the right assignments. Therefore all the free variables contained in the formula are implicitly present: Lexicon is a relation. Remember that since constants are free variables to the compiler, using them does not change the argument. And since every feature and every lexical entry is represented with a new free set variable, the alphabet size will be 2^{n+m}, n the number of lexical entries and m the number of features. Nevertheless we will continue to leave these “global” variables implicit.

For tests, we used the tool MONA (Klarlund and Møller, 1998). The major improvement of MONA against our own prototype (Morawietz and Cornell, 1997) is the use of binary decision diagrams (BDDs) for the representation of large alphabets. The graph structure of BDDs allows compression of the transitions by removing redundant tests and nodes. But the amount of compression which can be achieved is very much dependent on ordering the free variables and finding an optimal ordering is NP-hard. An introduction to BDDs can, for example, be found in Andersen (1996). It is still an open problem whether the generation of an entire grammar can be handled. The question is not efficiency of the compilation, but rather feasibility since the size of an automaton representing a grammar is still indeterminate. And it is unlikely that even the use of BDDs helps sufficiently with the representation of a realistic lexicon.

However, the tests have shown that we can compile modules and by this gain insight into parts of the formalization (e.g., see Morawietz and Cornell (To appear) for a report on the compilation of Rogers’ entire X-Bar theory). As an example consider the c-command relation between categories instead of nodes following the presentation of Rizzi’s ideas from Relativized Minimality in Rogers’ monograph. This is a nontrivial part of the theory, but turns out to have a compact automaton.

Informally, a category is a node which has been split into segments through adjunction. Categories are used in P&P approaches since for example in a WH-question the auxiliary is supposed to c-command its trace. Following Rizzi, this is explained by the fact that the node is adjoined to its head and therefore not dominated by it. In Fig. 4 one can see that I_{j} is indeed not dominated by the category formed by the two nodes labeled C. I_{j} c-commands its trace t_{j} since all categories which dominate it, also dominate t_{j}.

The definition of categories can be found in (6) and (7). In the formulas, we assume some additional predicates: Feq ensures agreement on some set of relevant features; Path can be understood as a dominance-connected ordered subgraph, and Adj is the feature marking an adjoined node.

Component(X) ⟺^{def} Path(X) ∧
(∀x, y)[(x ∈ X ∧ y ∈ X) ⇒ Feq(x, y)] ∧
(∀x, x′)(∃y)(∀z)[(x ∈ X ∧ x′ ∈ X ∧ x ◁ x′) ⇒
(x′ ∉ Adj ∧ x ◁ y ∧ y ≉ x′ ∧ y ∈ Adj ∧
(x ◁ z ⇒ (z ≈ x′ ∨ z ≈ y)))]

(6)

CP

NP_{i}  C̄
W ho  C  IP
I_{j} C NP  Ī
did Ø Lena t_{j}  VP

Figure 4. A syntax tree from Rogers (To appear)

So, a component is a set of nodes which (a) form a path in the tree; (b) agree on a set of particular features; and (c) have exactly one node in every local tree which is the result of an adjunction.

A category is then just a maximal component.

Category(X) ⟺^{def} Component(X) ∧
(∀Y)[(X ⊆ Y ∧ Y ⊈ X) ⇒ ¬Component(Y)]

(7)

Note that a number of additional constraints on the distribution of adjuncts is necessary to achieve the “right” behaviour.

Building on the given definition, we can define primitives of domination, precedence and c-command in terms of categories rather than nodes. We can relativize all of them to nodes, e.g. Category(x, y) means that there exists a category such that x and y are both members of it, thereby avoiding the third-order notions.

As might be suspected considering (6) and (7), the complete presentation of the formulas encoding category based c-command is fairly complex – although c-command itself is just a lifted version of what we saw in (3) using the new category-based primitives for domination instead of the ones from the signature – and therefore beyond the scope of this paper. The reader is encouraged to check the full formalization in Rogers’ monograph. But actually, after existentially binding the global variables, the resulting automaton is small. It has only 5 states and 16 transitions, see Fig. 5. Since c-command on categories is a complicated relation, we cannot give a detailed explanation of the automaton.

𝔄 = ⟨A, Σ, a_{0}, F, α⟩

A = {a_{0}, a_{1}, a_{2}, a_{3}, a_{4}}

Σ = {⟨x, y⟩, ⟨x, ¬y⟩, ⟨¬x, y⟩, ⟨¬x, ¬y⟩}
F = {a_{3}}
α(a_{0}, a_{0}, ⟨¬x, ¬y⟩) = a_{0} α(a_{0}, a_{0}, ⟨ x, ¬y⟩) = a_{2}
α(a_{0}, a_{0}, ⟨¬x, y⟩) = a_{1} α(a_{0}, a_{0}, ⟨ x, y⟩) = a_{3}
α(a_{0}, a_{1}, ⟨¬x, ¬y⟩) = a_{1} α(a_{0}, a_{1}, ⟨ x, ¬y⟩) = a_{3}
α(a_{0}, a_{2}, ⟨¬x, ¬y⟩) = a_{2} α(a_{0}, a_{2}, ⟨¬x, y⟩) = a_{3}
α(a_{0}, a_{3}, ⟨¬x, ¬y⟩) = a_{3} α(a_{1}, a_{0}, ⟨¬x, ¬y⟩) = a_{1}
α(a_{1}, a_{0}, ⟨ x, ¬y⟩) = a_{3} α(a_{1}, a_{2}, ⟨¬x, ¬y⟩) = a_{3}
α(a_{2}, a_{0}, ⟨¬x, ¬y⟩) = a_{2} α(a_{2}, a_{0}, ⟨¬x, y⟩) = a_{3}
α(a_{2}, a_{1}, ⟨¬x, ¬y⟩) = a_{3} α(a_{3}, a_{0}, ⟨¬x, ¬y⟩) = a_{3}

all other transitions are to a_{4}

Figure 5. The automaton for category based c-command

One can see from the discussions in this section that the approach of pure theorem proving, i.e., using only the automata as the operational interpretation of our formalism, is computationally not without problems. But we can define new primitives and work with them since we can represent MSO constraints, i.e., knowledge about variable bindings on trees, efficiently with tree automata. In the following sections we are going to use constraint logic programming to reintroduce a notion of derivation into the purely model-theoretic presentation. By this we provide a way to use the previously compiled parts or primitives of formalizations separately under the control of programs and gain the desired extension of the generative capacity.

3. Constraint Logic Programming

Logic programming (LP) reflects nicely the separation of the actual logic of a program and the control of its execution (Lloyd, 1984). Programs in the LP paradigm are sets of logical clauses. These programs are interpreted within Herbrand models, i.e., sets of ground atoms. One could be content with this declarative interpretation. But on the other hand one wants to compute with them. The added operational interpretation used in most LP languages is based on SLD-resolution (Linear resolution with a Selection function for Definite clauses). Then the semantics is reformulated in procedural terms of least models and fixpoints such that the languages have provably equivalent denotational and operational semantics. Two problems with this approach – the generate and test paradigm to find the solutions and the use of uninterpreted structures – can be overcome by the addition of constraints to the standard logic programming scheme.

Intuitively, with the constraint logic programming scheme we develop a way to give definite clause specifications over MSO formulas. We will use this extended language to constrain the variables by incrementally adding suitable constraints to a constraint store. The store can be viewed as a tree automaton representing the possible valuations. In fact, we control the generation of the tree automaton we are interested in. By this we can focus on just those parts of the grammar which are relevant to the actual computation instead of having to consider – and precompile – all possibilities inherent in the grammar at once. A standard interpreter (left to right, depth first search) is sufficient for the execution of one of our programs. The answer of a search branch of such a program will be a satisfiable MSO constraint represented by a tree automaton. Backtracking then allows the search for more answers. Furthermore, the embedding allows us to apply a wealth of techniques developed in general for (constraint) logic programming and the corresponding interpreters to optimize the behaviour of the programs.

In logic programming enhanced with constraints over a specific domain, we need a specialized mechanism to solve the constraints, i.e., decide their satisfiability. Although this mechanism is treated as a black box in the actual definitions of the constraint language, it is an important aspect in the effectiveness to have a suitable constraint solver. In Sec. 3.2.5 we will discuss some desiderata for an efficient constraint solver for our purposes.

The CLP language serves both the facilitation of the use of MSO formalizations in computational linguistics and the extension of the generative capacity of MSO-based grammar formalisms. Our main motivation for the necessity of the extension are the arguments on non-context-freeness of natural languages. For example, Swiss German (Shieber, 1985) or Dutch (Huybregts, 1984) have overt case marking on objects and allow cross-serial dependencies in subordinate clauses. Cross-serial dependencies cannot be formalized in MSO-based approaches since their underlying structure is comparable to the copy language – L_{copy} = {ww | w ∈ Σ^{∗}} – which is not context-free.

3.1. The Constraint Language. In this section we apply the general scheme developed in Höhfeld and Smolka (1988) for the definition of a constraint language to MSO logic, fixing the domain of computation to trees. We use this scheme as opposed to the more standard one of Jaffar and Maher (1994) since it abstracts from the actual details of the syntax of the constraint language and obviates some technical requirements on the language, most notably solution compactness. Remember that formally we do not need individual variables.

Following Höhfeld and Smolka, we can turn any MSO logic on trees or strings into a constraint language. MSO will be used as a place holder for any such constraint language. We already presented the definition of an interpretation for WS2S in Def. 2.1. We generalize it by the inclusion of a solution mapping [[−]]^{I} which in essence amounts to our compilation procedure.

Definition 3.1. A constraint language MSO = ⟨VAR, CON, V, INT⟩ is a fourtuple such that

1. VAR is a countable (possibly) infinite set of (MSO) variables,

2. CON is a (decidable) set of well formed formulas (of MSO logic),

3. V is a computable function which assigns to every ϕ ∈ CON a finite set V(ϕ) of variables, called the variables constrained by ϕ or the free variables of ϕ,

4. INT is a nonempty set of MSO-interpretations I such that each interpretation is a pair (N_{2}, [[−]]^{I}) consisting of N_{2} and solution or denotation mappings [[−]]^{I} such that

(a) [[−]]^{I} is a function mapping every constraint ϕ to a set [[ϕ]]^{I} of assignments, [[−]]^{I} : CON ⟶ ℘(ASS). We call that set the solutions of ϕ (in I).

(b) ϕ ∈ CON constrains only V(ϕ), i.e., if α ∈ [[ϕ]]^{I} and β is an assignment witch agrees with α on V(ϕ), then β ∈ [[ϕ]]^{I}.

Satisfiability and validity are defined as usual. Most conditions are trivially satisfied for MSO logics, but two details are left to be specified. Firstly we present the function which computes the free variables.

Definition 3.2. Let MSO = ⟨VAR, CON, V, INT⟩ be a constraint language, then the function V : CON → ℘(VAR) is defined as follows (R ranges over the defined relations from the signature, ∗ over binary connectives, Q over quantifiers):

V(R(X_{1}, …, X_{n})) = {X_{1}, …, X_{n}}  V(¬ϕ) = V(ϕ)
V(ϕ ∗ ψ) = V(ϕ) ∪ V(ψ)  V(QX[ϕ]) = V(ϕ) − {X}

And secondly, the definition of the denotation function [[−]]^{I}. This depends on the actual relations in the signature. We use L^{2} as our example to present it.

Example 3.3. Let M = ⟨T , P, D, L⟩ be a model for L^{2} and let α[X/A] be the assignment function just like α except that the variable X gets assigned the value A ⊆ T . Then L^{2} is a constraint language MSO with VAR being X, CON being the formulas of L^{2}, V as defined above and with INT consisting of interpretations I = (M, [[−]]^{I}) such that the denotation function is defined as follows:

[[x ◁ y]]^{I} = {α | ⟨α(x), α(y)⟩ ∈ P}
[[x ◁^{∗} y]]^{I} = {α | ⟨α(x), α(y)⟩ ∈ D}
[[x ≺ y]]^{I} = {α | ⟨α(x), α(y)⟩ ∈ L}
[[x ≈ y]]^{I} = {α | α(x) = α(y)}
[[x ∈ X]]^{I} = {α | α(x) ∈ α(X)}
[[ϕ ∧ ψ]]^{I} = [[ϕ]]^{I} ∩ [[ψ]]^{I}
[[ϕ ∨ ψ]]^{I} = [[ϕ]]^{I} ∪ [[ψ]]^{I}
[[¬ϕ]]^{I} = ASS − [[ϕ]]^{I}
[[∃X[ϕ]]]^{I} = {α | α[X/A] ∈ [[ϕ]]^{I} for some A ⊆ T }
[[∀X[ϕ]]]^{I} = {α | α[X/A] ∈ [[ϕ]]^{I} for all A ⊆ T }

3.1.1. Properties of MSO. In this section we recall some of the properties of MSO. In part these are properties directly derived from MSO logic. The other part concerns properties which are relevant in the proofs concerning the further development of the constraint language and its relational extension.

Renamings and variants are relevant in the proof of the soundness and completeness of the operational semantics in Sec. 3.2.3. The following definition of a renaming is based on the denotational properties of the formulas involved. It is not a purely syntactic substitution. For variants we demand that two formulas agree on their free variables and denote the same assignment functions modulo a renaming. A renaming is the bijection ρ : VAR → VAR such that it is the identity except for finitely many variables. If ρ is a renaming, a constraint ϕ′ is called a ρ-variant of ϕ if (a) ϕ′ is a syntactic variant of ϕ, i.e., ϕ′ results from simultaneously replacing every occurrence of a variable X in ϕ with ρ(X) and (b) if V(ϕ′) = ρ(V(ϕ)) and [[ϕ]]^{I} = [[ϕ′]]^{I}ρ with [[ϕ′]]^{I}ρ := {αρ^{−1} | α ∈ [[ϕ]]^{I}} for every interpretation I. A constraint ϕ′ is called a variant of ϕ if there exists a renaming ρ such that it is a ρ-variant under that renaming. Note that by this definition renamings preserve satisfiability and validity.

Definition 3.4. A constraint language MSO = ⟨VAR, CON, V, INT⟩ is

1. closed under renaming if every constraint ϕ ∈ CON has a ρvariant ψ ∈ CON for every renaming ρ,

2. closed under intersection if for every two constraints ϕ and ψ in CON there exists a constraint θ ∈ CON such that for every interpretation I ∈ INT: [[ϕ]]^{I} ∩ [[ψ]]^{I} = [[θ]]^{I},

3. decidable if the satisfiability of its constraints is decidable.

Lemma 3.5. L^{2} is a decidable constraint language closed under renaming and intersection.

3.2. Relational Extension. We add distinguished relations to the constraint language MSO to derive a relational extension. Recall that we take the step of adding special relations to a (new) language for two reasons. Firstly we can now give an operational semantics to inductive definitions in R(MSO) and by this explicitly separate the original signature and these defined relations. And secondly we extend both generative capacity and computational power. It is an important question which of the properties of MSO we can preserve and which we loose.

Definition 3.6. A constraint language MSO = ⟨VAR, CON, V, INT⟩ is extended with a decidable set of relations R and a corresponding arity function ar : R ⟶ ℕ to a relational constraint language R(MSO) = ⟨VAR, R(CON), V, R(INT)⟩ as follows:

1. The set of R(MSO)-constraints R(CON) is defined inductively such that

(a) ϕ ∈ R(CON) for all ϕ ∈ CON.

(b) r(X_{1}, …, X_{n}) ∈ R(CON) for all tuples of pairwise distinct variables X_{1}, …, X_{n} and relation symbols r ∈ R with ar(r) = n. We call these R(MSO)-atoms.

(c) if F and G are constraints in R(CON), then so are F & G, F → G and the empty conjunction ∅.

(d) Nothing else is in R(CON).

2. The function V computing the free variables of an R(MSO)-con-straint is again defined inductively:

(a) V(ϕ) := V(ϕ) for ϕ ∈ CON

(b) V(r(X_{1}, …, X_{n})) := {X_{1}, …, X_{n}} for r ∈ R with ar(r) = n (c) V(∅) := ∅ (d) V(F & G) := V(F) ∪ V(G)

(e) V(F → G) := V(F) ∪ V(G)

3. An R(MSO)-interpretation A is the extension of an MSO-inter-pretation I on the same domain to include the new relational symbols by choosing relations r^{A} ⊆ ℘(T ) × ⋯ × ℘(T ) for each r ∈ R, and by extending the solution mapping as follows:

(a) [[ϕ]]^{A} := [[ϕ]]^{I} for ϕ ∈ CON

(b) [[r(X_{1}, …, X_{n})]]^{A} := {α ∈ ASS | α(X_{1}, …, X_{n}) ∈ r^{A}}

(c) [[∅]]^{A} := ASS

(d) [[F & G]]^{A} := [[F]]^{A} ∩ [[G]]^{A}

(e) [[F → G]]^{A} := (ASS − [[F]]^{A}) ∪ [[G]]^{A} R(INT) is the set of all R(MSO)-interpretations A.

3.2.1. Definite Clauses. To be able to use the relational extensions we presented, we have to formalize the notion of computing with the language. The simplest approach – as has been presented for logic programs in Lloyd’s book – is to define definite clauses and definite clause specifications, also called programs.

In this section we follow again Höhfeld and Smolka in applying their general scheme to our special case. The key is that, as in standard logic programming, we can always find a minimal model for a given program. Firstly, we define what a program in the formal sense is.

Definition 3.7. Let R(MSO) = ⟨VAR, R(CON), V, R(INT)⟩ be a relational constraint language. A definite clause specification S is a finite set of definite clauses of the form

H ← ϕ & B_{1} & … & B_{n}

where H and the B_{i} are R(MSO)-atoms, n ≥ 0 and ϕ ∈ CON.

As usual, we will refer to the single atom as the head of the clause and to the conjunction of the atoms with the constraint as the body. The MSO-constraint in the body will also be called a guard. A definite clause with just the MSO-constraint and no atoms in the body is called a fact. A goal is a possibly empty conjunction of MSO-constraints and R(MSO)-atoms.

Definition 3.8. Given a definite clause specification S, an R(MSO)- interpretation A is a model of S if every variable assignment is a solution for every definite clause, i.e., ∀α ∈ ASS ∀σ ∈ S : α ∈ [[σ]]^{A}.

Höhfeld and Smolka prove that indeed there exists a least model A for every program which can be constructed from an interpretation I of the underlying constraint language as a limit of the application of the clauses in the following way.

The sets of interpretations A_{i} agree on their base interpretation I. Therefore we can order them according to the order imposed by the relational symbols in R, i.e., A_{i} ⊆ A_{j} iff r^{A_{i}} ⊆ r^{A_{j}} for all r ∈ R. Note that the denotation function actually preserves this order, i.e., for G an R(MSO)-atom, [[G]]^{A_{i}} ⊆ [[G]]^{A_{j}} if A_{i} ⊆ A_{j}. Intersection and union of such interpretations are again defined via their relations, i.e., A_{i}∩A_{j} = A_{k} iff r^{A_{i}} ∩ r^{A_{j}} = r^{A_{k}} and A_{i} ∪ A_{j} = A_{k} iff r^{A_{i}} ⊆ r^{A_{j}} = r^{A_{k}} for all r ∈ R. Note that a set of interpretations extending I forms a complete lattice.

Theorem 3.9 (Definiteness Theorem, H&S theo. 4.4). Let S be a definite clause specification in R(MSO), I an MSO-interpretation and B ranging over bodies of clauses from S. Then we can inductively define a chain of R(MSO)-interpretations A_{i} ⊆ A_{i+1}, i ≥ 0, extending I by

(i) r^{A_{0}} := ∅ (ii) r^{A_{i+1}} := {α(X⃗) | (r(X⃗) ← B) ∈ S and α ∈ [[B]]^{A_{i}}} (iii) r^{A} := ⋃_{i≥0} r^{A_{i}}

The least model A of S extending I is the union A := ⋃_{i≥0} A_{i}.

The proof of this theorem is via the monotonicity of the definitions and the corresponding fixpoint theorem.

3.2.2. An R(MSO) Example. As an example for the relational language we defined, we present the definition of append on lists in R(MSO). Notational conventions for the definite clauses are that the associated MSO-constraints are enclosed in curly brackets, lowercase letters denote node variables, uppercase letters or words starting with them set variables and relations in MSO are uppercase sans-serif and R(MSO) ones are lowercase sans-serif strings.

Firstly we need some explicit definitions of MSO constraints for the data type List on nodes. We do this by ordering a set of nodes by dominance. With the constraints Min and Max we can pick out the least and the greatest element in this set (the least one being the lowest one in the tree). The empty list is just an empty set, and a nonempty list has at least one element, is connected and all its elements stand in the reflexive dominance relation. The head of such a list is just the “highest” element, the tail all the remaining elements. It would have been possible equally well to assume a list to be a yield of a tree, i.e., a set of nodes ordered by precedence. We leave this definition to the reader. The exact definitions can be found in in (8) to (14).

append(X, Y, Z) ←
{Elist(X) ∧ Y ≈ Z}
append(X, Y, Z) ←
{Hd(x, X) ∧ Hd(x, Z) ∧ Tl(X, U) ∧ Tl(Z, V)} &
append(U, Y, V)

Figure 6. The definition of append in R(MSO)

(8)  Min(x, X) ⟺^{def} x ∈ X ∧ (∀y ∈ X)[y ≉ x ⇒ y ◁^{+} x]
(9)  Max(x, X) ⟺^{def} x ∈ X ∧ (∀y ∈ X)[y ≉ x ⇒ x ◁^{+} y]
(10)  Elist(X) ⟺^{def} ¬(∃x)[x ∈ X]
Nelist(X) ⟺^{def} (∃x)[x ∈ X] ∧ Connected(X)
∧ (∀x, y ∈ X)[x ◁^{∗} y ∨ y ◁^{∗} x]

(11)

(12)  List(X) ⟺^{def} Elist(X) ∨ Nelist(X)
(13)  Hd(x, X) ⟺^{def} Nelist(X) ∧ Max(x, X)
Tl(X, Y) ⟺^{def} Y ⊆ X ∧ Nelist(X) ∧ List(Y)
∧ (∀x ∈ X)[¬Hd(x, X) ⇔ x ∈ Y]

(14)

The resulting R(MSO) definition for append is almost like the definition in standard logic programming. We just have to make what corresponds to unifications between variables explicit in the constraints, see Fig. 6.

3.2.3. Operational Semantics. The standard approach for an operational semantics of logic programs is to move stepwise from goals to answers. In this section we adapt the Höhfeld and Smolka definitions of their generalization of SLD-resolution to R(MSO). In the following S is always a definite clause specification, A an atom, F and G goals and ϕ ∈ CON.

Intuitively, we can substitute the body of a clause if the head represents a renamed variant of an atom occuring in the goal. To limit the search for the right clause, we incorporate constraint solving. This prevents the execution of a body of a clause if the requirements stated in the constraint are not met, i.e., we apply the rule only if the combination of the information in the constraint store and the constraint in the clause does not result in a contradiction. To provide an example, in the case of Prolog only clauses whose head unifies with the selected atom are tried for further resolution.

Definition 3.10. Let S be a definite clause specification, V a finite set of MSO-variables, A an R(MSO)-atom, F and G goals, A an R(MSO)- interpretation and ϕ, ψ, θ satisfiable MSO-constraints. S-goal reduction (⟶^{r}_{S,V}) is defined to be

A & G & ϕ ⟶^{r}_{S,V} F & G & θ

if A ← F & ψ is a variant of a clause in S such that [[ϕ]]^{A} ∩ [[ψ]]^{A} = [[θ]]^{A} and (V ∪ V(G)) ∩ V(F) ⊆ V(A). Let ⟶^{r}_{S,V}^{∗} be the reflexive, transitive closure of ⟶^{r}_{S,V}.

Note that the condition on the free variables ensures that those common to F and G have to be “carried over” by A. The set V can be used to distinguish between variables introduced by the query and the ones introduced by the computation if V corresponds to the free variables of the initial goal. Since the language is closed under intersection, we can treat the conjunction of the two constraints ϕ & ψ as a single new constraint θ.

We have already stated informally what we expect the answer to a search branch to one of our programs to be. More formally, if S is a definite clause specification, then an S-answer of a goal G is a satisfiable MSO-constraint ϕ such that ϕ → G is valid in every model of S.

The reduction rule we defined is actually sound, i.e., if we reduce a goal we are at least as specific about the answer as we were before.

Theorem 3.11 (H&S prop. 5.1). Let S be a definite clause specification and G, F goals. If G ⟶^{r}_{S,V} F, then [[F]]^{A} ⊆ [[G]]^{A} for every model A of S.

Lemma 3.12 (Soundness). Let S be a definite clause specification, G a goal and ϕ an MSO-constraint. If G ⟶^{r}_{S,V}^{∗} ϕ, then ϕ is an S-answer.

Proof. ϕ is an S-answer just in case (ASS − [[ϕ]]^{A}) ∪ [[G]]^{A} = ASS for all models A of S. This is true by Theorem 3.11 since [[ϕ]]^{A} ⊆ [[G]]^{A} holds.

Given a finite set of variables V as above, the notion of a solution is extended accordingly, i.e., [[ϕ]]_{V}^{A} = {α↾_{V} | α ∈ [[ϕ]]^{A}}; α↾_{V} being the restriction of α to the variables occurring in V.

We state in the following corollary that reduction is also complete. Intuitively, if there exists a solution to a goal, then we can find a constraint representing it via goal reduction.

Corollary 3.13 (Completeness, H&S cor. 5.3). Let G be a goal, A an atom in G, A a minimal model of S and α ∈ [[G]]_{V}^{A}. Then there exists an S-answer ϕ of G such that G ⟶^{r}_{S,V}^{∗} ϕ and α ∈ [[ϕ]]_{V}^{A}.

3.2.4. Properties of R(MSO). In this section we investigate which properties of MSO are preserved by the extension to R(MSO). Höhfeld and Smolka establish the fact that if MSO is closed under renaming, so is R(MSO). Closure under intersection is covered by definition. But what about generative capacity and decidability?

Unfortunately, we have to answer the last point in the negative. We can indeed define undecidable problems. Consider the Post Correspondence Problem (PCP) (Post, 1946). A Post correspondence system over an alphabet Σ is a finite nonempty set P = {(l_{i}, r_{i}) | i = 1 … m & l_{i}, r_{i} ∈ Σ^{∗}}. A solution for such a system P is a sequence of indices 1 ≤ i_{1}, …, i_{n} ≤ m such that l_{i_{1}} ⋯ l_{i_{m}} = r_{i_{1}} ⋯ r_{i_{m}}. It is undecidable whether there exists a solution for a given system (if the alphabet has more than two symbols).

To be able to facilitate the presentation of the encoding into R(MSO) we sugar our notation. Instead of using the constraint part to deal with identity of sets (unification) and the decomposition of linearly ordered sets or better lists, we use the “•” to encode list concatenation ([X • Y] for Hd(X, Z) ∧ Tl(Z, Y)) directly in the atom and not in an extra constraint in the body. Furthermore we assume that all our variables are constrained to be lists and that there exists an appropriate extension of our List and append examples in (8) to (14) and in Fig. 6 to lists of lists.

The encoding adapts the one from Hanschke and Würtz (1993). Words are represented as lists, e.g., a_{1}a_{2}a_{3} = [a_{1}•a_{2}•a_{3}]. The empty lists denotes the empty word. The solution to the PCP will be encoded in two lists (of lists). We will successively generate all possible sequences of indices using the program in Fig. 7.

Considering the query in the first line, this encodes all sequences of length 1, in the next step we use the first sequence as a suffix to generate all sequences of length 2. In general, we select a sequence s of length j and use it as a suffix to generate the sequences of length j + 1. This is a fair strategy to generate all possible sequences. In fact, the program in Fig. 7 has an SLD refutation iff a given Post correspondence system has a solution. Therefore we can state the next lemma.

Lemma 3.14. Satisfiability in R(MSO) is undecidable.

← pcp([[l_{1}] • [l_{2}] • ⋯ • [l_{m}]], [[r_{1}] • [r_{2}] • ⋯ • [r_{m}]])
pcp([L • L1], [L • R1]) ←
pcp([L • X], [R • Y]) ←
append(X, [[l_{1} • L] • ⋯ • [l_{m} • L]], X1) &
append(Y, [[r_{1} • R] • ⋯ • [r_{m} • R]], Y 1) &
pcp(X1, Y 1)

Figure 7. The PCP predicate

Furthermore, we can achieve the same by only considering a smallest binary program (see Hanschke and Würz for a definition), since we can eliminate the calls to append by the use of difference lists. Since smallest binary programs (on terms) are Turing equivalent (Devienne et al., 1994), it seems that our extension has the same power.

There are two directions we can take from here. Firstly, we can accept the extension as it is. In that case we defined a general purpose programming language on trees. Compared with Prolog, the difference is that we do not interpret terms over a Herbrand universe, but sets of nodes in N_{2}. And secondly, we can search for (syntactic) characterizations of decidable subclasses of these inductive definitions. We pursue this last proposal in the next paragraphs.

Obviously we can use all relations which are explicitly definable in MSO. An example for an explicit definition is the one of lists given in (8) to (14) or the definition of an arbitrary fact like the base case of append in Fig. 6, i.e., those relations which reduce via a syntactic substitution to an MSO signature.

Moschovakis (1974) provides the notions of first and second-order inductive definability to designate those relations which are recursively definable.^{2} The following paragraphs relate the model-theoretic notions with the operational ones we used in the preceding sections.

We are going to define the relations recursively via an operator which computes all the tuples of sets contained in it. Since we limit ourselves to positive occurrences of the relation symbol, the operator is monotone and a least fixed point exists. An inductive definition is not satisfiable by a single relation but by a whole set of them. These are the fixed points of the operator. Intuitively, an inductive definition corresponds to a recursive definite clause definition where the relation we define is to be added to the signature of our model. In general, the name of the predicate in the definite clause corresponds to a third-order variable. For example in a fact like the base case of append(X, Y, Z), we can view append as a thirdorder variable with monadic second-order arguments. In the following all the X_{i} and X are meant to be (monadic) second-order variables. X is a third-order variable with monadic arguments, but naturally we do not allow quantification over the non-monadic and third-order ones. We assume the extension of the variable assignments to these second- and third-order variables such that they assign sets of nodes, i.e., relations on individuals or sets of sets of nodes, i.e., relations on sets. Recall that X⃗ denotes a tuple of distinct variables; X⃗_{n} stands for a tuple of length n.

2A detailed analysis of these notions in relation to L_{K,P}^{2} can be found in Rogers (To appear).

Definition 3.15. Let R ⊆ ℘(T )^{n} and ϕ be a formula with V(ϕ) = {X⃗_{n}, X} such that X has arity n and occurs only positively. Then we define the operator Γ_{ϕ} : ℘(℘(T )^{n}) → ℘(℘(T )^{n}) as

Γ_{ϕ}(R) := {α(X⃗_{n}) | N_{2} ⊧ ϕ[α] and α(X) = R}.

The corresponding least fixpoint of Γ_{ϕ}^{ω} = Γ_{ϕ} (⋃_{n<ω} Γ_{ϕ}^{n}), i.e., the least Γ_{ϕ}^{ω} such that Γ_{ϕ}(Γ_{ϕ}^{ω}) = Γ_{ϕ}^{ω} will be called F (Γ_{ϕ}).

The relation R is called (second-order) inductively definable iff there exists such a formula ϕ(X⃗_{n}, X) such that R = F (Γ_{ϕ}).

Recall from Def. 3.6 that the relations we define there are sets of sets and computed as fixpoints, too. And R(MSO) does not have negation so that the relational symbols occur only positively. In case we have multiple clauses for one relation we assume this to correspond to a disjunction of its clauses. We can classify the R(MSO)-relations as follows.

Lemma 3.16. Let R(MSO) be a relational constraint language with r ∈ R, ar(r) = n.

(i) An R(MSO)-relation r(X⃗_{n}) is explicitly monadic second-order definable if it is a fact only or defined with clauses which do not contain inductive definitions and which are not directly or indirectly inductive themselves.

(ii) An R(MSO)-relation r(X⃗_{n}) is second-order definable if it uses only first-order induction, i.e., there appear only first order variables in the definition of its clauses. In particular r is monadic second-order definable if n = 1.

(iii) An R(MSO)-relation r(X⃗_{n}) is inductively second-order definable if it uses second-order induction.

Proof. Let ϕ be the formula corresponding to the definite clause definition of the R(MSO)-relation r, i.e., for all definite clauses r(X⃗_{n}) ← ψ_{i} & G_{i} in S with all ψ_{i} being MSO-constraints, all G_{i} being (possibly empty) definite clause bodies and 1 ≤ i ≤ n, in general ϕ(X⃗_{n}, X) := X(X⃗_{n}) ← (ψ_{1} & G_{1}) ∨ ⋯ ∨ (ψ_{n} & G_{n}) and α(X) = r.

(i) For facts and other non-recursively defined relations we simply give an explicit formula r(X⃗_{n}) ⟺ (ψ_{1} & G_{1}) ∨ ⋯ ∨ (ψ_{n} & G_{n}).

(ii) If the definition of the R(MSO)-relation r uses only first-order induction, ϕ is of the form ϕ(X⃗_{n}, X) with each X_{i} ∈ X⃗_{n} being only a singleton set and Γ_{ϕ}(r) = {α(X⃗_{n}) | N_{2} ⊧ ϕ[α] and α(X) = r} with fixpoint F (Γ_{ϕ}) = r. The fixpoint exists since X occurs only positively. The relation is explicitly second-order definable by the Π_{1}^{1}-formula r(X⃗_{n}) ⟺ (∀Z)[(∀y⃗_{n})[ϕ(y⃗_{n}, Z) ⇒ y⃗_{n} ∈ Z] ⇒ X⃗_{n} ∈ Z] since it defines the property to be the least relation fulfilling ϕ. Note that if n = 1 then the preceding formula quantifies only over monadic second-order variables such that the relation is monadic second-order definable.

(iii) If the definition of the R(MSO)-relation r uses second-order induction ϕ is of the form ϕ(X⃗_{n}, X) with X⃗_{n} being arbitrary (monadic) second-order variables. Then the fixpoint F (Γ_{ϕ}) exists and equals r since X occurs only positively.

We have shown above that in general inductive second-order definable relations are undecidable. But the lemma gives us one (unattractive) way to ensure the decidability of the relations we define with our programs. We have to alter the Def. 3.6 such that only one singleton variable is allowed to appear in the atoms in all directly or indirectly recursive predicates. The new relations we introduce are then limited to r^{A} ⊆ T . Obviously this gives us only the re-introduction of the notion of derivation, but not more expressive power. On the other hand, there are binary inductive definitions which are decidable. Maybe the most obvious example is a definition of proper domination via recursion on immediate domination. We have to leave this point open for further research. But results from logic programming and higher order unification related to properties such as groundness or linearity of the involved programs or queries (Devienne et al., 1994; Levy, 1996) suggest that we might be able to find an interesting subclass. Other interesting subclasses of definable relations are identified as the binary matching relations (Lautemann et al., 1995) and the binary relations recognizable by tree-walking automata (Bloem and Engelfriet, 1997). It is a question open to further research how to relate these definability results to the inductive case.

3.2.5. The Interpreter. In this section on the interpreter we discuss the constraint solver and possible optimizations. For simplicity, we choose a basic left-to-right and depth-first selection of the goals.

The desiderata for a constraint solver are twofold. Firstly it is supposed to be complete and secondly efficient. Complete means just that it can decide the satisfiability of the constraints in the domain. Efficiency is mainly achieved by being able to work incrementally. The advantages of MSO theorem provers, despite their exponential worst case behaviours, are that

• they represent assignments to the variables efficiently as tree automata

• they can be used incrementally since we can view a tree automaton as a constraint store where the conjunction with a new constraint yields a new store;

• they are efficient since goal reduction uses only conjunction (which is only polynomial);

• emptiness, i.e., satisfiability, is trivially decidable after automata construction;

• we can create a library of constraints to avoid recomputation and view this as an extension of the signature of MSO;

• the automata are a normal form.

We present the working of the desired interpreter in more detail. First of all, we single out a particular subclass of formulas by designating the atomic satisfiable formulas as normal constraints. Note that this includes all formulas which can be compiled into a minimal, non-empty tree automaton.

In the constraint solving step we actually compute the conjunction of the input automata to a new tree automaton and decide the emptiness of its language. This ensures that if the clause is applicable we can continue to work with normal constraints.

To ensure normality through the entire computation we demand that both goals and definite clause specifications introduce and utilize only normal constraints. A normal goal G is a goal which contains only one normal MSO-constraint and a normal definite clause specification S is one in which all constraints in the clauses of S are normal. This does not impose any additional burden on the programmer since we can turn any definite clause specification into a normal one by compiling the necessary constraint if it is complex and by just eliminating the clauses containing unsatisfiable constraints.

The interpreter tries to solve a conjunction of normal MSO-constraints immediately to test each goal reduction step. If it can compute a new normal MSO-constraint the clause might be applicable. If not, we can discard this clause since it will not produce any solutions.

We only have a very preliminary prototype to test our ideas. We had to use our own implementation of a compiler since MONA can – at the moment at least – not be used inside other programs. Therefore we cannot make any claims to the practicality of the proposed interpreter.

A basic depth-first, left-to-right interpreter using the process sketched above does not use any number of optimizations which are available in the literature on constraint logic programming. We kept it deliberately simple, so that its behaviour is easily understandable. Nevertheless it is necessary to extend the scheme we proposed to get more benefits from using constraint logic programming. In the following paragraphs we will sketch some of the possible directions this might take.

Keeping within the Höhfeld and Smolka scheme, we can actually augment the system by including garbage collection and a type discipline. Garbage collection could be integrated since the scheme allows existential quantification in the relational extension. We could bind variables in places where they are not needed any more.

The second extension inside the scheme allows the typing of variables with MSO constraints as in standard imperative programming languages. The major advantage of the typing is that we can infer whether the specification contains errors by a well-typedness check. The definitions in Höhfeld and Smolka are general enough that they subsume our particular case.

Another possible optimization is the use of charts to record computations. In connection with the library of compiled relations, this might save the recomputation of some constraints. Obviously it involves checking whether the current constraint solving has been done before. But if we store the computations in a table, the lookup is not costly and therefore preferable to the recomputations involved in checking satisfiability.

A major change giving us a nice optimization would be the change to a concurrent framework. Maybe the most complete presentation of this can be found as the ask and tell framework developed in Saraswat (1993). Instead of only telling constraints, i.e., adding them to the constraint store, we can also ask whether a constraint is entailed by it. This amounts to checking the satisfiability of the constraint store conjoined with the negation of the constraint. Obviously this extension can be handled by the constraint solver. But to our knowledge there are no denotational semantics for this framework. We have to give up the nice properties of logic programs to coincide on their operational and declarative semantics. On the other hand, the framework allows to delay goals until the variables are sufficiently instantiated. Since we are considering P&P-based parsing, this seems to be a desirable property of our formalism.

A completely different source for optimizations can be found in the direction of static or offline program transformations. These techniques try to modify the program to optimize the runtime behaviour under a given selection strategy. Possible tasks include a data flow analysis of the program with the succeeding reordering of the literals in the bodies of clauses according to their determinacy (Strzalkowski, 1994). Another technique involves the addition of new predicates to allow bottom up execution of the program, called magic compilation (Ramakrishnan, 1991). Again, those approaches are not of immediate concern, but might be applicable to further improve execution of our programs.

4. Some Applications of R(MSO)

In this section we are going to sketch some applications of R(MSO). As noted in the introduction a number of natural language formalisms adopt the constraint-based view. A grammar is treated as a (finite) set of constraints which have to be satisfied. In particular, in MSO the grammar is a k +1-ary relation describing a tree T and its k labels. In general, the parsing problem is to find the well formed trees spanning the input string. In our context, if we can generate an automaton covering an entire grammar, parsing means the relativization of the grammar automaton to the actual input sentence, i.e., conjoining a description of the input with the grammar. The input has been recognized iff the resulting automaton is non empty. The automaton represents the parse forest, but it does not output any trees. To achieve this, we have to run the automaton as a generator and record the structure of the run and the labels used. Remember that due to our encoding of the relations as a closure instead of having a unique minimal representative, the number of trees we can generate may be infinite. The same is true for the answers produced by R(MSO).

The following discussion should not be misunderstood as a serious attempt to define a parser. We are not concerned with efficiency or the presentation of even a complete algorithm. Rather we want to show the suitability of R(MSO) to linguistic processing by exploiting facets of the parsing problem. Note that an explicit definition corresponds directly to a fact.

4.1. Pure Parsing. As discussed in Sec. 2.3, one could use a complete formalization of the grammar in MSO for parsing directly via theorem proving. Assume for example that Gram(X) encodes Roger’s formalization of Rizzi’s ideas. Then the parsing problem can be stated as a simple R(MSO) goal, too. We name this approach pure parsing. Remember that we ignore the global variables denoting features/labels in the head of the formula.

We have to add one detail to connect pure parsing and theorem proving. We have to relate the input description to the set T ree encoding the parse tree. This is done with the MSO-constraint Yield and an MSO set variable labeling nodes with an empty phonology (Empty). Naturally, its distribution has to be constrained further.

\begin{aligned}Yield(S, T) ⟺^{def} & (∀x ∈ T)[((¬(∃y ∈ T)[x ◁ y]) ⇔ \\ & (x ∈ S ∨ x ∈ Empty)) ∧ \\ & ¬(x ∈ S ∧ x ∈ Empty)] \\ & ∧ S ⊆ T \end{aligned} (15)

A set of nodes forms the yield of a (finite) tree if it has as members exactly the nodes from its frontier with a nonempty phonology. We combine the Yield and the Gram constraints to obtain the final one.

(16)  Parse(In, T ree) ⟺^{def} Yield(In, T ree) ∧ Gram(T ree)

The corresponding definite clause parse is trivially identical with the definition in the preceding equation.

We treat the input string In as a set of nodes labeled with the words as monadic properties and linearly ordered by precedence. Additionally, we exclude any domination relations within In and further nodes with a nonempty phonology. This is clearly definable and serves as the initial constraint in our goal. Suppose we want to recognize the input Jan sees Lena. Then the (simplified) goal looks as follows:

\begin{matrix}← & parse(In, T ree) & \\ \{(∃x, y, z ∈ In)[Jan(x) ∧ Sees(y) ∧ Lena(z) ∧ x ≺ y ≺ z ∧ \\ (¬∃u, v ∈ In)[u ◁^{+} v] ∧ \\ (∀w ∈ In)[(w ≉ x ∧ w ≉ y ∧ w ≉ z) ⇒ \\ Empty(w)]]\} \end{matrix} (17)

Naturally, we can generate these descriptions of the input from a more standard representation, e.g., lists of words, automatically.

4.2. Parsing with R(MSO) as a Programming Language. The other extreme would be not to use any MSO-based grammar formalizations, but to define data types and programs as for any other logic programming language. As a simple example, recall the definition of finite lists and append (see Sec. 3.2.4). With these datatypes we can then use R(MSO) and its interpreter as a programming language and implement (standard) parsing algorithms.

4.2.1. Johnson (1995). Using R(MSO) as a programming language, we can capture some of Johnson’s proposals (Johnson, 1995) more or less directly by specifying the modules in R(MSO) and using the underlying tree as our datastructure for recursion. His parse relation holds of a string and a tree in case it obeys the xbar theory, the ecp^{3} and the string is the yield of the tree, see Fig. 8. We take the liberty of presenting the constraints not as a single normal constraint but rather in a more informative manner representing all necessary conditions. But one could compile this conjunction into a new normal constraint on two variables without problems, i.e., String and Tree(X, Y). We assume that all our MSO variables, with the exception of the input which is constrained to be a string, i.e., a list of the leaves of a tree, are constrained to be trees, i.e., dominance-connected, rooted sets.

As an example, we will work through the definition of the xbar predicate. First, we have to define some new MSO-constraints though. The definition of a root node is relative to a specific set, x is the root of X.

(18)  Root(X, x) ⟺^{def} (x ∈ X) ∧ (∀y)[y ∈ X ⇒ x ◁^{∗} y]

3The ecp deals with the distribution of the empty nodes in the tree. We leave out its definition here since it can be captured using similar techniques as in the examples we will give, for more details see Morawietz and Cornell (To appear).

parse(W ords, T ree) ←
{String(W ords) ∧ Tree(T ree)} &
xbar(T ree) &
ecp(T ree) &
yield(W ords, T ree)

Figure 8. parse from Johnson (1995)

lexicon(x) ⟵ {Sees(x) ∧ V (x) ∧ 3rd(x) ∧ … }
lexicon(x) ⟵ {Jan(x) ∧ N(x) ∧ Masc(x) ∧ … }
lexicon(x) ⟵ {Lena(x) ∧ N(x) ∧ F em(x) ∧ … }
⋮

Figure 9. An R(MSO)-definition of the lexicon

The definition of daughters in (19) just picks those nodes which are the immediate daughters from the model. Since it is defined for models consisting of binary branching trees, it specifies the sole two daughters. By the use of ≺ between y and z we do not only order them, but force them to be different nodes, too.

(19)  Dtrs(x, y, z) ⟺^{def} x ◁ y ∧ x ◁ z ∧ y ≺ z
(20)  Subtree(X, y, Y) ⟺^{def} y ∈ X ∧ (∀x ∈ X)[y ◁^{∗} x ⇔ x ∈ Y]

The subtree predicates are such that in the first one Y is the subtree of X rooted in y. In the second one x is the root of X with daughters y and z which are the roots of Y and Z respectively.

Subtrees(X, x, Y, y, Z, z) ⟺^{def} Root(X, x) ∧ Dtrs(x, y, z) ∧
Subtree(X, y, Y) ∧ Subtree(X, z, Z)

(21)

Coming back to an issue raised in Sec. 2.3 in (5), let us note that in the CLP extension, we can avoid having to compile the lexicon as one constraint by having facts for each lexical entry separately (see Fig. 9). Naturally this is highly nondeterministic and shifts the burden to the CLP interpreter. But at least the approach makes the problem feasible. xbar(X) ← ; {Sing(X)} & ; lexicon(X)

xbar(X) ←
{Subtrees(X, x, Y, y, Z, z)} &
local xbar(x, y, z) &
xbar(Y) &
xbar(Z)

Figure 10. xbar following Johnson (1995)

local xbar(x, y, z) ← CP (x) ∧ W h(y) ∧ C1(z) ∧ y ≺ z
local xbar(x, y, z) ← CP (x) ∧ C(y) ∧ IP (z) ∧ y ≺ z
local xbar(x, y, z) ← C1(x) ∧ C(y) ∧ IP (z) ∧ y ≺ z
⋮

Figure 11. local xbar following Johnson (1995)

Now we come back to the definition of the X-Bar principle itself. The first clause of xbar in Fig. 10 allows nodes which appear in the lexicon. This includes those leaves of the parse tree with an empty phonology under the assumption that we include traces, PRO and other phonologically empty nodes with entries in the lexicon. The second one forces each local tree to satisfy some local xbar constraints and the immediate subtrees to satisfy xbar. For simplicity, the local xbar predicate consists just of phrase structure rules (see Fig. 11).

The predicate Yield was already defined in (15). We could have used the yield clause before the other predicates to reduce the search space, but since we are not really concerned with efficiency here, we stuck as closely as possible to Johnson’s definition.

Furthermore, the general approach of constraining variables to a range of particular values allows the specification of data types. We can define them in the constraint language without having to explicitly include a type discipline. We simply attach additional conditions to every variable appearing in a clause. Consider as an example again the definition of

lex(X) ← ; {Elist(X)}

lex(X) ←
{Hd(x, X) ∧ Tl(X, Y)} &
lexicon(x) &
lex(Y)

Figure 12. An R(MSO)-definition of lex

the lexicon. Instead of anchoring xbar with it, we could have used as an alternative an atom lex(W ords) in the definition of parse in Fig. 8 which would recurse on the input string, see Fig. 12.

In the definition one can see that we split the work into subtasks making sure that each terminal node is labeled with a lexical word and the necessary lexical features. This presupposes that we alter the definition of lists we gave in (12) such that they are precedence ordered instead of being ordered by dominance.

The advantage of guiding the search by the use of available data structures is readily apparent. What we did here for lists and for the set of nodes representing the tree avoids the need to compile the entire available information into one automaton which might be too big for present day computers to handle.

Additionally, we can use this implicit typing to choose a more specific interpretation for the variables. During the presentation of MSO we already discussed following Rogers and Rizzi (and others) in their assumption that the basic entities a P&P theory deals with are not longer nodes, but categories. Now we can constrain the variables in R(MSO) to range over categories so that they become the basic components of a theory.

An even better way to guide the search would be to check for the information content of the variables to be constrained and make the further action dependent on that. But in our present framework we cannot check for entailment and then act appropriately on the result. We can reject the alternative, but this might not be what we want to do. It would be more appropriate to keep the task in a queue and execute it when the variable becomes “specific” enough. This can be done in a concurrent framework which we cannot discuss further here.

xp(x) ←

{Max(x) ∧ Proj(x, y) ∧ (∃X)[Dts(x, X) ∧ Hd(y, X) ∧ Tl(X, Z)]} &

x1(y) &
specs(y, Z)

Figure 13. xp following Fong (1991)

4.2.2. Fong (1991). The next example is taken from Fong (1991). He uses phrase structure rules with restrictions attached to them. We can state his rule that an XP rewrites to an X1 followed by its specifiers if XP is a maximal projection and X1 immediately projects to XP as in Fig. 13. Again, we need some auxiliary definitions. We follow Fong in them, although we think they are pretty ad hoc. Max identifies those nodes which are maximal projections, Proj expresses that two nodes are projections of each other and Dts just collects all daughters of x in a set ordered by precedence.

(22)  Max(x) ⟺^{def} x ∈ NP ∨ x ∈ V P ∨ …
(23) Proj(x, y) ⟺^{def} (x ∈ NP ⇔ y ∈ N1) ∨ (x ∈ V P ⇔ y ∈ V 1) ∨ …
(24) Dts(x, X) ⟺^{def} (∀y)[x ◁ y ⇔ y ∈ X]

Since we are dealing with rules on nodes here, we do not get an accepted tree in the end. If we want to have an explicit parse tree, we have to either follow standard parsing techniques and record the rule applications or alternatively to include a particular subset in all the predicates such that quantification is always relative to it. It represents the parse tree in the end.

4.3. Nonlocal Constraints. All of these examples are just supposed to show how powerful R(MSO) is. We can cope with most of the standard approaches, although it does seem to be a bit cumbersome at times. But the real advantage of MSO and R(MSO) lies in the ability to directly express nonlocal constraints. Following an argument of Johnson (1995) on nonlocal constraints, we claim that they are crucial in the P&P-based approaches to natural language and the difference to other theories as for example HPSG (Pollard and Sag, 1994). This is most clearly seen in phrase structure based implementations of these theories, e.g., in ALE (Carpenter and Penn, 1998). We can see the strong locality requirements since all the feature constraints are coupled to phrase structure rules.^{4} The constraints are only concerned with a node and its immediate children. They can be checked during the (standard) parse tree construction. Naturally, this requires some encoding of the nonlocal dependencies for example between a filler and its gap via slash features. Since this seems to be more a problem of memory management and implementation techniques than of linguistic analysis, we strive to avoid it.

The relaxation of the locality conditions is realizable in R(MSO) directly since the variables range over sets of nodes. This is where we gain on Johnson’s approach. Where he pursues the alternatives of coroutining and compilation into local constraints, we can use the principles directly on sets of nodes. And furthermore, we have quantification available in the constraint language MSO so that we can express statements as the following: “there has to exist a trace somewhere down in this subtree”.

One approach to parsing which reflects the modular nature of P&Ptheories would be the incremental narrowing of the constraint store by passing the set of nodes representing the tree to be constructed through the various modules. This is an improvement on the general generate and test method since we do not have to construct a particular tree which has to be validated. We limit the range of values the variable can take, although, on the surface, it looks much like the standard Prolog approaches to P&P-parsing. But we are not limited to the construction of any local dependencies since we are directly passing on the constraints on the entire tree. In fact, we modify a tree automaton representing the constraint store. Even with a definition as given in Fig. 8, we can almost use the pure MSO approach, only modified to work incrementally on a particular input. Instead of using the tree for recursion we can just conjoin more an more separately compiled modules. This becomes especially interesting if we consider using an approach to the lexicon as the one given in Fig. 12 since we do not have to specify xbar with definite clauses any more.

As mentioned above, the other area of advantages of MSO-constraints is in the specification of the existence of further information to be found. This is most easily be illustrated in a phrase structure based approach: we can now express the relation between a filler and its gap directly. Assume for example that we have a definite clause which is a phrase structure rule combining a +WH element with a VP. We make sure that indeed the VP contains the appropriate trace without having to specify a passing mechanism like slash features by quantifying over the trace, see Fig. 14.

4In HPSG itself they are not bound to the ID schemata, but one still has to express explicit paths of features to find the desired values.

s(X) ←

{(∃x, y, z)[Subtrees(X, x, Y, y, Z, z)] ∧

(∃z)[Z(z) ∧ T race(z) ∧ Feq(z, Y)]} &

np_{wh}(Y) &

vp(Z)

Figure 14. Nonlocality in a phrase structure rule

The clause finds and recurses on the subtrees if there exists a trace in Z such that it agrees on the relevant features with the extracted WH-phrase.

An example for the use of quantification in the guard of an R(MSO)- clause which is more suitable for P&P approaches can be found in formalizations of the binding principles. We can state a constraint that for all appropriate nodes in the scope of the current node, a principle has to hold. More concretely, whenever we find a proper noun phrase we stipulate that it may bind all appropriate anaphoric noun phrases if it occurs in their governing category. This is a simplified version of Principle A of the Binding Theory. A very simple formalization of such a constraint – ignoring all the inherent problems of the binding theory – may look as given below. We assume the existence of predicates Anaphor to pick out anaphoric noun phrases, Gov-Cat which encodes the governing category and A-Bind ensuring that x A-binds y.

NP (x) ⇒
((∀y)[(Anaphor(y) ∧ (∃X)[Gov-Cat(y, X) ∧ X(x)])
⇒ A-Bind(x, y)])

(25)

5. Summary

We presented in this paper the first step towards MSO-based constraint logic programming. We applied the Höhfeld and Smolka scheme to MSO logic on trees resulting in the the constraint logic programming language R(MSO). The scheme gives us a sound and complete operational semantics. We presented an outline for a basic interpreter using goal reduction and constraint solving. Since we have specialized constraint solvers for MSO formulas, e.g., MONA, it is possible to develop a straightforward prototype.

One advantage we see in the logic programming approach consists in the operational interpretation which can be given to the relational extensions of our constraint language. We have shown how to leave the pure model theory towards a more processing oriented view. In fact, we defined a programming language which can directly use linguistic primitives. A further advantage is that we are able to apply techniques from computer science to further develop a useful tool for natural language processing.

We raised some topics and problems in the paper which are yet to be answered. There are three major areas we have to investigate further. The first is concerned with formal issues connected with R(MSO). If we want to extend our relational constraint language with negation it seems to be necessary to clarify which alternatives there are compared to the standard approaches. Standardly, compactness is a condition to be met if the desideratum of an agreement of operational and denotational semantics for a CLP language with negation is to be achieved. Compactness fails in MSO since finiteness is definable. Another interesting point seems to be the generative capacity of the relational extension. Considering the discussion on definability in Sec. 3.2.4, the relational extension gains in power since it involves second-order inductive definitions. It is especially interesting whether we can find a mild, decidable extension, e.g., to the indexed languages. In that case the objection that MSO cannot handle all natural languages, i.e., Swiss German or Dutch, could be invalidated.

The second direction is concerned with the further development and extension of the R(MSO)-interpreter. For example, we are interested in whether there still exists a denotational interpretation for a concurrent framework; and if this is the case whether the denotational and operational semantics still coincide as for standard logic programming. An issue raised briefly in Saraswat (1993) is the use of domain theory in the guise of information systems for the development of the semantics. We believe that this also is an interesting area for further research.

The third direction is probably the most difficult. We have to spend more time on the development of R(MSO)-based formalizations of P&Ptheories. We hinted at some details, but naturally this does not provide proof for a conclusive realization of the principles and modules. We do not doubt that a formalization can be found since R(MSO) seems to be powerful enough. But it also seems to be nontrivial to come up with a proper and complete implementation which uses the features MSO and R(MSO) offer. Especially the investigation into the successor of GB, the minimalist program (Chomsky, 1995) seems to be promising, since it also combines procedural and representational techniques.

References

Andersen, H. R. (1996). An introduction to binary decision diagrams,

Course Notes, Technical University Denmark. Ayari, A., Basin, D. and Podelski, A. (1998). LISA: A specification lan-

guage based on WS2S, in M. Nielsen and W. Thomas (eds), Computer Science Logic, CSL’97, number 1414 in LNCS, Springer.

Basin, D. and Klarlund, N. (To appear). Automata based symbolic reasoning in hardware verification, The Journal of Formal Methods in Systems Design.

Bloem, R. and Engelfriet, J. (1997). Characterization of properties and relations defined in monadic second order logic on the nodes of trees, Technical Report 97-03, Leiden University.

Büchi, J. (1960). Weak second-order arithmetic and finite automata, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 6: 66–92.

Carpenter, B. and Penn, G. (1998). ALE: The attribute logic engine, Version 3.0 Beta, User manual, Laboratory for Computational Linguistics, Carnegie Mellon University.

Chomsky, N. (1981). Lectures on Government and Binding, Dordrecht:

Foris. Chomsky, N. (1995). The Minimalist Program, Vol. 28 of Current Studies

in Linguistics, MIT Press. Devienne, P., Lebg̀ue, P., Parrain, A., Routier, J. and Würtz, J.

(1994). Smallest horn clause programs, Journal of Logic Programming 19/20: 1–41.

Doner, J. (1970). Tree acceptors and some of their applications, Journal

of Computer and System Sciences 4: 406–451. Fong, S. (1991). Computational Properties of Principle–Based Grammat-

ical Theories, PhD thesis, MIT. Frank, R. and Vijay-Shanker, K. (1998). TAG derivation as monotonic

c-command, Proceedings of the Fourth Workshop on Tree-Adjoining Grammars and Related Frameworks TAG+98, Philadelphia, PA. Extended Abstract.

Gécseg, F. and Steinby, M. (1997). Tree languages, in G. Rozenberg and A. Salomaa (eds), Handbook of Formal Languages: Beyond Words, Vol. 3, Springer.

Hanschke, P. and Würtz, J. (1993). Satisfiability of the smallest binary

program, Information Processing Letters 45(5): 237–241. Höhfeld, M. and Smolka, G. (1988). Definite relations over constraint

languages, LILOG Report 53, IBM Deutschland, Stuttgart, Germany.

Huybregts, R. (1984). The weak inadequacy of context-free phrase structure grammars, in de Haan, Trommelen and Zonneveld (eds), Van Periferie naar Kern, Foris, Dordrecht, pp. 81–99.

Jaffar, J. and Maher, M. J. (1994). Constraint logic programming: A

survey, Journal of Logic Programming 19/20: 503–581. Johnson, M. (1995). Constraint-based natural language parsing, Eu-

ropean Summer School in Logic, Language, and Information (ESS-LLI ’95), Barcelona, Course notes.

Kayne, R. S. (1994). The Antisymmetry of Syntax, Vol. 25 of Linguistic

Inquiry Monographs, MIT Press. Kelb, P., Margaria, T., Mendler, M. and Gsottberger, C. (1997). Mosel:

A flexible toolset for monadic second-order logic, in E. Brinksma (ed.), TACAS ’97 Workshop, number 1019 in LNCS, Springer, pp. 183–202.

Klarlund, N. (1998). MONA & Fido: The logic-automaton connection in practice, in M. Nielsen and W. Thomas (eds), Computer Science Logic, CSL’97, number 1414 in LNCS, Springer.

Klarlund, N. and Møller, A. (1998). MONA Version 1.2 User Manual, BRICS Notes Series NS-98-3, Department of Computer Science, University of Aarhus.

Lautemann, C., Schwentick, T. and Thérien, D. (1995). Logics for contextfree languages, in L. Pacholski and J. Tiuryn (eds), Computer Science Logic CSL ’94, number 933 in LNCS, Springer, pp. 205–216.

Levy, J. (1996). Linear second-order unification, in H. Ganzinger (ed.), Proceedings of the 7th International Conference on Rewriting Techniques and Applications (RTA-96), number 1103 in LNCS, Springer, pp. 332–346.

Lloyd, J. (1984). Foundations of Logic Programming, Springer Verlag. Morawietz, F. and Cornell, T. (1997). On the recognizability of rela-

tions over a tree definable in a monadic second order tree description language, Arbeitspapiere des SFB 340 85, Universität Tübingen.

Morawietz, F. and Cornell, T. (To appear). The logic-automaton connec-

tion in linguistics, Proceedings of LACL 1997, LNAI, Springer. Moschovakis, Y. N. (1974). Elementary Induction on Abstract Structures,

North-Holland, Amsterdam. Pollard, C. J. and Sag, I. A. (1994). Head-Driven Phrase Structure Gram-

mar, University of Chicago Press and CSLI Publications. Post, E. (1946). A variant of a recursively unsolvable problem, Bulletin

of the AMS 52: 264–268. Rabin, M. O. (1969). Decidability of second-order theories and automata

on infinite trees, Transactions of the AMS 141: 1–35.

Ramakrishnan, R. (1991). Magic templates: A spellbinding approach to

logic programs, Journal of Logic Programming 11: 189–216. Rizzi, L. (1990). Relativized Minimality, MIT Press. Rogers, J. (To appear). A Descriptive Approach to Language-Theoretic

Complexity, Studies in Logic, Language and Information, CSLI. Saraswat, V. A. (1993). Concurrent Constraint Programming, MIT Press. Shieber, S. M. (1985). Evidence against the context-freeness of natural

language, Linguistics and Philosophy 8: 333–343. Strzalkowski, T. (1994). A general computational method for grammar

inversion, in T. Strzalkowski (ed.), Reversible Grammars in Natural Language Processing, Kluwer, pp. 175–200.

Thatcher, J. and Wright, J. (1968). Generalized finite automata theory with an application to a decision problem of second-order logic, Mathematical Systems Theory 2(1): 57–81.

Index

(M,[[−]]^{I}), 16 MSO, 16 L^{2}, 7 L_{K,P}^{2} , 6, 17 R(MSO), 18 S-answer, 22 MONA tool, 11, 28

⟶^{r}_{S,V}^{∗} , 22

⟶^{r}_{S,V} , 22

Andersen (1996), 12 Ayari et al. (1998), 6 Büchi (1960), 4 Basin and Klarlund (To appear), 8 Bloem and Engelfriet (1997), 27 Carpenter and Penn (1998), 35 Chomsky (1981), 1 Chomsky (1995), 38 Devienne et al. (1994), 24, 26 Doner (1970), 4, 9 Fong (1991), 35 Frank and Vijay-Shanker (1998), 6 Gécseg and Steinby (1997), 2 Hanschke and Würtz (1993), 23 Huybregts (1984), 15 Höhfeld and Smolka (1988), 1, 2, 15 Jaffar and Maher (1994), 16 Johnson (1995), 31, 35 Kayne (1994), 6, 7 Kelb et al. (1997), 8 Klarlund and Møller (1998), 12 Klarlund (1998), 4, 8 Lautemann et al. (1995), 27 Levy (1996), 27 Lloyd (1984), 14 Morawietz and Cornell (1997), 4, 12 Morawietz and Cornell (To appear), 8,

12, 31 Moschovakis (1974), 24 Pollard and Sag (1994), 35 Post (1946), 23 Rabin (1969), 4 Ramakrishnan (1991), 29 Rizzi (1990), 6 Rogers (To appear), 1, 6, 13, 24 Saraswat (1993), 29, 38 Shieber (1985), 15 Strzalkowski (1994), 29 Thatcher and Wright (1968), 4, 9

append

in R(MSO), 21 assignment, 5 assignment tree, 5

binding, 37

c-command asymmetric directed, 7 category based, 13

categories, 12

closure under intersection, 18 under renaming, 18 CLP-interpreter, 27 coding of variables, 9 combinatorial explosion, 10, 11 completeness, 23 constraint language, 16

decidability constraint language, 18 of R(MSO), 23 of WS2S, 9 definability

R(MSO)-relations, 25

explicitly monadic second-order, 25 explicitly monadic second-order, 8 inductive, 25 inductively second-order, 25 monadic second-order, 25 second-order, 25

definite clause specification, 19

normal, 27 definiteness theorem, 20

free variables in MSO, 16 in R(MSO), 18

goal reduction, 22 grammar, 5, 29

lexicon in L^{2}, 11 in R(MSO), 32, 34

lists in MSO, 20

model

of S, 19 MSO logical language, 4

normal constraints, 27

parse in R(MSO), 36 Johnson, 31 pure, 30

parsing problem, 11, 29 PCP, 23 phrase structure rules

Fong, 34 nonlocal conditions, 36

relational constraint language

R(MSO)-interpretation, 18 relational constraint language

R(MSO)-constraints, 18 renaming, 17

satisfiability in R(MSO), 23 in MSO, 5

solution

of a constraint, 16 soundness, 22 structure

for L_{K,P}^{2} , 8 for WS2S, 5 of MSO, 16

theorem proving, 11 tree

binary, 2 labeled, 5

tree automaton, 3

for asymmetric directed c-command,

10 for category based c-command, 14

variant, 17

X-Bar Johnson, 32 Rogers, 12 yield, 30 Seminar für Sprachwissenschaft, SFB 340, A8, University of Tübingen, Wilhelmstr. 113, 72074 Tübingen, Germany

E-mail address: frank@sfs.nphil.uni-tuebingen.de