Bericht Nr. 86, Februar 1997

ISSN 0947-6954/97

Arbeitspapiere des Sonderforschungsbereichs 340

Sprachtheoretische Grundlagen für die Computer linguistik

Frank Morawietz :

Monadic Second Order Logic, Tree Automata and Constraint Logic Programming

Universität Stuttgart Universität Tübingen Deutschland Informationssysteme GmbH Arbeitspapiere des SFB 340

Bericht Nr. 86, Februar 1997

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 assignment trees satisfying the formulas. Since this allows a compact and efficient representation of constraints, we can use mso theorem provers as constraint solvers for the clp interpreter. Building on the detailed investigation of mso logic in Rogers (1994) as a tree description language in the Principles and Parameter (P&P) paradigm, we present as motivation and applications details from the realm of P&P-based parsing.

1. Introduction

Model theoretic techniques are used in formalizations of a number of approaches toward theories about natural language. Maybe most notably in feature logics (King; 1989; Carpenter; 1992) for Head-Driven Phrase Structure Grammar (Pollard and Sag; 1994); modal logic (Blackburn and Meyer-Viol; 1994) for Lexical-Functional Grammar (Kaplan and Bresnan; 1983); or full first order predicate logic (Stabler; 1992), monadic second order logic (Rogers; 1994) or again modal logic (Kracht; 1995) for the

To appear in: Kolb, H.-P. & U. Mönnich (eds.), The Mathematics of Syntactic Structure.

The research presented in this report was sponsored by Teilprojekt A8 of the Sonderforschungsbereich 340 of the Deutsche Forschungsgemeinschaft. 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/97 \begin{matrix}c \\ ◯ \end{matrix}1997 Der Autor

Principle and Parameter (P&P) approaches in the Government and Binding tradition (Chomsky; 1981).^{1} All of these constraint-based formalisms characterize objects with logical description languages declaratively., i.e., without the specification of details on the generation of the 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.

In this paper we bridge the gap between the two by exploiting the connection between constraints in monadic second order (mso) logic on (finite binary) trees and tree automata. Our purpose is twofold. Firstly we discuss the operational interpretations of mso logic. Since the solutions to constraints expressed in monadic second order logic are represented by tree automata recognizing the assignment trees satisfying the formulas, we can use the automata as the operational interpretation of out formalism. 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. We want to extend the computational power since mso logic characterizes the strongly context-free languages, but natural languages are generally believed to be higher in the Chomsky hierarchy (Shieber; 1985; Huybregts; 1984). Inductive definitions can be seen as special cases of constraint logic programming (clp) clauses. The specification of a clp interpreter reintroduces the operational concept of derivation of a (representation of a) structure. More concretely, we propose the embedding of mso logic into the constraint logic programming scheme of Höhfeld and Smolka (1988).^{2} The extension gives us an even more powerful and flexible language and allows us to guide the compilation process with appropriate programs.

The paper is organized as follows. In the first section we review the results on mso logic and tree automata 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 the relational extension, discuss its properties and present some examples. In the last section, we argue for the usefulness of the approach with examples from the realm of 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 (1984).

1We do not claim that this enumeration is in any way complete or representative.

2We are aware that a constraint logic programming approach toward P&P has been taken in Hathout (1992), too. But unfortunately the thesis is in French and therefore not completely accessible to us.

Assume an alphabet Σ = Σ_{0} ∪ Σ_{2} with Σ_{0} = {λ} and i the arity of the elements in Σ_{i}. The set of binary trees T_{Σ} over Σ is the set of terms build 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 Σ. 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 \{\underline{0}, \underline{1}\} only.

As an example consider the alphabet with Σ_{2} = {A}. Some trees derived from that alphabet are shown in figure 1. Note that λ serves as

A  A  A  A
λ λ  A λ  A  A  λ  A
λ λ  λ λ λ λ  A λ
λ λ

Figure 1. Some example trees

a terminator and has no content.

A deterministic (bottom-up) tree automaton 𝔄 on binary trees is a tuple ⟨A, Σ, a_{0}, F, α⟩ with A the set of states, a_{0} ∈ A the initial state, F ⊆ A the final states and α : (A×A×Σ) → A the transition function. 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_{Σ}. 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).

Since tree automata will be used later on, we present an example here. The automaton in figure 2 recognizes, among others, the trees given in 𝔄 = ⟨{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 2. A simple tree automaton

figure 1. This admittedly very simple tree automaton recognizes all binary trees whose interior nodes are labeled with A. 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, determinization and minimization. Most of the constructions are adaptions from the corresponding ones on finite state automata. We use them to parallel the connectives and quantifiers from our logic. More details on both the specification and implementation of the tree automata and their constructions can be found in either Morawietz and Cornell (1996) or Henriksen et al. (1995) and Biehl et al. (1996).

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 an interesting descriptive complexity result. It characterizes exactly the strongly context-free languages.

The techniques we are using come originally from an old result in logic, that the weak mso theory of two successor functions (WS2S) is decidable (Thatcher and Wright; 1968; Doner; 1970). A “weak” second order 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.^{3} The 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.

3All 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.

The proofs of these decidability results are inductive on the structure of mso formulas. Therefore 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. We will see how this is done in the next section, but the point can be appreciated immediately. For example, Niehren and Podelski (1992) have investigated the usefulness of these techniques in dealing with 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 (1994) has developed a language rich in long-distance 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, the automaton for Kayne-style 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 (1995).

A mso logical language has a syntax of both first and second order quantification, 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 build as usual. So we deviate from first order logic by the use of monadic second order variables and quantifiers. To create a tree description logic we fix the domain of the interpretation to trees and add constant binary relations to the syntax which will be interpreted as the successor functions. Due to the inductive proof we can also add any desired mso definable relation.

For the structure of WS2S, we are going to assume a tree domain with the extension of (at least) the two successor functions. These correspond intuitively to the relations of left and right daughter. Then the structure can be extended with the interpretations of the extra relations we want to use. We will call the structure of WS2S N_{2}.

Intuitively, mso predicates pick out sets of nodes. We can think of them as labeling the nodes. Therefore, mso logic on trees does give us the power to specify constraints on labeled trees. Each formula represents a constraint on the valuation of its free variables which is determined by the assignment of the variables to (sets of) nodes. 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 (sets of) nodes in a tree, we will sometimes call them assignment trees.

2.2.1. An Example Language: L_{K,P}^{2} . We draw our examples from tree description logics used in the P&P paradigm. In particular L_{K,P}^{2} , a logic proposed in Rogers (1994), 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 thesis most of the proposals made in Relativized Minimality by Rizzi (1990).^{4}

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 and added, e.g., proper precedence to express ordering information. We parameterize the language with both individual and predicate constants.

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

Occasionally we use L_{∅,∅}^{2} and refer to it as L^{2}. The change does not limit the power of the language since we can always encode both the predicate and individual constants as free variables. Since L_{K,P}^{2} has set valued variables only, we have to enforce that the variables denoting individuals are of cardinality 1 as given as an example below in equation (2). We deviate slightly from Rogers’ definition of the language in that we include ∈ explicitly. Again, nothing substantial is changed by this.

We will freely use appropriate symbols for standard combinations of the boolean operators, for example ⇒, ≉, ⇔, … As an example for relations we can define with this language, take the subset or equal relation in equation (1), the constraint for a set to contain exactly one member in equation (2) and, more linguistically motivated, the formula denoting the relation of directed asymmetric c-command^{5} in the sense of Kayne (Kayne; 1994), see equation (3).

4L_{K,P}^{2} is not limited to binary finite trees. Rogers actually allows for the full power of Rabin’s result to be used.

(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_{1}, x_{2}) ⟺^{def} & ¬(x_{1} ⊲^{∗} x_{2}) ∧ ¬(x_{2} ⊲^{∗} x_{1}) ∧ x_{1} ≺ x_{2} ∧ \\ & (∀x_{3})[x_{3} ⊲^{+} x_{1} ⇒ x_{3} ⊲^{+} x_{2}] \end{aligned} (3)

The definition in equation (3) specifies that two nodes asymmetrically c-command each other iff neither dominates the other, they are not identical, x_{1} precedes x_{2} and all x_{3} which properly dominate x_{1} properly dominate x_{2}. We depict an example tree in figure 3. The dashed arrow represents the c-command relation. Note that x_{1} also c-commands y and

\begin{aligned}& x_{3} \\ x_{1} & & y \\ & z & & x_{2} \end{aligned}

Figure 3. An example for asymmetric directed c-command

z.

Models for L_{K,P}^{2} are an appropriate set of nodes, a tree domain, with relations interpreting the elements from the signature.^{6}

Example 2.2. 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⟩.

5This relation is not monadic, but reducible via syntactic substitution to a mso signature.

6We limit the structure to dominance, parent and precedence since the others can be defined in terms of them.

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 just about as complex as it is possible to be. The number of states can be in the worst case given as a function of the number of variables in the input formula with a stack of exponents as tall as the number of quantifier alternations in the formula. However, there is a growing body of work in the computer science literature (Henriksen et al.; 1995)^{7} 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 linguistic applications as well.

Nevertheless, it is attractive to have a principled means of generating automata from a constraint-based theory. 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 variable assignments have to assign sets of nodes to the variables. Doner and Thatcher & Wright 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.

More formally, let again N_{2} be the structure of WS2S and ϕ(X⃗) a formula with free variables X⃗. For each relation r(X⃗) from the signature of the mso logic, we have to define a tree automaton 𝔄^{r} recognizing the assignment tree. For each mso formula ϕ(X⃗), we can inductively build a tree automaton 𝔄^{ϕ} such that

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

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

Consider as an example the corresponding tree automaton to Kayne’s c-command relation from equation (3). It is shown in figure 4. Consider the subscripts of the variables to correspond to positions in a bitstring. A \underline{1} in position i means that the node is in set X_{i}. Roughly, these bitstrings are the alphabet the automata work on. On closer examination of the transitions, we note that we just percolate the initial state as long as we

7The given reference is to the description of the tool MONA on mso logic of strings.

There is work in progress to extend MONA to trees (Biehl et al.; 1996).

𝔄 = ⟨\{a_{0}, a_{1}, a_{2}, a_{3}, a_{4}\}, \{\underline{1}\underline{1}, \underline{1}\underline{0}, \underline{0}\underline{1}, \underline{0}\underline{0}\}, a_{0}, \{a_{3}\}, α⟩
α(a_{0}, a_{0}, \underline{0}\underline{0}) = a_{0} α(a_{0}, a_{0}, \underline{1}\underline{0}) = a_{2}
α(a_{0}, a_{0}, \underline{0}\underline{1}) = a_{1} α(a_{0}, a_{1}, \underline{0}\underline{0}) = a_{1}
α(a_{0}, a_{3}, \underline{0}\underline{0}) = a_{3} α(a_{1}, a_{0}, \underline{0}\underline{0}) = a_{1}
α(a_{2}, a_{1}, \underline{0}\underline{0}) = a_{3} α(a_{3}, a_{0}, \underline{0}\underline{0}) = a_{3}

all other transitions are to a_{4}

Figure 4. The automaton for AC-Com(x_{1}, x_{2})

find only nodes which are neither x_{1} nor x_{2}. From the initial state on both the left and the right subtree we can either go to the state denoting “found x_{1}” (a_{2}) if we read symbol \underline{1}\underline{0} or to the state denoting “found x_{2}” (a_{1}) if we read symbol \underline{0}\underline{1}. We can then percolate a_{1} as long as the other branch does not immediately dominate x_{1}. If we come into the situation that we have a_{2} on the left subtree and a_{1} on the right one, we go to the final state a_{3} which again can be percolated as long as empty symbols are read. Clearly, the automaton recognizes all trees which have the desired ccommand relation between the two nodes. But in addition to the arbitrary number of intermediate nodes, we can also have an arbitrary number of \underline{0}\underline{0} labeled nodes dominating the constellation or being dominated by it. 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.

It is obviously desirable to keep the automata as small as possible. Therefore we employ the suitably adapted minimization of finite state automata. If we think of the automata as representing knowledge of the grammatical structures we want to characterize, then the automata constructions symbolize how to combine or alter the knowledge accordingly. Especially, minimization corresponds to a generalization of knowledge.

2.4. Theorem Proving. Automated theorem proving is the standard approach to processing with constraint-based grammars. The effectiveness of 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. And an automaton recognizes the empty language (due to minimization) iff it has only an initial state which is not final. 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 a whole grammar. Unfortunately, as mentioned above, the problem to generate the tree automata from arbitrary mso formulas is highly exponential. Sources of exponentiality are the necessary determinization of automata, the cross product for the representation of the combination of the states in the transitions, and the explosion of the alphabet 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 specified a set called Lexicon via a disjunctive specification of lexical labels, e.g., Sees, and the appropriate combination of features, e.g., V. Since every feature and every lexical entry is represented with a new free set variable, the alphabet size with the encoding as bitstrings will be at least 2^{n+m}, n is the number of lexical entries and m the number of features.

For tests, we used a prototype called MoSeL (Morawietz and Cornell; 1996)^{8} which compiles the tree automata from the formulas. But it is an open problem whether the generation of a complete grammar can be handled. The question is not so much efficiency, but rather feasibility since the size of an automaton representing an entire grammar is still indeterminate.

But the tests have shown that we can compile modules and by this gain insight into parts of the formalization. For example, we have successfully compiled the tree automaton representing c-command on categories rather then on single nodes following the presentation of Rizzi’s ideas from Relativized Minimality in Rogers’ thesis. Informally, a category is a node which has been split into segments through adjunction. The definition of categories can be found in equations (6) and (7).^{9} 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) one node in every local tree has to be adjoint.

8As mentioned, we are aware of promising work in progress at the University of Aarhus on the extension of MONA under the Thatcher & Wright semantics. MONA++ tries to minimize the alphabet explosion by the use of binary decision diagrams for the alphabet representation and the quadratic blow-up in the transition table by the use of guided automata.

9We are glossing over some details, F eq ensures agreement on the relevant features; P ath can be understood as a connected ordered subgraph, and Adj is the feature

\begin{aligned}Component(X) ⟺^{def} & P ath(X) ∧ \\ & (∀x, y)[(x ∈ X ∧ y ∈ X) ⇒ F eq(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)))] \end{aligned} (6)

A category is a maximal component.

\begin{aligned}Category(X) ⟺^{def} & Component(X) ∧ \\ & (∀Y)[(X ⊆ Y ∧ Y ⊈ X) ⇒ ¬Component(Y)] \end{aligned} (7)

Building on that, we can define primitives of domination, precedence and c-command in terms of categories rather than nodes.

Categories are used in P&P approaches since for example in a WHquestion 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 figure 5 one can see that I_{j} is indeed not dominated by the category formed by the two nodes labeled C. I_{j} can c-command its trace t_{j} since all categories which dominate it, also dominate t_{j}.

As might be suspected considering equations (6) and (7), the complete presentation of the formulas encoding category based c-command is fairly complex and therefore beyond the scope of this paper.^{10} But actually, the resulting automaton is small. It has only 5 states and 15 transitions, see figure 6.

One can see from the discussions in this section that the approach of pure theorem proving 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, so far, purely model-theoretic presentation. By this we provide a way to use parts or primitives of formalizations separately by the specification of programs and gain the desired extension of the generative capacity.

denoting an adjoint node. A number of additional constraints on the distribution of adjuncts is necessary to achieve the right behaviour.

10The reader is encouraged to check the details in Rogers’ thesis.

CP

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

Figure 5. A syntax tree from Rogers (1994)

𝔄 = ⟨\{a_{0}, a_{1}, a_{2}, a_{3}, a_{4}\}, \{\underline{1}\underline{1}, \underline{1}\underline{0}, \underline{0}\underline{1}, \underline{0}\underline{0}\}, a_{0}, \{a_{3}\}, α⟩

α(a_{0}, a_{0}, \underline{0}\underline{0}) = a_{0} α(a_{0}, a_{0}, \underline{1}\underline{0}) = a_{2} α(a_{0}, a_{0}, \underline{0}\underline{1}) = a_{1} α(a_{0}, a_{1}, \underline{0}\underline{0}) = a_{1} α(a_{0}, a_{1}, \underline{1}\underline{0}) = a_{3} α(a_{0}, a_{2}, \underline{0}\underline{0}) = a_{2} α(a_{0}, a_{2}, \underline{0}\underline{1}) = a_{3} α(a_{0}, a_{3}, \underline{0}\underline{0}) = a_{3} α(a_{1}, a_{0}, \underline{0}\underline{0}) = a_{1} α(a_{1}, a_{0}, \underline{1}\underline{0}) = a_{3} α(a_{1}, a_{2}, \underline{0}\underline{0}) = a_{3} α(a_{2}, a_{0}, \underline{0}\underline{0}) = a_{2} α(a_{2}, a_{0}, \underline{0}\underline{1}) = a_{3} α(a_{2}, a_{1}, \underline{0}\underline{0}) = a_{3}

α(a_{3}, a_{0}, \underline{0}\underline{0}) = a_{3} all other transitions are to a_{4}

Figure 6. The automaton for category based c-command

3. Constraint Logic Programming

Logic programming reflects nicely the separation of the actual logic of a program and the control of its execution (a standard reference to logic programming is Lloyd; 1984). The execution method used in most logic programming (lp) languages is based on SLD-resolution. Programs in the lp paradigm are sets of clauses. One could be content with a logical interpretation. But on the other hand one wants to compute with them. So the semantics is reformulated in terms of least models and fixpoints. The programs are interpreted within Herbrand models, i.e., sets of ground atoms. The two main problems^{11} with this approach, the generate and test paradigm to find the solutions and the necessary use of uninterpreted structures only, can be overcome by the addition of constraints to the standard logic programming scheme. There are two ways to enhance logic programming languages with constraints. One is to provide specialized interpreted domains of computation, as for example done in Jaffar and Lassez (1986). The other one is concerned with the application of consistency techniques (Frühwirth et al.; 1993). In this paper we are concerned mainly with the first of these issues. The guiding of the search behaviour of the programs will be sketched briefly, but left as a topic for further research.

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 focus on just those parts of the grammar which are relevant to the actual computation instead of having to consider – and precompile – all possibilities at once. A standard interpreter, as for example the one used in Prolog (left to right, depth first search), is sufficient for the execution of one of our programs. The answer of a 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 section 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 crossserial dependencies in subordinate clauses. Cross-serial dependencies can not be formalized in mso-based approaches since their underlying structure is comparable to the copy language^{12} which is not context-free.

11There are more problems – one which deserves attention is the one of infinite computations. We do not address this issue here, but propose an approach using domain theory to remedy that (Carlson; 1991).

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. We fix the domain of computation to trees. We use this scheme as opposed to the more standard one of Jaffar and Lassez (1986) 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. If we want to use them, we can use sets with the additional constraint that they are singleton. This is the case in both mso theorem provers (MoSeL and MONA) we know of. Nevertheless, we will use as abbreviations lowercase letters x, y, … for singletons and uppercase letters X, Y, … for set valued variables. ℘(X) denotes the power set of X.

Abstracting away from the actual syntactic details, we can turn any mso logic into a constraint language. MSO will be used as a placeholder for any logic based on WS2S.

Definition 3.1. The 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.

As usual, assignments are relative to an interpretation.

Definition 3.2. Let T be a tree domain. An I-assignment is a total function α : VAR → ℘(T ). We call the set of all those mappings ASS^{I}.

We already presented the definition of an interpretation in example 2.2. We generalize it by the inclusion of a solution mapping [[−]]^{I}.

12L_{copy} = {ww | w a word}

Definition 3.3. An interpretation I of the constraint language MSO is a pair (M,[[−]]^{I}) consisting of a nonempty model M and solution mappings [[−]]^{I} : CON ⟶ ℘(ASS^{I}) such that:

1. [[−]]^{I} is a function mapping every constraint ϕ to a set [[ϕ]]^{I} of Iassignments. We call that set the solutions of ϕ in I.

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

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

Definition 3.4. The function V : CON → ℘(VAR) is defined as (R ranges over the defined relations, ∗ over binary connectives, Q over quantifiers):

V(X R Y) = {X, Y }  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.5. Let I = (M, [[−]]^{I}) with M = ⟨T , P, D, L⟩ a model for L^{2} be an interpretation and let α_{\frac{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 X being VAR, CON, V and INT as defined. The denotation function [[−]]^{I} 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} − [[ϕ]]^{I}
[[∃X[ϕ]]]^{I} = \{α | α_{\frac{X}{A}} ∈ [[ϕ]]^{I} for some A ⊆ T \}
[[∀X[ϕ]]]^{I} = \{α | α_{\frac{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 respectively.

Renamings and variants are relevant in the proof of the soundness and completeness of the operational semantics in section 3.2.3. The following definition of a renaming is based on the semantic 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 a bijection ρ : VAR → VAR that is the identity except for finitely many exceptions. If ρ is a renaming, we call a constraint ϕ′ a ρ-variant of ϕ if ϕ′ is a syntactic variant of ϕ, i.e., ϕ′ results from simultaneously replacing every occurrence of a variable X in ϕ with ρ(X) and V(ϕ′) = ρ(V(ϕ)) and [[ϕ]]^{I} = [[ϕ′]]^{I}ρ with [[ϕ′]]^{I}ρ := {αρ^{−1} | α ∈ [[ϕ]]^{I}} for every interpretation I. A constraint is called a variant 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.6. Let ϕ, ψ, θ ∈ CON. A constraint language is

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

2. closed under intersection if for every two constraints ϕ and ψ there exists a constraint θ such that for every interpretation I

[[ϕ]]^{I} ∩ [[ψ]]^{I} = [[θ]]^{I},

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

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

In the following we blur the distinction between L^{2} and MSO, but we always assume that CON is closed under 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 in a (new) language for two reasons. Firstly we can now give an operational semantics to the inductive definitions of 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.8. We extend MSO with a decidable set of relations R and a corresponding arity function to a relational constraint language R(MSO) on the same set of variables X by building the R(MSO)- constraints R(CON) with the function V computing the free variables and R(MSO)-interpretations R(INT) from MSO.

Definition 3.9. The R(MSO)-constraints R(CON) are defined inductively such that

1. ϕ ∈ R(CON) for all ϕ ∈ MSO.

2. r(X_{1}, …, X_{n}) ∈ R(CON) for all tuples of pairwise distinct variables X_{1}, …, X_{n} and relation symbols r of rank n. We call these atoms.

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

4. Nothing else is in R(CON).

Definition 3.10. The set of free variables V of an R(MSO)-constraint is again defined inductively:

1. V(ϕ) := V((ϕ) if ϕ is an MSO-constraint

2. V(r(X_{1}, …, X_{n})) := {X_{1}, …, X_{n}}

3. V(∅) := ∅

4. V(F & G) := V(F) ∪ V(G)

5. V(F → G) := V(F) ∪ V(G)

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

1. [[ϕ]]^{A} := [[ϕ]]^{I} if ϕ is an MSO-constraint

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

3. [[∅]]^{A} := ASS^{A}

4. [[F & G]]^{A} := [[F]]^{A} ∩ [[G]]^{A}

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

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. This has been done for logic programs in Lloyd (1984) by defining 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.12. A definite clause specification S is a set of definite clauses of the form

B ← ϕ & A_{1} & … & A_{n}

where B and the A_{i} are 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. 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.13. Given a definite clause specification S, a model of S is an R(MSO) interpretation A such that every variable assignment α is a solution for every definite clause δ ∈ S.

Höhfeld and Smolka prove that indeed there exists a least model A for every program which can be constructed from any MSO-interpretation I as a limit of the application of the clauses.

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., [[A]]^{A_{i}} ⊆ [[A]]^{A_{j}} if A_{i} ⊆ A_{j}. Intersection and union of such interpretations are again defined via the relations. Note that a set of interpretations extending I forms a complete lattice.

Theorem 3.14 (H&S theo. 4.4). Let S be a definite clause specification in R(MSO) and I an MSO-interpretation. Then we can inductively define a chain of R(MSO)-interpretations A_{i} extending I by

1. r^{A_{0}} := ∅

2. r^{A_{i+1}} := {α(X⃗) | (r(X⃗) ← G) ∈ S and α ∈ [[G]]^{A_{i}}}

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

We have already stated informally what we expect the answer 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.

3.2.2. An R(MSO) Example. As an example for the relational language we defined, we present the definition of append on finite lists in R(MSO). Notational conventions are that the MSO-constraints are enclosed in curly brackets, lowercase letters denote node variables, uppercase letters or words starting with them set variables and relations both in MSO and R(MSO) are lowercase 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 linear precedence. With the constraints min and max we can pick out the least and the greatest element in this set. The empty list is just an empty set, and a nonempty list has a minimal and a maximal element, and all the elements which are neither are totally ordered by ≺. The head of such a list is just the smallest element, the tail all the remaining elements. The exact MSO-definitions can be found in in equations (8) to (14).

(8) min(x, X) ⟺^{def} x ∈ X ∧ (∀y)[(y ∈ X ∧ y ≉ x) ⇒ x ≺ y]
(9) max(x, X) ⟺^{def} x ∈ X ∧ (∀y)[(y ∈ X ∧ y ≉ x) ⇒ y ≺ x]
(10)  elist(X) ⟺^{def} ¬(∃x)[x ∈ X]

\begin{aligned}nelist(X) ⟺^{def} & (∃x, y)[min(x, X) ∧ max(y, X)] ∧ \\ & (∀x, y)[(¬min(x, X) ∧ ¬min(y, X) \\ & ∧ ¬max(x, X) ∧ ¬max(y, X) \\ & ∧ x ∈ X ∧ y ∈ X) ⇒ \\ & (x ≺ y ∨ y ≺ x)] \end{aligned} (11)

(12)  list(X) ⟺^{def} elist(X) ∨ nelist(X)
(13) hd(X, x) ⟺^{def} min(x, X)
(14)  tl(X, Y) ⟺^{def} Y ⊆ X ∧ (∀x)[(¬min(x, X) ∧ x ∈ X) ⇒ x ∈ Y]

The resulting R(MSO) definition for append is almost like the corresponding definition in standard logic programming. We just have to make the desired unifications between the variables explicit in the constraints, see figure 7.

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.

\begin{aligned}append(X, Y, Z) & ← \\ & \{elist(X) ∧ Y ≈ Z\} \end{aligned}

append(X, Y, Z) ←
{hd(X, x) ∧ hd(Z, x) ∧ tl(X, U) ∧ tl(Z, V)} &
append(U, Y, V)

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

Intuitively, we can substitute the body of a clause if the head represents a renamed variant of the 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. Informally, 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.

Definition 3.15. Let ϕ, ψ, θ be satisfiable MSO-constraints and A a R(MSO)-interpretation. S-goal reduction (⟶^{r}_{S}) is defined to be

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

if A ← F & ψ is a variant of a clause in S such that [[ϕ]]^{A} ∩ [[ψ]]^{A} = [[θ]]^{A} and V(G) ∩ V(F) ⊆ V(A).

Since the language is closed under intersection, we can treat the conjunction of the two constraints ϕ & ψ as a single new constraint θ.

The 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. We need some technical preliminaries before we can state the theorem. First we generalize the notion of a solution to a set of constraints. If Φ is a set of constraints and I an interpretation, the solutions of Φ in I are defined to be [[Φ]]^{I} := ⋃_{ϕ∈Φ}[[ϕ]]^{I}. Note that this interprets the constraints disjunctively, as opposed to conjunctively in the definition of the denotation function. So, solutions for a set of constraints are the union of the sets of assignment functions of the elements of the set.

Theorem 3.16 (H&S prop. 5.1). If G ⟶^{r}_{S} F, then [[F]]^{A} ⊆ [[G]]^{A} for every model A of S.

Lemma 3.17 (Soundness). If G ⟶^{r}_{S}^{∗} ϕ, then ϕ is an S-answer.

Proof. ϕ is an S-answer just in case (ASS^{A} − [[ϕ]]^{A}) ∪ [[G]]^{A} = ASS^{A} for all A which are a model of S. This is true by theorem 3.16 since [[ϕ]]^{A} ⊆ [[G]]^{A} holds.

We can now proceed to show the completeness of the reduction rule. Since the proof relies on a rather involved complexity measure, we rely on the reader to supply his or her own intuition on what a (procedural) complexity reduction means.^{13} Completeness in this sense can be paraphrased as follows. For every assignment function in the denotation, given an atom, a reduction is possible and it will still be in the denotation after the reduction.

Theorem 3.18 (H&S theo. 5.2). Let G be goal, A an atom in G, A be a minimal model of S, and α ∈ [[G]]^{A}. Then there exists a clause C in S such that

1. S-goal reduction of G on A using a variant of C is possible,

2. if G_{1} is obtained from G by S-goal reduction on A using a variant of C then α ∈ [[G_{1}]]^{A} and the complexity of the goal is reduced.

The preceding theorem actually stated what happened when we commit to a particular choice (don’t care nondeterminism). But in general we are not interested which atoms and clauses are used in achieving the result (don’t know nondeterminism). This is reflected in the next corollary.

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

Intuitively, if there exists a solution to a goal, then we can find a constraint representing it via goal reduction.

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 the definition of the relational extension. 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} with l_{i} and r_{i} words over Σ. A solution for such a system S is a sequence of indices 1 ≤ i_{1}, …, i_{n} ≤ m iff 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).

13The formal details are in Höhfeld and Smolka (1988).

To be able to present the encoding into R(MSO) we have to sugar our notation. Instead of using the constraint part to deal with our decomposition of linearly ordered sets or better lists, we use the “.” to encode list concatenation ((X.Y) for hd(Z, X) ∧ tl(Z, Y)) directly in the atom. 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 equations (8) to (14) and in figure 7 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 figure 8. Considering the query in the first line, this

← pcp((l_{1}).((l_{2}).(· · · .(l_{m})) …), (r_{1}).((r_{2}).(· · · .(r_{m})) …))
pcp((L.X), (L.Y)) ←
pcp((L.X), (R.Y)) ←
append(X, (l_{1}.L). · · · .(l_{m}.L), X1)
append(X, (r_{1}.L). · · · .(r_{m}.L), Y 1)
pcp(X1, Y 1)

Figure 8. The PCP predicate

encodes all sequences of length 1, in the next step we use the sequence 1 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 figure 8 has a SLD refutation iff a given Post correspondence system has a solution. Therefore we can state the next lemma.

Lemma 3.20. Satisfiability in the relational extension R(MSO) is undecidable.

Furthermore, we can achieve the same by only considering a smallest binary program (see Hanschke 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. But, as yet, we do not have a proof for that.

So we can indeed define problematic relations. 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 trees. 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 equations (8) to (14) or the definition of an arbitrary fact like the base case of append in figure 7. Rogers provides the notions of first and second order inductive definability to designate those relations which are recursively definable without leaving MSO. His refers to Moschovakis (1974) as the source of the definitions. The following paragraphs relate the model-theoretic notions with the operational ones we used in theorem 3.14.

We are going to define the relations recursively via an operator which computes all the tuples of sets contained in it. 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. Since we limit ourselves to positive occurrences of the relation symbol, the operator is monotone and a least fixed point exists. 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. The name of the predicate in the definite clause corresponds to a second order variable. In the following all the X_{i} and X are meant to be monadic second order variables. X is a second order variable with monadic arguments. Recall that X⃗ and x⃗ denote tuples of distinct variables.

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

Γ_{ϕ}(r) := {α(X⃗) | M ⊧ ϕ[α] and α(X) = r}.

It is a fact along the lines of theorem 3.14 that this operator has a fixpoint. If a formula exists such that there is a least fixed point for an operator computing the relation, we call the relation (positive) inductive second order definable. Recall from definition 3.11 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. We have shown above that inductive second order definable relations might be undecidable.

But if we limit ourselves to just singleton variables, we stay within the power of MSO.

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

Λ_{ϕ}(r) := {α(x⃗) | M ⊧ ϕ[α] and α(X) = r}.

The free variable X stands for the (monadic) relation on nodes we are defining. Again, if a formula exists such that there is a least fixed point for such the relation, we call it (positive) inductive first order definable. Those relations are definable since they can be explicitly second order defined with the following formula. In fact, this seems to be a variant of Beth’s theorem.^{14}

r(y⃗) ⟺^{def} (∀X)[(∀x⃗)[ϕ ⇒ x⃗ ∈ X] ⇒ y⃗ ∈ X] (15)

Now we know one way to ensure the decidability of the relations we define with our programs. We have to alter the definitions 3.9 – 3.11 such that only singleton variables are 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 × ⋯ × T . Unfortunately this gives us only the reintroduction of the notion of derivation, but not more expressive power. We have to leave this point open for further research. But results from logic programming^{15} and higher order unification^{16} suggest that we might be able to find an interesting subclass.

Ω ∪ ϕ(P) ⊧ ∀x⃗[ψ(x⃗) ⟺ P (x⃗)].

14Beth’s theorem (as in Makowsky (1992)): Let Ω be a set of first order formulas over a signature Σ and P be an n-ary relation symbol not in Σ. We say a formula ϕ(P) over Σ ∪ {P } defines P implicitly using Ω, if in each model M of Ω there is at most one interpretation of P. We say that the predicate implicitly defined by ϕ using Ω has an explicit definition for which there is a formula ψ(x⃗) over Σ such that The theorem then says that for Ω a set of first-order formulas and for ϕ(P) an implicit definition of P using Ω, there exists an explicit definition of P using Ω.

15The results are related to properties such as groundness or linearity of the involved programs and queries, see Devienne et al. (1994).

16Levy’s result states that linear unification is decidable (Levy; 1996).

3.2.5. The Interpreter. In this section on the interpreter we specify a search strategy, a constraint solver and discuss 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 (Frühwirth et al.; 1993). 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 knowledge about the variables very efficiently as tree automata

• they can be used incrementally since the nature of the proof allows us to view a tree automaton as a constraint store where the conjunction with a new constraint yields a new store;

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

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

• we can define what it means for an MSO constraint to be normal.

To make some of the statements more precise we present the working of the desired interpreter in more detail. First of all, we single out a particular subclass of formulas.

Definition 3.23. A normal MSO-constraint is a formula whose corresponding minimized tree automaton recognizes a nonempty language.

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.

Lemma 3.24. For every pair of normal MSO-constraints we can compute a new MSO-constraint and decide whether it is normal.

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 a definite clause specification such that the 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.

Lemma 3.25. Every definite clause specification can be converted to a normal definite clause specification.

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. By this testing of the applicability of the clauses, we achieve something like Prolog’s term unification to find matching clauses.

The outline of the interpreter 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 a type discipline. This allows the typing of variables with MSO constraints as it is done 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 it subsumes 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.

The third possible aspect which we do not address is the use of consistency techniques like constraint propagation. It involves narrowing the domain of values the variables can take by inferring the information between constraints. For more information on constraint propagation, see Le Provost and Wallace (1993).

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). Similar techniques, called guards or residuation have also been proposed by Smolka (1993). Instead of only telling constraints, i.e., adding them to the constraint store, we can also ask whether a constraint is entailed by the constraint store. This amounts to checking the satisfiability of the constraint store conjoined with the negation of the constraint. Obviously this is an extension that the constraint solver can handle. 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 allows the framework 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. We think that this is a major point for further research.

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 (1991), Minnen and Gerdemann (1993)). Another technique involves the addition of new predicates to allow bottom up execution of the program, called magic compilation (Beeri and Ramakrishnan (1987), 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 the case of P&P-based theories formulated in MSO, the linguistic structures which are subject to the constraints of the grammar are tree like sets of nodes. 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. 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 the 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). In R(MSO) we can specify a parsing program.

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. We provide examples for both the limited and the full extension of MSO. Note that an explicit definition corresponds directly to a fact.

4.1. Pure Parsing. As discussed in section 2.3, one could use a complete formalization of the grammar in MSOfor 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.

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 anotherMSOconstraint identifying nodes with an empty phonology (e phon).

\begin{aligned}yield(S, T) ⟺^{def} & (∀x)[(x ∈ T ∧ ¬∃y[x ⊲ y] ∧ ¬e phon(x)) ⇒ \\ & x ∈ S] ∧ \\ & ¬(∃z)[z ∈ S ∧ z ∉ T] \end{aligned} (16)

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.

(17) gram(In, X) ⟺^{def} yield(In, T ree) ∧ gram(T ree)

The definite clause can be found in figure 9.

\begin{aligned}parse(In, X) & ← \\ & \{gram(In, X)\} \end{aligned}

Figure 9. Pure MSO parse

Treat the input string In as a set of nodes labeled with the words as monadic properties and linearly ordered by precedence. Additionally, we have to exclude 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)[x, y, z ∈ In ∧ Jan(x) ∧ Sees(y) ∧ Lena(z) ∧ \\ x ≺ y ≺ z ∧ \\ (∀w)[(w ∈ IN ∧ w ≉ x ∧ w ≉ y ∧ w ≉ z) ⇒ \\ e phon(w)]]\} \end{matrix} (18)

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 section 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). His parse relation holds of a string and a tree in case it obeys the xbar theory, the ecp and the string is the yield of the tree, see figure 10. We assume that all our mso variables are constraint to be trees.

parse(W ords, T ree) ←
{list(W ords)}  &
xbar(T ree)  &
ecp(T ree)  &
yield(W ords, T ree)

Figure 10. parse from Johnson (1995)

As an example, we will work through the definition of the xbar predicate. First, we have to define some new MSO-constraints though.

(19)  root(X, x) ⟺^{def} (x ∈ X) ∧ (∀y)[y ∈ X ⇒ x ⊲^{∗}y]

The definition of a root is relative to a specific set, x is the root of X.

(20)  dtrs(x, y, z) ⟺^{def} x ⊲ y ∧ x ⊲ z ∧ y ≺ z

The definition of daughters (dtrs) 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.

(21)  subtree(X, y, Y) ⟺^{def} (∀x)[(x ∈ X ∧ y ⊲^{∗}x) ⇒ x ∈ Y]

\begin{aligned}subtrees(X, x, Y, y, Z, z) ⟺^{def} & root(X, x) ∧ dtrs(x, y, z) ∧ \\ & subtree(X, y, Y) ∧ subtree(X, z, Z) \end{aligned} (22)

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.

Coming back to an issue raised in section 2.3 in equation (5), let us note that we can avoid having to compile the lexicon as one constraint by having facts for each lexical entry separately (see figure 11). Naturally this is highly nondeterministic and shifts the burden to the clp interpreter. But at least the approach makes the problem feasible.

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

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

The first clause of xbar in figure 12 allows empty nodes to appear freely. The distribution of those nodes has to be constrained with the ecp. The second clause allows nodes which appear in the lexicon while the third 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 figure 13).

\begin{aligned}xbar(X) & ← \\ & \{elist(X)\} \end{aligned}

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 12. 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 13. local xbar following Johnson (1995)

The ecp deals with the distribution of the empty nodes in the tree.^{17} The predicate yield was already defined in equation (16). 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.

The general approach of constraining variables to particular values allows the specification of data types. We can define them in the constraint language without having to include a type discipline. We attach additional conditions to every variable appearing in a clause. In the case of MSO, we already discussed following Rogers and Rizzi (and others) in their assumption that the basic entities the theory deals with are not longer nodes, but categories. Recall the definitions and discussion from section 2.3. Now we can constrain our variables in R(MSO) to range over categories so that they become the basic components of a theory. Again, details can be found in Rogers’ thesis.

17We leave out the definition of the ecp predicate. It can be captured using similar techniques as in the preceding examples.

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 figure 14.^{18} Again, we need some auxiliary definitions. We follow Fong in them, although we think they are pretty ad hoc.

(23) max(x) ⟺^{def} x ∈ NP ∨ x ∈ V P ∨ …

max denotes those nodes which are labeled maximal.

(24) proj(x, y) ⟺^{def} (x ∈ NP ⇔ y ∈ N1) ∨ (x ∈ V P ⇔ y ∈ V 1) ∨ …

proj expresses that two nodes are projections of each other.

(25) dts(x, X) ⟺^{def} (∀y)[x ⊲ y ⇔ y ∈ X] ∧ list(X)

dts just collects all daughters of x in a list.

xp(x) ←
{max(x) ∧ proj(x, y) ∧ (∃X)[dts(x, X) ∧ hd(X, y) ∧ tl(X, Z)]} &
x1(y)  &
specs(y, Z)

Figure 14. xp following Fong (1991)

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.

18We take here 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 three variables without problems, i.e., proj max list(x, y, Z).

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 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 big difference to other theories as for example HPSG. This is most clearly seen in phrase structure based implementations of these theories, e.g., in Shieber (1992) or Carpenter (1993). We can see the strong locality requirements since all the feature constraints are coupled to the phrase structure rules. In HPSG itself they are bound to the ID schemata. 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 (Pollard and Sag; 1994). 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 mso 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. As presented in figure 15, we can almost use the pure MSO approach, only modified to work incrementally on a particular input. Remember that the resulting tree automaton can represent a number of possibilities to construct trees which are licensed by this particular branch of the search tree.

parse(In, X) ←
{yield(In, X)} &
θ-theory(X)  &
xbar(X)  &
case(X)  &
move-α(X)  &
lex(In)  &
⋮

Figure 15. A possible R(MSO)-definition of parse

Now we can add either MSO relations which just encode these modules, or we can split them further where suitable. As an example, we present two definitions of lex in figure 16. In the first definition one can

\begin{aligned}lex(X) & ← \\ & \{elist(X)\} \end{aligned}

lex(X) ←
{hd(X, x) ∧ tl(X, Y)} &
lexicon(x)  &

lex(Y)

or

\begin{aligned}lex(X) & ← \\ & \{(∀x)[x ∈ X ⇒ lexicon(x)]\} \end{aligned}

Figure 16. Two possible R(MSO)-definition of lex

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. We use the list structure of the input to recurse on it. Whereas in the second approach we rely directly on the power of the constraint solver to handle the problem. Note that this second example presupposes the compilation of the whole lexicon into a variant of the lexicon definition we presented in equation (5). The MSO-constraint lexicon is a disjunction of all the lexical items. This shows the advantage of guiding the search by the use of available data structures. What we did here for lists might be done similarly for the set of nodes representing the tree and the subsets representing the subtrees. By this we can recurse on the tree structure without loosing the ability to express nonlocal constraints. We always constrain the whole set by constraining its members.

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. But as discussed before, this has to be left for further work.

Another area of advantages of MSO-constraints is in the specification of the existence of further information to be found. If we consider some phrase structure based approaches, we can now express the relation between a filler and its gap directly. Assume for simplicity that the definite clauses are just used to encode phrase structure rules. Suppose we have a 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 figure 17. The clause finds and recurses on the subtrees if there exists a trace in

s(X) ←
{subtrees(X, Y, Z) ∧ (∃z)[z ∈ Z ∧ z ∈ T race ∧ feq(z, Y)]} &
np_{wh}(Y)  &

vp(Z)

Figure 17. Nonlocality in a phrase structure rule

Z such that it agrees on the relevant features with the extracted WHphrase. The auxiliary definition identifying the two immediate subtrees is presented in equation (26).

subtrees(X, Y, Z) ⟺^{def} (∃x, y, z)[subtrees(X, x, Y, y, Z, z)] (26)

An example for the use of quantification in R(MSO) 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 Principle. We leave the formal specification to the reader.

5. Summary

We presented in this paper the first step towards MSO-based constraint logic programming. We applied the Höhfeld and Smolka scheme for the definition of the constraint logic programming language R(MSO) with relational extensions. This 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., MoSeL or 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 certainly 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 can investigate. The first is concerned with formal issues connected with R(MSO). If we want to extend our constraint language with negation it seems to be necessary to clarify which alternatives we have since MSO is not compact.^{19} Another interesting point seems to be the generative capacity of the relational extension. Considering the discussion on definability in section 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 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 of research.

19Compactness 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.

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.

References

Beeri, C. and Ramakrishnan, R. (1987). On the power of magic, Proceedings of the 6th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems.

Biehl, M., Klarlund, N. and Rauhe, T. (1996). Algorithms for guided tree

automata, Proc. WIA ‘96, LNCS, Springer-Verlag. Blackburn, P. and Meyer-Viol, W. (1994). Linguistics, logic and finite

trees, IGLP Bulletin. Büchi, J. R. (1960). Weak second-order arithmetic and finite automata,

Zeitschrift für mathematische Logik und Grundlagen der Mathematik 6: 66–92.

Carlson, B. (1991). An approximation theory for constraint logic programs, Licentiate Thesis. Dep. of Computer Science, Uppsala University.

Carpenter, B. (1992). The Logic of Typed Feature Structures, Vol. 32 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press.

Carpenter, B. (1993). ALE the attribute logic engine, user’s guide, User manual, Laboratory for Computational Linguistics, Philosophy Department, Carnegie Mellon University, Pittsburgh, PA 15213.

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

Foris. 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. (1995). C-command and grammatical

primitives, Presentation at the 18th GLOW Colloquium. University of Tromsø.

Frühwirth, T., Herold, A., Küchenhoff, V., Le Provost, T., Lim, P., Monfroy, E. and Wallace, M. (1993). Constraint logic programming: An informal introduction, Technical Report ECRC-93-05, ECRC. Appears in Logic Programming Summer School, Zürich, Springer Lecture Notes.

Gécseg, F. and Steinby, M. (1984). Tree Automata, Akadémiai Kiadó,

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

program, Information Processing Letters 45(5): 237–241. Hathout, N. (1992). Theórie du Governement et du Liage et programma-

tion logique avec contraintes: une application à l’analyse automatique du français, PhD thesis, L’Université Paul Sabatier de Toulouse (Sciences), Toulouse.

Henriksen, J. G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, R., Rauhe, T. and Sandhol, A. (1995). Mona: Monadic second-order logic in practice, in Brinksma, Cleaveland, Larsen, Margaria and Steffen (eds), Tools and Algorithms for The Construction and Analysis of Systems: International Workshop, TACAS ’95, Selected Papers, Lecture Notes in Computer Science 1019, Springer, pp. 89–110.

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 struc-

ture grammars, in de Haan, Trommelen and Zonneveld (eds), Van Periferie naar Kern, Foris, Dordrecht, pp. 81–99.

Jaffar, J. and Lassez, J.-L. (1986). Constraint logic programming, Technical report, IBM-Thomas J. Watson Research Center, Yorktown Heights, N.Y. 10598.

Johnson, M. (1995). Constraint-based natural language parsing, ESSLLI

’95 Barcelona notes. Kaplan, R. M. and Bresnan, J. (1983). Lexical-functional grammar: A

formal system for grammatical representation, in J. Bresnan (ed.), The Mental Representation of Grammatical Relations, MIT Press, Cambridge, Mass, pp. 173–381.

Kayne, R. S. (1994). The Antisymmetry of Syntax, Vol. 25 of Linguistic Inquiry Monographs, MIT Press, Cambridge, Mass. and London, England.

King, P. J. (1989). A Logical Formalism for Head–Driven Phrase Structure

Grammar, PhD thesis, University of Manchester. Kracht, M. (1995). Syntactic codes and grammar refinement, Journal of

Logic, Language, and Information 4: 41–60. Le Provost, T. and Wallace, M. (1993). Generalized constraint propaga-

tion over the clp scheme, Journal of Logic Programming 16: 319–359. Levy, J. (1996). Linear second order unification, Proceedings of the Con-

ference on Rewriting Techniques and Applications, Springer. Lloyd, J. (1984). Foundations of Logic Programming, Springer Verlag. Makowsky, J. A. (1992). Model Theory and Computer Science: An Appe-

tizer, Vol. 1 of Handbook of Logic in Computer Science, Oxford Science Publications, pp. 763–814.

Minnen, G. and Gerdemann, D. D. (1993). Direct automated inversion

of logic grammars, SFB-Report 35, SFB 340, University of Tübingen. Morawietz, F. and Cornell, T. L. (1996). On the recognizability of rela-

tions over a tree definable in a monadic second order tree description language, SFB-Report 85, University of Tübingen, SFB 340, A8.

Moschovakis, Y. N. (1974). Elementary Induction on Abstract Structures,

North-Holland, Amsterdam. Niehren, J. and Podelski, A. (1992). Feature automata and recogniz-

able sets of feature trees, in M.-C. Gaudel and J.-P. Jouannaud (eds), Proceedings of the 4th International Joint Conference on Theory and Practice of Software Development, Springer Verlag, LNCS 668, Orsay, France, pp. 356–375.

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 American Mathematical Society 52: 264–268. Rabin, M. O. (1969). Decidability of second-order theories and automata

on infinite trees, Transactions of the American Mathematical Society 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. (1994). Studies in the Logic of Trees with Applications to

Grammar Formalisms, PhD thesis, University of Delaware, Dep. of Computer & Information Sciences, Newark, DE 19716. Published as

Technical Report No. 95-04. Saraswat, V. A. (1993). Concurrent Constraint Programming, MIT Press,

Cambridge, Massachusetts. Shieber, S. M. (1985). Evidence against the context-freeness of natural

language, Linguistics and Philosophy 8: 333–343. Shieber, S. M. (1992). Constraint–Based Grammar Formalisms, MIT

Press. Smolka, G. (1993). Residuation and guarded rules for constraint logic

programming, in F. Benhamou and A. Colmerauer (eds), Constraint Logic Programming: Selected Research, MIT Press, chapter 21, pp. 405– 419.

Stabler, E. P. (1992). The Logical Approach to Syntax: Foundations, Spec-

ifications and Implementations, MIT Press, Cambridge, Massachusetts. Strzalkowski, T. (1991). A general computational method for grammar

inversion, Proceedings of the Reversible Grammar Workshop, Berkeley, CA.

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

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