Bericht Nr. 85, Februar 1997

ISSN 0947-6954/97

Arbeitspapiere des Sonderforschungsbereichs 340

Sprachtheoretische Grundlagen für die Computer linguistik

Frank Morawietz & Tom Cornell :

On the Recognizability of Relations over a Tree definable in a Monadic Second Order Tree Description Language

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

Bericht Nr. 85, Februar 1997

ON THE RECOGNIZABILITY OF RELATIONS OVER A TREE DEFINABLE IN A MONADIC SECOND ORDER

TREE DESCRIPTION LANGUAGE

FRANK MORAWIETZ AND TOM CORNELL

Abstract. In this technical report we describe both the theoretical background and the implementation of the prototype MoSeL, a theorem prover based on the monadic second order tree description language L_{K,P}^{2} (Rogers 1994). We make use of the results by Thatcher and Wright (1968) and Doner (1970) proving that the (weak) monadic theory of two successor functions is decidable. They show that formulas in monadic second order logic on trees are satisfiable if and only if the satisfying variable assignments can be recognized by a tree automaton. In the paper we provide the necessary background on tree automata and their constructions, redo the decidability proof and describe its realization in the Prolog implementation MoSeL.

1. Introduction

Rogers (1994) presents L_{K,P}^{2} , a monadic second-order language for describing properties of trees. Aside from being very powerful and flexible, L_{K,P}^{2} is proved to be decidable. The proof is rather indirect. First L_{K,P}^{2} is shown to be intertranslatable with the language of SnS, the theory of multiple successor functions. SnS is known, in turn, to be decidable, and this is shown by proving that any relation which can be defined in that language is recognizable, that is, definable by a tree automaton of a particular sort. In particular, it can be shown (see Rabin 1969, Thatcher and Wright 1968, Doner 1970) that from any formula in the language of

The research presented in this report was sponsored by Teilprojekt A8 of the Sonderforschungsbereich 340 of the Deutsche Forschungsgemeinschaft. We want to thank Hans-Peter Kolb, Uwe Mönnich and Jim Rogers for helpful discussion. Needless to say, all errors and infelicities that remain are our own.

ISSN 0947-6954/97 \begin{matrix}c \\ ◯ \end{matrix} 1997 Die Autoren

SnS one can construct a tree automaton which recognizes all and only trees whose labels encode instances of the defined relation.

In the first section of this report we redo the decidability proof for a language essentially like Rogers’ L_{K,P}^{2} (or more accurately, L_{∅,∅}^{2}) in a more direct manner, essentially skipping the translation to the language of SnS entirely. In fact this is quite simple to do: we merely need to show that the relations defined by the atomic formulas of L_{K,P}^{2} are recognizable, by presenting automata that recognize them. Then the inductive step from the proofs in Rabin (1969), Thatcher and Wright (1968), and Doner (1970) can be applied unchanged. From this we get the more general result that any monadic second order tree description language whose atomic formulas can be converted to automata will be decidable.

These are perhaps not very interesting results on their own. We present them here as a foundation for further investigations in the relation of automata to logic, which in turn is an interesting new angle on automatic theorem proving and ultimately, we hope, on constraint logic programming. As a step in this direction, in the second section we present MoSeL, a prototype for a tool for automated theorem proving over monadic second order tree description languages. The implementation is done in Prolog and follows the inductive decidability proof almost to the letter. Our program serves as a translator from logical formulae to tree automata. The interaction of minimization and conditions on reachability of states ensures that we generate non empty automata only if the formula is satisfiable, i.e., the existential closure of the formula represents a theorem of our language.

2. Theoretical Background

2.1. The Language. We focus in this report on one particular tree description language, the language L_{K,P}^{2} introduced in Rogers (1994). L_{K,P}^{2} is a monadic second order language built up from the following relation symbols.^{1}

x ⊲^{+} y — x properly dominates y,
x ⊲^{∗} y — x dominates y,
x ⊲ y — x immediately dominates y,
x ≺ y — x properly precedes y.

1The K and P subscripts refer to arbitrary sets of individual and predicate constant symbols, with which the language can be parameterized. They do not play a role in this paper since, without loss of generality, constants can be treated as free variables.

That is, atomic formulas are built up out of the relation symbols ⊲^{+}, ⊲^{∗}, ⊲, and ≺ together with the logical constants ≈ and ∈, the boolean connectives ∧ and ¬, and the existential quantifier ∃. Quantifiers may bind variables which range over individuals and also over sets of individuals. We write individual variables as x, y, z, x_{1}, x_{2}, … and set variables as X, Y, Z, X_{1}, X_{2}, . . .. As usual we make free use of the “abbreviations” ϕ ∨ ψ, ϕ ⇒ ψ, ϕ ⇔ ψ, and (∀x)ϕ for ¬(¬ϕ ∧ ¬ψ), ¬(ϕ ∧ ¬ψ), ¬(ϕ ∧ ¬ψ) ∧ ¬(¬ϕ ∧ ψ), and ¬(∃x)¬ϕ, respectively.

As an example of the language in action, the following formula defines a relation which is, in fact, the ⊲^{∗} relation.

D(x, y) ⟺_{def}

(∀X)[(∀x_{1}, x_{2})[x_{1} ∈ X ∧ x_{2} ⊲ x_{1} ⇒ x_{2} ∈ X] ⇒ (y ∈ X ⇒ x ∈ X)]

So we note in passing that our language is not in fact as spare as it could be: ⊲^{∗} can be defined in terms of ⊲, and then ⊲^{+} can be defined in terms of ⊲^{∗} and (the negation of) ≈. This is only true for the second order language L_{K,P}^{2} . Were we to restrict ourselves to the first order language L_{K,P}^{1} (as in, e.g., Backofen et al. 1995), then we would need these second-order definable relations back again as primitives.

2.2. Trees and Tree Automata.

2.2.1. The Structure and Language of Multiple Successor Functions. The fundamental results on which we build here (Rabin 1969, Doner 1970, Thatcher and Wright 1968) involve the monadic second order theory of multiple successors. These generalize Peano’s approach to generating the natural numbers. Instead of looking at the structure ⟨N, 0, s⟩, wherein every natural number is either zero or some number of applications of s to zero, we look now at, for example, ⟨N, 0, r_{1}, r_{2}⟩. Thinking about the natural numbers, we could define xr_{1} = 2x + 1 and xr_{2} = 2x + 2, thereby generating the odd numbers by applications of r_{1} and the evens— besides zero—by applications of r_{2}. (We write the successor functions postfix to make the generalization of automata on strings to automata on trees a little clearer.) Note in particular that each natural number is still the value of a unique term in the language of two successor functions; the numbers are this way arranged in a tree, rather than in the familiar number line (which is now seen to be just a degenerate tree). In general, for finite p, xr_{i} = px + i, 1 ≤ i ≤ p.

Obviously, we are interested far more in trees and less in number theory. But the logic of multiple successors gives us what is in many ways the simplest and most fundamental tree logic. Other logics, like Rogers’ L_{K,P}^{2} , may be more convenient for grammatical applications, but everything is grounded here.

For the rest of this paper we will be concerned with the structure of two successor functions, N_{2} = ⟨N_{2}, 0, r_{1}, r_{2}⟩. The domain of this structure, N_{2}, is an infinite, strictly binary branching tree. As the language of N_{2}, we take for our terms the set of strings {1, 2}^{∗}. The empty string ϵ is our sole constant and is taken to denote 0. The string wi, w ∈ {1, 2}^{∗}, i ∈ {1, 2} is interpreted as the application of r_{i} to the number denoted by w. So for example the string 21 denotes the value of 0r_{2}r_{1}, that is, 5. For our purposes, though, it is easier to think of 21 as being the specification of a path through a tree which starts at the root, takes in the right daughter of the root, and ends at that node’s left daughter.

The monadic second order theory of n successor functions, conventionally termed SnS, is the set of all sentences involving quantification over sets of individuals as well as individuals, based on the logical constants ≈ and ∈ and the successor functions, which are true of N_{n}, the structure of n successor functions. Doner (1970) and Thatcher and Wright (1968), as well as Rabin (1970), deal with the so-called weak interpretation of that theory, where set variables are constrained to vary over finite subsets of N_{2}. Rabin (1969), on the other hand, deals with the strong interpretation of the theory, in which set variables can range over arbitrary subsets of N_{2}, and indeed beyond S2S to SωS, the structure of countably many successor functions. It turns out that even in these wild and wooly cases, the theory remains decidable.

We are primarily interested in linguistic applications where we can count on the sets of nodes we wish to isolate being finite. Accordingly, we focus on the weak interpretation of S2S, and generalizations only to systems of finitely many successors. For practical purposes, this means that the tree automata we construct run over finite trees; we do not need to consider here automata on infinite objects, though it is important to note that Rogers himself follows Rabin’s work on the strong theories of SnS and SωS most closely.

Note that because we are dealing with monadic second order logic for trees, we can always pick out finite subsets of N_{2} as our trees of interest, simply relativizing all of our formulas to a chosen set variable whose members are all and only the nodes of our tree of choice. So the fact that N_{2} is itself an infinite tree of fixed branching factor is not a problem for us.

2.2.2. Tree Domains, Term Algebras and Automata. The structure of n successor functions is the mathematical foundation of what are often called in computer science tree domains. A tree domain can be based on any linearly ordered set K; it is defined as a subset T ⊆ K^{∗} such that, for u, w ∈ K^{∗}, i, j ∈ K,

1. uw ∈ T ⇒ u ∈ T (prefix closure),

2. uj ∈ T and i < j ⇒ ui ∈ T (closure under left sister). Note that the branching factor of a tree presented as a tree domain is not necessarily fixed.

A labeled tree can be thought of as a function t : T → Σ, where T is a tree domain and Σ is an alphabet from which we draw our labels. This is the conception of a tree which is used in Doner (1970), for example. It stays close to the ultimate structure of interest, and so makes the model theory a little easier, but the automata theory is slightly harder to develop in this framework.

Thatcher and Wright (1968), on the other hand, adopt a more algebraic approach, which makes the automata theory more elegant, but requires some footwork when it comes time to focus on the model theory. In this algebraic approach (ordered, labeled) trees are defined as terms over a particular alphabet. Notationally, given an alphabet Σ = Σ_{0} ∪Σ_{1} ∪⋯ Σ_{p}, where each Σ_{i} is a set of i-place function symbols, we refer to the set of Σ-terms as T_{Σ}. A tree t over Σ is any member of T_{Σ}.

Thatcher and Wright (1968) define an automaton (over finite trees) as an algebra A = (A, α), with A the set of states and α a function mapping alphabet symbols—symbols from Σ—to functions over A. Because T_{Σ} is a free algebra and α ↾ Σ_{0} is a mapping from its generators to A, we can extend α to a homomorphism h_{A} from arbitrary terms of T_{Σ} to A. For example, for λ ∈ Σ_{0} and f ∈ Σ_{2}, we have the following.

h_{A}(λ) = α(λ)
h_{A}(ft_{1}t_{2}) = α(f)(h_{A}(t_{1}), h_{A}(t_{2}))

If we think of the α(Σ) as our direct transition functions, then h_{A} is just the standard generalization of a direct transition function to inputs of arbitrary size. The process of computing the value of h_{A}(t) is clearly the same process as that of determining what state to assign to t’s root given an assignment of states to its leaves. That is, computing h_{A}(t) is just running a bottom-up automaton on t.

Thatcher and Wright (1968) use an algebra A to pick out a set of trees by selecting a set of final states A_{F} ⊆ A and defining the language of the automaton to be

{t | h_{A}(t) ∈ A_{F} }.

They refer to this set as the behavior of A with respect to A_{F}, and write

bh_{A}(A_{F}) = {t | h_{A}(t) ∈ A_{F} }.

We find that once one focuses on constructions on automata and operations on the forests they recognize it is easier to reserve the word automaton for the pairing of an underlying state-algebra (A, α) with a particular set of final states A_{F}. Here we will refer to the pair A = (A, α) as the “underlying state-algebra,” or more often just “algebra”, and refer to an automaton 𝔄 as the triple 𝔄 = (A, α, A_{F}).^{2} Accordingly, we will speak only of the behavior of an automaton, the intended set of final states being understood. We will write T (𝔄) for the set of trees recognized by 𝔄, the language bh_{𝔄}(A_{F}) of 𝔄. However, since the assignment of a state to a tree is independent of any choice of final states, we will retain the notation h_{A}(t), refering only to the underlying algebra, when it is useful to do so.

We can extend this approach easily to deal with nondeterministic automata, as follows. We allow our direct transition functions α(Σ) to map tuples of states to sets of states. Technically, since our transition functions are no longer operations, strictu senso, then our “algebras” are also no longer algebras. Nonetheless all of the essential concepts generalize to these “nondeterministic algebras”. We can still extend the direct transition functions to a homomorphism so that given a nondeterministic algebra A = (A, α), it still makes sense to denote the set of states assigned to a tree t as h_{A}(t). Since h_{A}(t) is now a set of states, the behavior of a nondeterministic automaton such as 𝔄 is defined as follows.

T (𝔄) = {t | h_{A}(t) ∩ A_{F} ≠ ∅}

It is often convenient to think of α as a transition relation over A^{n+1}, rather than as a function from A^{n} → ℘A.

Note that, just as for finite automata on strings, there is an equivalence (for bottom-up automata only!) between deterministic and nondeterministic automata. In particular, for every nondeterministic tree automaton we can effectively construct a deterministic automaton which recognizes the same set of trees.

2.2.3. The Emptiness Problem for Tree Automata. Suppose we are given an automaton 𝔄 = (A, α, A_{F}), and we wish to know whether or not T (𝔄) is empty. One way of deciding this is to systematically generate and test all of the Σ-trees of depth less than or equal to |A|. It is a standard theorem in the study of tree automata that the language of 𝔄 is nonempty if and only if this (finite) subset is non-empty.

2This is essentially the approach in Gécseg and Steinby (1984), except that they assume an alphabet distinguishing constants and variables, so their definition of an automaton includes a variable assignment function.

We use another approach, which we adapt from Rabin (1970). (He is concerned with automata on infinite trees; we adapt his algorithm to finite trees.) We define inductively the set of nodes which can be reached from the initial states; if any final state can be reached from some initial states, then the language is non-empty.

Q^{0} = α(Σ_{0}) (1)

Q^{n+1} = Q^{n} ∪ {a|(∃σ ∈ Σ, a_{1}, a_{2} ∈ Q^{n})[α(σ)(a_{1}, a_{2}) = a]}
(i.e., Q^{n} ∪ α(Σ_{2})(Q^{n} × Q^{n}))

Q = ⋃_{n<ω} Q^{n}

Provably, the construction of Q reaches a fixpoint at the latest when n = |A|. At that point, the emptiness of the language of 𝔄 reduces to the question whether or not

A_{F} ∩ Q = ∅.

In fact we can be even more hard-nosed and efficient: the minute a final state appears in one of the Q^{n} we know that T (𝔄) is non-empty, and the minute Q^{n+1} = Q^{n} we know we have decided the question, one way or the other. This algorithm is polynomial (cubic) in the number of states in the underlying state-algebra.

2.2.4. Constructions on Tree Automata. The recognizable sets, that is, the sets of trees that can be recognized by some tree automaton, enjoy numerous useful closure properties. The proofs of these properties are well-known and easily accessible (see, e.g., Gécseg and Steinby 1984), but we summarize here the key automaton-constructions which are used in these closure proofs as witnesses to the recognizability of some derived tree-set. These constructions form the foundations of our computational investigations into the use of tree automata in theorem provers for tree logics.

Boolean constructions. Suppose we are given an automaton 𝔄 which recognizes a set U of trees, and another automaton 𝔅 which recognizes a set V of trees. That is,

U = T (𝔄),
V = T (𝔅).

It is entirely straightforward to construct an automaton which recognizes U ∩ V, U ∪ V, or U − V. All of these constructions are based on the cross product of the two algebras A and B, and differ only in the proper choice of final states.

(2)  A × B = (A × B, γ)
γ(λ) = (α(λ), β(λ))
γ(f)((a_{1}, b_{1}), (a_{2}, b_{2})) = (α(f)(a_{1}, a_{2}), β(f)(b_{1}, b_{2}))

Then

\begin{aligned}U ∩ V & = bh_{A×B}(A_{F} × B_{F}) & (3) \\ U ∪ V & = bh_{A×B}((A_{F} × B) ∪ (A × B_{F})) & (4) \\ U − V & = bh_{A×B}(A_{F} × (B − B_{F})) & (5) \end{aligned}

Note that in the particular case where U = T_{Σ} the difference U − V (i.e., the complement of V) can be handled without the cross-product construction. The relevant automaton is just (B, β, B − B_{F}).

Note further that in the case of union, if the state-sets of the input automata are disjoint then a simple union construction on the input automata suffices. That is, U ∪ V can be recognized by an automaton ℭ = (A ∪ B, α ∪ β, A_{F} ∪ B_{F}). Since the state sets (and hence the domains of α and β) are disjoint, α ∪ β is certain to be well-defined. This construction corresponds directly to the notion that any tree in U ∪ V can be recognized by running 𝔄 or else running 𝔅. The cross-product construction corresponds to running two automata simultaneously and in the essentially disjunctive union operation there is clearly no need to do this.

Projection. The boolean constructions assume that U and V are both subsets of T_{Σ}, for some fixed Σ. We need also a construction which takes us from a set of trees in one alphabet Σ to another, call it Ω. Assume that we are given a mapping P : Σ → Ω; we extend it to a mapping P̄ from T_{Σ} → T_{Ω} in the natural way. That is:

P̄(λ) = P (λ)
P̄(ft_{1}t_{2}) = P (f)P̄(t_{1})P̄(t_{2})

Now suppose that U ⊆ T_{Σ}, and that we are given 𝔄 = (A, α, A_{F}) such that U = T (𝔄). We construct a nondeterministic automaton 𝔅 working on the new “projected” alphabet as presented in (6). But first we have to introduce some notation. Let F be a set of functions. Then F (x, y) is meant to denote {z | (∃g ∈ F)[g(x, y) = z] }.

(6)  𝔅 = (A, β, A_{F})
β(λ) = α(P^{−1}(λ))
β(f)(a_{1}, a_{2}) = α(P^{−1}(f))(a_{1}, a_{2})

Then

P̄(U) = T (𝔅)

So, considering the remark on notation above, α(P^{−1}(f))(a_{1}, a_{2}) denotes the set of a such that, for some g with P (g) = f, the following equation holds: α(g)(a_{1}, a_{2}) = a.

Inverse projection. We can also define an inverse-projection construction. Suppose we are again given a projection P : Σ → Ω and now a set V ⊆ T_{Ω}, and V is known to be recognizable. That is, for some Ω-automaton 𝔄 = (A, α, A_{F}), V = T (𝔄). We construct an automaton 𝔅 as follows.

(7)  𝔅 = (A, β, A_{F})
β(σ) = α(P (σ)) for all symbols σ ∈ Σ

Then

P̄^{−1}(V) = T (𝔅)

Determinization. As with finite state automata, there is an equivalence in tree automata between nondeterministic and deterministic automata. (Note, however, that this only holds for bottom-up automata!) The crucial step in the proof, which shows that from any nondeterministic automaton we can construct a deterministic one which recognizes the same set, is witnessed by a construction which we present here. This is, like most of these constructions, a simple generalization of the corresponding construction for finite state automata, in this case the subset construction.

To see why this construction is necessary, one may note simply that there are nondeterministic automata which, after the application of the complementation construction, still recognize the same set. For example,

𝔄 = ({a_{0}, a_{1}}, α, {a_{0}})
α(λ) = {a_{0}, a_{1}}

α(σ)(a_{0}, a_{0}) = {a_{0}} for all σ ∈ Σ_{2} All other transitions are to a_{1} recognizes all of T_{Σ}: all we have to do is assign a_{0} to every leaf, and the tree is guaranteed to be assigned a_{0}.

Applying the complement construction directly to 𝔄 gives us

𝔅 = ({a_{0}, a_{1}}, α, {a_{1}}).

But T (𝔅) is also T_{Σ}! All we have to do is to assign every leaf a_{1}, and any arbitrary tree will be assigned a_{1}. If on the other hand we determinize 𝔄 first, then in the resulting automaton every node will be assigned {a_{0}, a_{1}}, which is a final state. The final states of the complement automaton will be just those states which do not contain a_{0}, that is, {∅, {a_{1}}}. No tree can be assigned either state, so indeed our complemented automaton recognizes the complement of T_{Σ}, as we would have hoped.

Suppose we are given a nondeterministic Σ-automaton 𝔄 = (A, α, A_{F}). We construct a new deterministic automaton 𝔅 from 𝔄 as follows.

𝔅 = (℘A, α̂, B_{F}) (8)

α̂(λ) = α(λ)
For Q_{1}, Q_{2}, Q ⊆ A,
α̂(σ)(Q_{1}, Q_{2}) = ⋃{Q|(∃a_{1} ∈ Q_{1}, a_{2} ∈ Q_{2})[α(σ)(a_{1}, a_{2}) = Q]}
(i.e., ⋃ α(σ)(Q_{1} × Q_{2}) )
B_{F} = {Q ⊆ A|Q ∩ A_{F} ≠ ∅}

Then it is a standard result of tree automata theory that

T (𝔄) = T (𝔅).

In mathematical work this means that we can ignore the difference between deterministic and nondeterministic automata. In applying these ideas to computation, however, it is important to note that, for example, some of the boolean constructions only work for deterministic automata, and therefore we must always assume that the input to such a construction has been filtered through the determinization construction if necessary.

Minimization. Since the process which determinizes an automaton assumes the presented subset construction—which leads in the worst case to 2^{|A|} states—we have to find a way to keep the resulting automaton as small as possible. The standard solution to this is the minimization of an automaton as found for example in Gécseg and Steinby (1984). The goal of the minimization construction is to find an automaton which has a smaller state set and fewer transitions without altering the recognized language. Minimal automata always exist and are unique up to isomorphism of their transition graph. Unfortunately, however, the minimal automaton can still be very big; nothing prevents the occasional appearance of the worst-case scenario. Still, in the normal case only a few of the state-sets output by the determinization construction are actually needed, and we can reduce the resulting automaton.

Assume that we are given a tree automaton 𝔄 = (A, α, A_{F}), k ≤ |A|. (In the following we are blurring the distinction between an automaton and the underlying algebraic structure.) A simple source of nonminimality is the occurrence of states and transitions which are never used. We defined the set of reachable states already in our discussion of the emptiness problem in section 2.2.3, (equation (1)). In the following we refer to that set as R_{A}. Obviously we can eliminate all other states from the state set without altering the language recognized by the automaton.

Another source of non-minimality is the occurrence of equivalent states, i.e., states which can be substituted for each other in any computation without affecting the result. To be able to achieve the elimination of those equivalent states, we need some auxiliary definitions. Note that we presuppose that indeed all states are reachable.

The following definition ensures that the sequence of equivalence relations which will be defined later is indeed a sequence of congruence relations. This is so since congruences are invariant with respect to unary algebraic functions.^{3}

We are interested in evaluating the behavior of a pair of states a_{1} and a_{2} against a fixed context. That is, given a transition function α(σ), for some σ, and a particular state c, we consider a_{1} to be equivalent to a_{2} just in case α(σ)(a_{1}, c) = α(σ)(a_{2}, c) and α(σ)(c, a_{1}) = α(σ)(c, a_{2}), for all choices of σ and c. That is, assigning a_{1} or a_{2} to a given node never makes a difference in the state that will be assigned to that node’s parent. More formally:

Definition 1. A mapping f : A → A is called an elementary translation of the automaton 𝔄, if there exists m > 0, σ ∈ Σ_{m}, 1 ≤ j ≤ m and elements c_{1}, …, c_{j−1}, c_{j+1}, …, c_{m} ∈ A such that

f(a) = α(σ)(c_{1}, …, c_{j−1}, a, c_{j+1}, …, c_{m}) for all a ∈ A.

We denote the set of all elementary translations by ET (𝔄).

3Lemma I.3.16 in Gécseg and Steinby (1984): An equivalence relation is a congruence relation iff it is invariant with respect to all elementary translations.

The effect of this definition is that f always refers to a certain argument position and leaves the other arguments fixed. Additionally this makes it possible to talk about the behaviour of just two arguments, i.e. states, separately without having to refer to the special context of operations, i.e. elements, from Σ and A.

Any two states whose behaviour is identical can be collapsed into a single one. We define indistinguishability inductively as follows:

Definition 2. Two states p, q ∈ A are called k-indistinguishable iff (i) both are final or both are non-final, and (ii) if k > 0, then for all f ∈ ET (𝔄) both a and b and f(a) and f(b) are

k − 1-indistinguishable. We say that two states are equivalent iff they are k-indistinguishable for all k.

The process has to terminate since our state set is finite, i.e., we can have at most |A| different states and therefore equivalence classes. Equivalence concerning states is determined by demanding indistinguishability concerning all k.

Since we are only interested in the case of m = 2, we can be a little more concrete about the definition of elementary translations and the congruence relations they induce. We obtain an ordered series of congruence relations ≡_{i} on states a_{1}, a_{2} ∈ A with a_{1} ≡_{0} a_{2} iff both are final or both are non-final and a_{1} ≡_{k+1} a_{2} iff a_{1} ≡_{k} a_{2} and for all σ ∈ Σ_{2} and for all c ∈ A

α(σ)(a_{1}, c) ≡_{k} α(σ)(a_{2}, c) (9)

α(σ)(c, a_{1}) ≡_{k} α(σ)(c, a_{2})

Since ≡_{i} = ≡_{i+1} for some i < |A|, this process stops with a largest congruence relation which we call ∼_{A}.^{4}

Since we want to use this congruence relation to minimize the automaton, we have to define what it means to reduce an automaton by a congruence relation. The quotient automaton 𝔄/_{ρ} of an automaton 𝔄 with respect to the congruence relation ρ is

𝔄/_{ρ} = (A/_{ρ}, α_{ρ}, A_{F} /_{ρ}) (10)

α_{ρ}(σ)([a_{1}]_{ρ}, [a_{2}]_{ρ}) = [α(σ)(a_{1}, a_{2})]_{ρ}
for all a_{1}, a_{2} ∈ A and σ ∈ Σ_{2}

4The proof that ∼_{A} is a congruence relation is in Gécseg and Steinby (1984), Theorem II.6.10.

The resulting equivalent automaton represents a real reduction in the number of states in case the congruence was non-trivial. Obviously the greatest congruence achieves the greatest reduction. The recognized forest is preserved under the quotient construction.

Corollary 1 (Gécseg and Steinby (1984) II.6.7). If ρ is a congruence relation, then T (𝔄/_{ρ}) = T (𝔄).

Now we can define what it means to be a minimal automaton.

Definition 3. An automaton 𝔄 is called (i) connected if A = R_{A}, i.e., all states are reachable (ii) reduced if ∼_{A}= id_{A}, i.e., the state set cannot be reduced any further (iii) minimal if it is connected and reduced.

We know that construction of the quotient automaton under a congruence relation preserves the language, but we still have to show that our minimization process indeed finds the least automaton. This is stated in the next theorem.

Theorem 2 (Gécseg and Steinby (1984) II.6.13). For every recognizable forest T there exists a minimal tree automaton which is unique up to isomorphism. If 𝔄 is a connected recognizer of T, then the minimal automaton is 𝔄/_{∼_{A}}.

This suggests the following algorithm for minimization. Minimize an automaton 𝔄 by the following steps:

1. Discard all unreachable states and the transitions on them. This results in a connected automaton 𝔄′ with T (𝔄′) = T (𝔄).

2. Reduce 𝔄′ by constructing the greatest congruence ∼_{A} and the corresponding quotient automaton 𝔄′/_{∼_{A}}.

Some examples for the process of minimization can be found in Appendix A.3.

Note that we can incorporate the reachability test into the algorithms for the other automata constructions. For example, the determinization algorithm constructs the states just blindly as the power set of the previous states. But by constructing the state set incrementally via the transitions from the initial state, we can coroutine parts of the two algorithms. A new state is only introduced into the state set in case it is constructed as the value of some transition on existing states. This leaves just the construction of the congruences and the quotient automaton as a separate step.

2.3. Coding Relations on Finite Sets of Nodes as Sets of Labeled Trees. The decidability of S2S follows from the fact that each relation definable in the underlying language corresponds to a recognizable set of trees. The key to that correspondence is the use of a certain family of alphabets with a particular interpretation—a coding scheme—according to which a tree can represent a tuple of sets of nodes in N_{2}. In this section we set out the essentials of that coding scheme. This scheme is somewhat easier to present if we think of trees as tree domains together with a labeling function than if we think of them as terms.

For an n-ary relation we choose an alphabet

Σ^{n} = \{\underline{0}, \underline{1}\}^{n},

that is, the set of n-ary strings of bits. Then, given a tree t : {1, 2}^{∗} → \{\underline{0}, \underline{1}\}^{n}, if a node w ∈ \{1, 2\}^{∗} has a label t(w) = ⟨k_{1}, …, k_{n}⟩, then wherever k_{i} = \underline{1}, we interpret w as a member of set X_{i}, the ith set variable. In this way we can interpret a Σ^{n} tree as encoding an assignment function for variables in the (monadic second-order) language of S2S. The tree t is interpreted as a function assigning to each X_{i} the set of nodes in which the ith bit is “on”.

In our algebraic approach, Σ^{n} = Σ_{0}^{n} ∪ Σ_{2}^{n}, and Σ_{0}^{n} contains only the single symbol λ. To really pursue the coding scheme in this framework we would have to set up a correspondence between terms in T_{Σ^{n}} and labeled subsets of N_{2}. The best way to do this is probably to define an addressing function addr which assigns to any subterm of a T_{Σ^{n}}-term the string in {1, 2}^{∗} which is its root’s “address”. Then addr assigns the empty string to the whole term, and given an arbitrary subterm t = ft_{1}t_{2}, addr(t_{1}) = (addr(t))1 and addr(t_{2}) = (addr(t))2.^{5} Given this it is relatively easy to view terms as specifying functions from nodes to label symbols. For example, the T_{Σ^{2}}-tree \underline{1}\underline{0}λλ encodes a pair of sets, the first of which contains only the root node, and the second of which is empty.

The construction we embark upon has the following goal, then. Given a formula ϕ in n free set variables, we wish to construct a tree automaton 𝔄_{ϕ} which recognizes all and only the trees encoding satisfying assignments for ϕ. Supposing for a moment that we could write ϕ[t] for the interpretation of ϕ according to the assignment function encoded by t, we would wish to define an automaton constructor 𝔞𝔲𝔱 such that

t ∈ T (𝔞𝔲𝔱(ϕ)) ⟺ N_{2} ⊧ ϕ[t].

5Recalling that N_{2} is primarily a structure of the natural numbers, we can alternatively define addr as follows. The value of addr for the whole term is zero, and given an arbitrary subterm t = ft_{1}t_{2}, addr(t_{1}) = 2·addr(t)+1 and addr(t_{2}) = 2·addr(t)+2.

Technically, we can only encode tuples of sets this way, so we can only encode assignments to sequences of set variables. However, it is relatively easy to deal with individual variables as well. At very least, we can translate to a language in which all individual variables have been replaced one-for-one with set variables which are constrained to denote singleton sets. We can do this because singletonhood is definable in a language without individual variables (in which ⊆ replaces both ≈ and ∈ as the sole ‘built-in’ relation symbol).

Sing(X) ⟺_{def} (∀Y)[Y ⊆ X ⇒ (X ⊆ Y ∨ (∀Z)Y ⊆ Z)] ∧ (∃Y)[X ⊈ Y]

This formula looks rather forbidding, but the minimal automaton corresponding to it is quite simple. (In fact it can be constructed by hand without any difficulty.) For the case of Σ^{1}, the automaton is as follows.

𝔄 = ({a_{0}, a_{1}, a_{2}}, α, {a_{1}}), (11)

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

all other transitions are to a_{2}

The set of trees encoding Sing(X_{1}) is then just T (𝔄). (It is easily seen that this automaton is just counting the number of occurrences of \underline{1} in the number system “zero, one, (too) many.”) Where several variables are required to be singletons, the conjunction construction can be applied to multiple copies of this automaton.

There is yet a third solution, which is one we will often employ in practice. It is quite easy to assure as part of the construction of primitive automata that certain sets can contain only one member. In effect, this amounts to constructing the relevant cross product automaton, optimizing it and renaming the states. We will see a number of examples of this technique in §2.5.

Note that the set of trees which represent a certain tuple of sets will necessarily be infinite. To see this note that the n-tuple \underline{0}^{n} labels a node which plays no direct role in the sets being picked out. Now suppose we have a tree t which represents the desired tuple. All of its leaves are labeled λ, our sole zero-place function symbol, which plays no role in the representation of the tuple. Clearly we can take any of these λ-labeled nodes and replace it with \underline{0}^{n}λλ without either adding, removing or displacing any node marked for membership in one of the sets. Furthermore we can repeat this process as often as we like. Any tree we derive in this manner will represent the same tuple of sets as the tree with which we started. The same procedure can go in the other direction as well: any subtree of the form \underline{0}^{n}λλ can be replaced with λ, and we can do this as often as we like without affecting the tuple of sets which the tree represents.

Two courses are open to us. If we want to be able to say “the tree” that officially encodes tuple K, then we must take steps to isolate one member of this infinite set for special treatment. Both Doner (1970) and Thatcher and Wright (1968) ultimately follow this course. On the other hand, as Doner (1970) shows, given any set of trees which represent a given tuple, both its minimal member and its “closure” under extension with and removal of filler-trees \underline{0}^{n}λλ form recognizable sets. In spite of historical precedent, it seems to us that the encoding via the closure is simpler to implement than the encoding via minimal representatives, and that is the one we will pursue here. From now on we will distinguish the following two notions:

• a set of trees represents the relation made up of the tuples the trees encode;

• a set of trees encodes a relation just in case it contains all of the

trees that encode each tuple of the relation. Note that encoding is a strictly stronger notion than representation; a set which encodes a relation necessarily represents it, but a set which (merely) represents a relation need not encode it. We will be at some pains to ensure that the automata we construct for a given formula recognize that formula’s encoding.

So now we can say what it means for a relation on ℘_{fin}N_{2} to be recognizable. An n-ary set-valued relation is a subset of (℘_{fin}N_{2})^{n}. Each member of R ⊆ (℘_{fin}N_{2})^{n} is thus an n-tuple of (finite) sets of nodes, and can be encoded by a (finite) Σ^{n}-labeled tree. The relation R is, then, encodable by a set of trees, namely the full set of trees which encode its members. So we have the following.

Definition 4. An n-ary relation R is recognizable if and only if it can be encoded by a recognizable set of Σ^{n}-trees.

2.3.1. Some More Constructions. Now that we have our coding scheme in place, we will need some more constructions in order to implement it. We need in particular a construction to deal with the following case.

Suppose we have an automaton 𝔄 which recognizes the following Σ^{2}-tree, together with all of its extensions by \underline{0}\underline{0}λλ.

\begin{matrix}\underline{1} & \underline{0} \\ \begin{matrix}\underline{0} & \underline{1} \\ λ & & λ \end{matrix} & λ \end{matrix}

Now take the projection function P defined as follows:

P : Σ^{2} → Σ^{1} = ⟨k_{1}, k_{2}⟩ ↦ ⟨k_{1}⟩

Then applying P̄ to the tree above yields

\underline{1} ; \underline{0} ; λ  λ  λ

So the automaton we derive by applying the projection construction to 𝔄 will recognize this tree and all of its extensions by \underline{0}λλ.

Now, our original automaton, 𝔄, recognized the official encoding of a certain relation (essentially the relation holding between nodes which are the root and nodes which are the first successor of the root). But this is no longer true of the projected automaton! In particular, it will not recognize the following tree, obtained by replacing the subtree \underline{0}λλ with λ, even though this tree encodes the same 1-tuple of sets as the tree above.

\underline{1} ; λ λ

Therefore we need to do a little clean-up work if we want our automata to maintain the official encoding. This is not just a matter of pointless bookkeeping! If T (𝔄) encodes a given relation, then its complement encodes the complement of the relation. But now if we complemented the projected automaton (even after making it deterministic!), we would wind up with a set of trees containing the tree above, which therefore does not even represent the complement of the projection of T (𝔄), since that tree encodes a tuple in T (𝔄).

First, let us define the set V of trees as being those subtrees of trees in P̄(T (𝔄)) which are labeled only with λ and \underline{0}. We need to compute the set of states A_{V} which are assigned by h_{A} to members of V. This is easy to do: we need only a slight variant of the procedure of section §2.2.3 for checking the emptiness of an automaton’s recognized forest. There we allowed node-labels to range freely over the alphabet. All we need to do now is to fix our attention on transitions for nodes labeled with \underline{0}’s. We proceed as follows.

A_{V}^{0} = α(Σ_{0}) (12)

A_{V}^{m+1} := A_{V}^{m} ∪ \{a|(∃a_{1}, a_{2} ∈ A_{V}^{m})[α(\underline{0}^{n})(a_{1}, a_{2}) = a]\}
i.e., A_{V}^{m} ∪ α(\underline{0}^{n})(A_{V}^{m} × A_{V}^{m})

A_{V} := ⋃_{m<ω} A_{V}^{m}

Once again, the construction is guaranteed to reach a fixpoint in a number of steps bounded by the size of A. At that point, A_{V} = A_{V}^{m}.

Now we construct from 𝔄 a nondeterministic automaton 𝔄′, as follows.

𝔄′ = (A, ρ, A_{F}), (13)

ρ(λ) = A_{V} ,
ρ(σ)(a_{1}, a_{2}) = {α(σ)(a_{1}, a_{2})}

(Note that the resulting automaton 𝔄′ is only truly nondeterministic at the leaves of a tree.) In describing the construction we tacitly assumed that the input was a deterministic automaton; we will in general be applying it to nondeterministic automata, but this does not present us with anything like the kind of problems we have with complementation. We simply need to modify the procedure for constructing A_{V} to read

A_{V}^{m+1} := A_{V}^{m} ∪ ⋃\{Q|(∃a_{1}, a_{2} ∈ A_{V}^{m})[α(\underline{0}^{n})(a_{1}, a_{2}) = Q]\} (14)

and we need to remove the set braces from the definition of the transition functions, so that it now reads as follows.

ρ(σ)(a_{1}, a_{2}) = α(σ)(a_{1}, a_{2}) (15)

This gives us a “roll-up” or truncation construction. For completeness we should provide also a closure construction which guarantees that the entire extension got by replacing λ-trees with \underline{0}^{n}λλ-trees is recognized. Note however that in practice, while we need the truncation construction, we do not need the closure construction, since its behavior can be easily built into the primitive automata and is inherited under the various constructions. (The curious reader is referred to the proof of Lemma 11 in Thatcher and Wright (1968).)

2.4. The Decidability Proof (Inductive Step). In this report we wish to emphasize the “modular” nature of the decidability proof, by tackling the inductive step first. This step is common to proofs of the decidability of both the language of S2S and L_{K,P}^{2} , and indeed it assures the decidability of any monadic second order language with “automatondefinable” atomic formulas. So we will here assume an arbitrary monadic second-order language L, assuming only that all relations definable by L’s atomic formulas alone are recognizable.

First, all sentences of L are either of the form (∃X)ϕ or of the form ¬(∃X)ϕ. We know that

N_{2} ⊧ ((∃X)ϕ) iff there is an A ⊆ N_{2} and N_{2} ⊧ ϕ(A)

Such an A exists just in case the (unary) relation defined by ϕ is nonempty. (Each member of that unary relation is a potential candidate for X.) By the same token, N_{2} ⊧ ¬(∃X)ϕ just in case the relation defined by ϕ is empty. So the decidability of L reduces to the decidability of emptiness for the L-definable relations.

This indicates our strategy. If we can show that all L-definable relations are recognizable then, knowing that the emptiness of recognizable sets is decidable, we have immediately that the emptiness of L-definable relations is decidable, and so membership of L-sentences in the L-theory of N_{2} is decidable as well.

We prove this by induction. In the next section we will prove that the atomic wffs of L_{K,P}^{2} define recognizable relations, by the brute force approach of actually exhibiting the automata which witness this fact. To prove the inductive step, we must prove the following claim (which is essentially Lemma 19 in Thatcher and Wright (1968), and the second half of Theorem 3.7 in Doner (1970)):

Theorem 3. If formulas ϕ and ψ define recognizable relations, then so do

1. ϕ ∧ ψ,

2. ¬ϕ,

3. (∃X)ϕ.

The proof is a matter of exhibiting the constructions by which we arrive at 𝔞𝔲𝔱(ϕ ∧ ψ), 𝔞𝔲𝔱(¬ϕ) and 𝔞𝔲𝔱((∃X)ϕ), given 𝔞𝔲𝔱(ϕ) and 𝔞𝔲𝔱(ψ).

Case 1: Conjunction. Unsurprisingly, the construction which proves the conjunction case is based on the construction for the intersection of two recognizable sets ((3), p. 8). However, simple intersection is not quite enough, since ϕ and ψ may differ on their variables. Suppose that ϕ has free variables X_{1} and X_{2}, while ψ has free variables X_{2} and X_{3}. That is, ϕ defines relation R(X_{1}, X_{2}) while ψ defines relation S(X_{2}, X_{3}). Our first problem is to get the relations to “line up”. The solution is as follows. Clearly, R is the projection of some relation R′(X_{1}, X_{2}, X_{3}), under a projection P_{3} which maps ⟨k_{1}, k_{2}, k_{3}⟩ ↦ ⟨k_{1}, k_{2}⟩. Similarly, S is the projection of a relation S′(X_{1}, X_{2}, X_{3}) under a projection P_{1} which maps ⟨k_{1}, k_{2}, k_{3}⟩ ↦ ⟨k_{2}, k_{3}⟩. Since the recognizable sets are closed under inverse projection (“cylindrification”), and since by assumption both R and S are recognizable, it must be the case that R′ and S′ are recognizable as well.

So the first step is to identify the relevant projections and invert them, giving us automata 𝔄′ and 𝔅′ recognizing R′ and S′, respectively. Now R′ ∩ S′ is a 3-ary relation which is just

bh_{A′×B′}(A_{F} × B_{F}).

(Recall that the inverse projection construction preserves the states and final states of its inputs; for example, 𝔄′ = (A, α′, A_{F}), where only the transition function differs from 𝔄.)

The same construction can be extended to handle formulas that overlap on any number of variables.

Case 2: Negation. This case is relatively straightforward, as long as we can make the following assumption. If we are attempting to construct 𝔞𝔲𝔱(¬ϕ), we must be able to assume that 𝔞𝔲𝔱(ϕ) is deterministic. The conjunction construction, and the complementation construction itself, preserve this property of their inputs, and all of the atomic automata are deterministic, so we need only worry about this constraint in the case of existential quantification, to be considered below.

As long as our determinism constraint is satisfied, the construction for 𝔞𝔲𝔱(¬ϕ) is just complementation. If

𝔞𝔲𝔱(ϕ) = (A, α, A_{F}),

then

𝔞𝔲𝔱(¬ϕ) = (A, α, A − A_{F})

and that is that.

Case 3: Quantification. The core of this construction is the projection construction from §2.2.4. We wish to construct 𝔞𝔲𝔱((∃X_{i})ϕ), given 𝔞𝔲𝔱(ϕ). Suppose ϕ defines a relation

R(X_{1}, …, X_{i}, …, X_{n}).

Then 𝔞𝔲𝔱(ϕ) is a Σ^{n} automaton that recognizes trees each of which encodes a tuple of subsets ⟨S_{1}, …, S_{n}⟩. ((∃X_{i})ϕ)(S̄) is satisfiable by any sequence of sets S̄ whose i-th member can be replaced by a set S′_{i} such that ϕ(S̄[\frac{S′_{i}}{X_{i}}]) is satisfiable. That formula is satisfiable if the set of tuples of sets which satisfy it is not empty. That set of tuples is the relation ϕ defines. So (∃X_{i})ϕ defines a relation which is a projection of the relation defined by ϕ, where the projection essentially removes or suppresses the ith member of the elements of Σ^{n} to yield Σ^{n−1}.

The projection function corresponding to the quantifier prefix (∃X_{i}) is the following.

P_{i} : Σ^{n} → Σ^{n−1} = ⟨k_{1}, …, k_{i}, …, k_{n}⟩ ↦ ⟨k_{1}, …, k_{i−1}, k_{i+1}, …, k_{n}⟩ (16)

In section §2.3.1 we observed that the output of this construction need not recognize an encoding, even when its input does. It was for just this purpose that we developed the truncation operation, and we apply it here. But we are not done yet! Both projection and truncation introduce nondeterminacy into the automaton, and we must therefore determinize the output in case we later apply complementation.^{6} So the sequence of steps we must go through are as follows.

1. Apply the projection construction.

2. Apply the truncation construction.

3. Apply the subset construction. This gives us a deterministic automaton which recognizes the projection of the encoding of T (𝔞𝔲𝔱(ϕ)).

2.5. The Decidability Proof (Various Base Steps). The base of the induction involves proving that the relations definable by atomic formulas of the relevant language are recognizable. In the case of L_{K,P}^{2} , then, we must prove five cases.

Theorem 4. The relations defined by the following formulas are all recognizable.

1. x ⊲^{+} y,

2. x ⊲ y,

3. x ≺ y,

4. x ≈ y,

5. x ∈ X.

We prove theorem 4 by brute force, exhibiting five automata which recognize the encodings of the five relations defined in the theorem.

Keep in mind, however, that our encoding scheme is defined as if all our variables were set variables. We will see below that in all of these proofs the assignments to individual variables appearing in these formulas are constrained to be unique. Put another way, it is as if we translated our formulas to a language containing only set variables, but where certain of these sets were in addition constrained to be singletons. (That is, we appear to adopt a typographical convention which requires all lower-case variables to denote singleton sets. Note that we still write x_{i} ∈ X_{j}, not x_{i} ⊆ X_{j}.)

6As a matter of efficiency, it may be better to delay determinization until a negation is actually encountered, at which time we can also minimize the resulting automaton.

Case 1: Dominance. We define here a Σ^{2}-automaton 𝔄 such that T (𝔄) encodes the relation defined as x_{1} ⊲^{+} x_{2}.

𝔄 = ({a_{0}, a_{1}, a_{2}, a_{3}}, α, {a_{2}}), (17)

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

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

α(\underline{0}\underline{0})(a_{0}, a_{i}) = a_{i}, a_{i} ∈ \{a_{0}, a_{1}, a_{2}\}, all other transitions are to a_{3}.

Note that for any tree recognized by 𝔄, only a single node can be labeled \underline{1}\underline{0} and only a single node can be labeled \underline{0}\underline{1}. That is, variables x_{1} and x_{2} are assigned to unique nodes by any variable assignment encoded by a tree in T (𝔄). This is assured by the fact that all subtrees peripheral to a path containing denotata for x_{1} and x_{2} must be assigned a_{0} by 𝔄. But no subtree containing either \underline{0}\underline{1} or \underline{1}\underline{0} (or for that matter \underline{1}\underline{1}) can be assigned a_{0}. So nodes for x_{1} and x_{2} must be found on a single path to the root, and, clearly, they can only be found once on any given path. Informally, the automaton 𝔄 is in state a_{0} while it is looking for an occurrence of a node labeled \underline{0}\underline{1}. Once it has found such a node it changes to a_{1}, which means that it is currently searching for a node labeled \underline{1}\underline{0}. Once it has found such a node it switches to the final state a_{2}.

As long as 𝔄 sees only nodes labeled \underline{0}\underline{0}, it remains in whatever state it is currently in, so the node denoted by x_{1} can be arbitrarily far above the node denoted by x_{2}, and both can be embedded arbitrarily deeply in the tree, and arbitrarily far above the frontier. This last point assures that 𝔄 recognizes a true encoding. Since the tree λ and any tree containing only zeroes and λ’s are all assigned a_{0} (only), they can be freely substituted for each other and so we have the effects of both truncation and closure built into the automaton.

Case 2: Immediate Dominance. The immediate dominance automaton is a simple variant of the dominance automaton of the last paragraph. We need only disallow \underline{0}\underline{0} from intervening between the node labeled \underline{0}\underline{1} and the node labeled \underline{1}\underline{0}. That is, we can remain in state a_{1} only momentarily.

𝔄 = ({a_{0}, a_{1}, a_{2}, a_{3}}, α, {a_{2}}), (18)

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

α(\underline{0}\underline{0})(a_{i}, a_{0}) = a_{i}, a_{i} ∈ \{a_{0}, a_{2}\}

α(\underline{0}\underline{0})(a_{0}, a_{i}) = a_{i}, a_{i} ∈ \{a_{0}, a_{2}\} all other transitions are to a_{3}.

Case 3: Precedence. Essentially, x_{1} ≺ x_{2} just in case there is a pair of sisters the leftmost one of which (reflexively) dominates x_{1} and the rightmost one of which (reflexively) dominates x_{2}. The automaton encodes this fairly directly.

𝔄 = ({a_{0}, a_{1}, a_{2}, a_{3}, a_{4}}, α, {a_{3}}), (19)

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

all other transitions are to a_{4}.

Once again, the set of nodes labeled \underline{1}\underline{0} is a singleton, and likewise for \underline{0}\underline{1}. Also, 𝔄 does recognize an official encoding of the precedence relation, though this fact is a little trickier to establish here. A simple inductive argument suffices, however, to show that h_{A}(λ) = a_{0} and, whenever h_{A}(t_{1}) = a_{0} and h_{A}(t_{2}) = a_{0}, then h_{A}(\underline{0}\underline{0}t_{1}t_{2}) = a_{0}. So, in essence, all representations of the tuple of empty sets are treated equivalently.

Case 4: Equality. The automaton for x_{1} ≈ x_{2} is designed to scan an input tree for a single node labeled \underline{1}\underline{1}.

𝔄 = ({a_{0}, a_{1}, a_{2}}, α, {a_{1}}), (20)

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

α(\underline{0}\underline{0})(a_{i}, a_{0}) = a_{i}, a_{i} ∈ \{a_{0}, a_{1}\},

α(\underline{0}\underline{0})(a_{0}, a_{i}) = a_{i}, a_{i} ∈ \{a_{0}, a_{1}\}, all other transitions are to a_{2}.

Again, only a single node labeled \underline{1}\underline{1} is tolerated. All other nodes must be labeled \underline{0}\underline{0} or λ. As usual, the automaton does not distinguish subtrees \underline{0}\underline{0}λλ from subtrees λ.

Case 5: Set membership (a.k.a. ‘singleton subset’). The automaton for x_{1} ∈ X_{2} (properly, x_{1} ⊆ X_{2} ∧ Sing(x_{1})) is essentially just like the automaton for equality, except that now only x_{1} is constrained to appear uniquely. Nodes labeled \underline{0}\underline{1} may appear freely; in fact they are indistinguishable from \underline{0}\underline{0}, reflecting that the relation here defined is completely indifferent to the size of X_{2}, as long as it is at least 1.

𝔄 = ({a_{0}, a_{1}, a_{2}}, α, {a_{1}}), (21)

α(λ) = a_{0},
α(\underline{1}\underline{1})(a_{0}, a_{0}) = a_{1},
α(\underline{0}k)(a_{i}, a_{0}) = a_{i}, k ∈ \{\underline{0}, \underline{1}\}, a_{i} ∈ \{a_{0}, a_{1}\},
α(\underline{0}k)(a_{0}, a_{i}) = a_{i}, k ∈ \{\underline{0}, \underline{1}\}, a_{i} ∈ \{a_{0}, a_{1}\},

all other transitions are to a_{2}.

This completes the “brute force” proof of the base case for decidability of our language.

So far, we have been content to restrict our attention to the most convenient alphabet (that containing only the two variables mentioned in the formulas). We pause here to show briefly how to rigorously describe the more general case. We take as our example the equality automaton, which has the smallest transition table. We assume an arbitrary (finite) value of n, giving us as our alphabet Σ^{n} = Σ_{0}^{n} ∪ Σ_{2}^{n} = \{λ\} ∪ \{\underline{0}, \underline{1}\}^{n}. We assume also the n projection functions π_{1}, …, π_{n}, such that π_{i} := (k_{1} … k_{n} ↦ k_{i}). Then 𝔞𝔲𝔱(x_{i} ≈ x_{j}) can be described by the following assertions.

𝔞𝔲𝔱(x_{i} ≈ x_{j}) = ({a_{0}, a_{1}, a_{2}}, α, {a_{1}}), (22)

α(λ) = a_{0},
α(σ)(a_{0}, a_{0}) = a_{1}, iff π_{i}(σ) = \underline{1} and π_{j}(σ) = \underline{1},
α(σ)(a_{i}, a_{0}) = a_{i}, iff π_{i}(σ) = \underline{0} and π_{j}(σ) = \underline{0},
α(σ)(a_{0}, a_{i}) = a_{i}, iff π_{i}(σ) = \underline{0} and π_{j}(σ) = \underline{0},

all other transitions are to a_{2}.

Note that doing things in this abstract way might simplify some of our constructions. In particular, in considering the proper construction to correspond to conjunction, we had to consider the case that the two input formulas did not share all of their variables. As a result we had to invoke the inverse projection construction. However, once we translate our automata to this more abstract form, we free them to a great extent from the underlying alphabet, and in particular the inverse projection step is no longer required as part of the conjunction construction. But we will not implement this idea for the constructions. For a discussion of this issue, see section 3.2.

3. Implementational Issues

3.1. Introduction. In this part of the report we describe the prototype MoSeL and its implementation in some detail. MoSeL is a compiler which transforms L_{K,P}^{2} formulas to tree automata. Our implementation (in SIC-Stus Prolog) follows point-for-point the decidability proof described in the previous chapter. Therefore its correctness is almost trivially established.

In a sense MoSeL represents a case study in a slightly unusual approach to automated theorem proving. We do not employ the standard techniques of resolution based theorem proving, model construction or tableau methods. Instead we translate the formulas to tree automata, which are themselves neither models nor, properly speaking, syntactic theories. Nonetheless, the results on which our research is based establish that the language recognized by a tree automaton is non-empty iff the formula is satisfiable. Tree automata recognize an encoding of the assignment under which the formula is satisfiable. Models for the formula can be generated by recording the generation process for these assignment trees, i.e., the automata encode the models allowed by the formula. In a certain sense the automata with non empty languages are a normal form. In this respect our work is similar to MONA (Henriksen et al. 1995). MONA, too, is a tool to compile formula of a monadic second order logic – but on strings – into finite state automata. The connection to our work on the monadic second order tree description logic L_{K,P}^{2} is straightforward. It corresponds to the step from Büchi’s (Büchi 1960) result on S1S to Rabin’s (Rabin 1969) result on S2S.^{7}

Automated theorem proving gains its importance for computational linguistics from the fact that processing with grammar formalisms couched in logic can be seen as such. So, one goal of our approach is to provide a tool to verify and use descriptions about natural language presented in L_{K,P}^{2} .

The chapter proceeds as follows. We start by outlining the datastructure for the tree automata. Then we have a section on some work which can be done before the actual processing starts. The fourth section presents the compiler and the implementations of the constructions discussed in the first chapter. We conclude with a discussion of strengths and weaknesses of MoSeL.

3.2. The Data-Structure. For the Presentation of the data structure for tree automata it seems easiest to take an example and explain the data-structure from there. Consider again the automaton for equality as presented in (20). In Figure 1 we depict the automaton for equality of two singleton sets (x_{1} ≈ x_{2}) as a list of trees. We assume that the current alphabet ranges over two variables, i.e., there exist four different alphabet symbols, corresponding to the cases where a given node has been assigned to x_{1}, to x_{2}, to both, or to neither. We will transform this most basic representation step by step to the one we are actually going to use.

a_{0}  a_{1}  a_{2}
nonfin  fin  nonfin
a_{0}  a_{2}  a_{1}  a_{0}  a_{2}
\underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1} a_{1} \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1} a_{0} \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1} a_{2} \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1} a_{1} \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1}
a_{0} a_{2} a_{2} a_{1}  a_{2} a_{2} a_{2} a_{2}  a_{2} a_{2} a_{2} a_{2}  a_{2} a_{2} a_{2} a_{2}  a_{2} a_{2} a_{2} a_{2}
\underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1}  \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1}  \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1}  \underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1}
a_{1} a_{2} a_{2} a_{2}  a_{1} a_{2} a_{2} a_{2}  a_{2} a_{2} a_{2} a_{2}  a_{2} a_{2} a_{2} a_{2}

Figure 1. The full equality automaton for x_{1} ≈ x_{2}

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

We keep a list of states on the top level which are marked as final or non-final. From each of these states hangs another list of states. This is to be interpreted as the states from the topmost list being the left state of a transition and the states from the lower one as the right. Each arc ends in a pair with the alphabet symbol being represented with the relevant bit string followed by the resulting state. As an example for a transition suppose we want to find α(\underline{1}\underline{1})(a_{0}, a_{0}). We go to a_{0} in the topmost layer, find a_{0} hanging off of it, then find its daughter labeled \underline{1}\underline{1} and the resulting state a_{1}.

Obviously this is a rather space consuming representation. For example, note that most transitions are to a_{2}. But a_{2} is a non final state which cannot be left once it is entered. In other words, it is a sink state. So far our example represented a total transition table, but in the first chapter of this report we already simplified the representation of automata considerably by just stating that all other transitions are to a sink state. So the most obvious optimization is to switch to a partial transition function. We can identify the sink state automatically and then remove, or rather not construct, all the transitions resulting in it. If there are no remaining transitions on a pair of states, we can eliminate that pair as well. Note that we still keep the sink state in our topmost list for convenience. This will be explained further in the discussion of the negation construction. Our new automaton looks as presented in Figure 2.

a_{0}  a_{1} a_{2}
nonfin  fin nonfin
a_{0}  a_{1} a_{0}
\underline{0}\underline{0} \underline{1}\underline{1} \underline{0}\underline{0} \underline{0}\underline{0}
a_{0} a_{1} a_{1} a_{1}

Figure 2. The equality automaton without sink transitions

This automaton is already a lot smaller than the previous one, but in the general case we can still do better. To facilitate access to the results of transitions we represent the alphabet with the results not as a plain list but as a balanced binary search tree. A tree is balanced iff for every node the heights of its two subtrees differ at most by one. Access, deletion and insertion become in the worst case O(log n) operations. Obviously our bit vector representation of the alphabet corresponds to natural numbers. We use these as the keys to access and sort these balanced trees. The actual implementation uses the library assoc provided with the SICStus Prolog distribution (SIC 1995). This makes the nesting deeper, but we do not have to search the whole list if we want to find the result of a specific transition. Again in our example this does not result in a real change since we only have at most two elements in the lowest lists left. Nevertheless, the new automaton is depicted in Figure 3. We marked the balanced tree which is relevant for the pair of states (a_{0}, a_{0}). Accessing the result of the transition means now to find the relevant key in the balanced tree and to extract the corresponding value. Note that t denotes the empty balanced tree and serves as a terminator. We also identify the sink state with the atom sink. Keeping the sink state unique helps in reducing the state space and saves some of the labor of minimization.

a_{0}  a_{1}  sink
nonfin  fin  nonfin
a_{0}  a_{1}  a_{0}
\begin{aligned}& 3 \\ & a_{1} \\ & 0 & t \\ & a_{0} \\ t & t \end{aligned}  \begin{aligned}& 0 \\ & a_{1} \\ t & & t \end{aligned}  \begin{aligned}& 0 \\ & a_{1} \\ t & & t \end{aligned}

Figure 3. The equality automaton with balanced trees

To translate this representation into Prolog we use explicit lists of states with dependent substructures, either again a list or an association tree. We present the actual data-structure in EBNF-like notation in Table 1. In the table we allow ourselves the use of standard Prolog notation for lists, i.e., in the expression [ H | T ]H stands for the head of the list and T for the tail. (This can create some confusion since | is also the EBNF symbol for disjunction or alternation.)

The first argument of the automaton contains the initial state(s), the second one a list of state trees. The initial state has to be unique in principle, but can become a non-singleton list under the quantification construction. Each state tree consists of two parts: a header, containing the actual state-name and an indication of its final/nonfinal status, followed by an association list of states. Each element of that list consists

          AUT → aut( NESTATELIST, NETREELIST )
  NESTATELIST → [ STATE | STATELIST ]
    STATELIST → []  |  NESTATELIST
   NETREELIST → [ STATETREE | TREELIST ]
    STATETREE → HEADER - ASSOCLIST
     TREELIST → []  |  NETREELIST
    ASSOCLIST → []  |  [ STATE - NEASSOC | ASSOCLIST ]
      NEASSOC → t( NUM, STATE, NUM, ASSOC, ASSOC ) |

                   t( NUM, NESTATELIST, NUM, ASSOC, ASSOC )

        ASSOC → t  |  NEASSOC
       HEADER → ( STATE, MARKER )
       MARKER → fin  |  nonfin

NUM → n ∈ IN

        STATE → atom

Table 1. The data-structure for tree automata ported to Prolog

again of the actual state and a balanced tree. Concerning the association tree note that t denotes the empty balanced tree and t( K, A, N, T1, T2 ) stands for a balanced tree with key K, content A, difference in depth of the subtrees N and left subtree T1 and right subtree T2. The content of a particular node can be either a state if the automaton is deterministic or a list of states if the automaton is nondeterministic. State names are arbitrary Prolog atoms with sink being the distinguished atom representing the sink state. By forcing non-empty lists on both the list of initial states and the list of state trees we capture the restriction that we have to have at least one (initial) state. Similarly, if we have a state in our association tree list it has to have a non-empty association tree. Otherwise all transitions are to sink and the state would have had to be removed.

In Figure 4 we show as an example the corresponding “pretty printed” version of the equality automaton in Prolog.

This data structure uses alphabet symbols as keys in the association trees. This means that the data structure for x_{1} ≈ x_{2} is different from the data structure for x_{23} ≈ x_{17}. Considering that we want to maintain a library of already compiled automata, it seems problematic to have such a concrete representation of automata only. Therefore we employ the projections presented in Section 2.5 to allow a generic representation of automata in the database. There we do not have this tree like presentation but rather Prolog clauses, each representing a transition on variable

             aut( [ a0 ],
                  [ (a0,nonfin)-
                       [ a0-t(3,a1,-1,t(0,a0,0,t,t),t),
                         a1-t(0,a1,0,t,t) ],
                    (a1,fin)-[ a0-t(0,a1,0,t,t ) ],
                    (sink,nonfin)-[] ]
                )

Figure 4. The equality automaton in Prolog

                 states( e(_,_), [q0,q1,sink] ).
                 finals( e(_,_), [q1] ).
                 m( e(_,_), lambda, q0 ).
                 m( e( A, B ), S, Q1, Q2, Q ) :-
                       pi( A, S, IBit ),
                       pi( B, S, JBit ),
                       m0( e, IBit, JBit, Q1, Q2, Q ).
                 m0( e, 0, 0, q1, q0, q1 ).
                 m0( e, 0, 0, q0, q1, q1 ).
                 m0( e, 1, 1, q0, q0, q1 ).
                 m0( e, 0, 0, q0, q0, q0 ).

Figure 5. Prolog clauses for the generic equality automaton.

alphabet symbols by using the projections as an intermediate layer. (See Figure 5.)

We identify the relevant automaton by the use of an appropriate tag. In the example in Figure 5, the tag is the Prolog term e(A,B), where the variables A and B are assigned the names of the particular variables being equated. Since these names correspond to bit-positions in the alphabet symbols, we can use them in calling the projection functions pi/3 to test the relevant bits. More on these tags will be found in Section 3.4.1. With these abstract representations of automata for particular relations we do not have to have new automata in the database for each new alphabet constellation. When compiling an actual formula, we use these abstract automata as source code and compile them to our tree data-structure which is then used by the theorem prover. This is one of the tasks of the preprocessor, to which we now turn.

3.3. The Preprocessor. The formula preprocessor serves multiple purposes. First, we allow the input of formulas in a fairly “user-friendly” form, i.e., with lowercase letters for singleton variables and uppercase letters for set valued variables, so we have to convert the input from this format to our internal representation, that is, bit vectors whose bit positions correspond to particular variable names. So one purpose of the preprocessor is to count the number of variables appearing in the input and replace them with natural numbers representing their position in the bit vector. Currently this is done from the outside in, that is, the outermost variable gets assigned the lowest number. Doing things this way simplifies the projection construction. In projection we work our way from the inside out, so we can always just discard the highest numbered variable. More on this in section 3.4.4.

The second purpose of the preprocessor is to introduce the necessary singletonhood constraints for the appropriate variables. As mentioned previously, the basic automata contain the necessary constraints on singletonhood for their variables. But since this is just an abbreviation, we have to be very careful under negation. Consider the formula ¬x ≈ y. Given the automaton in Figure 5, this is satisfied under an assignment which maps x, for example, to two distinct nodes. That is, the equality automaton will fail in this case, because it is designed to enforce singletonhood, and so the automaton for the entire formula will succeed. That is, if we do nothing else, this formula yields the same automaton as

¬(Sing(x) ∧ Sing(y) ∧ x ≈ y).

We wish our automata to respect the typing of the variables in the input formula. That is, the automaton we really want is the automaton for

Sing(x) ∧ Sing(y) ∧ ¬x ≈ y.

Therefore we have to add the necessary singletonhood statements, and in the right places. For bound variables, this just means converting quantifiers over individual variables to restricted quantifiers over singleton set variables. For free individual variables, the singleton constraints must appear conjoined with the entire formula.

The third purpose of the preprocessor is to do cylindrification. Since for example conjunction just works for relations on the same set of variables we have to make sure that we actually know the scope of the alphabet at each formula. Suppose we have two formulas x_{1} ≈ x_{3} and x_{2} ⊲^{+} x_{3}. To be able to conjoin them, they both have to be compiled to automata scanning for all three variables, although for each component automaton only two are relevant. To achieve this, the preprocessor counts the numbers of free variables for each subformula and annotates each construction with them. The process which makes the automata concrete can then take this information and create the appropriate bit-strings.

Again we are going to illustrate this with an example. Consider the formulas in (23)–(26). We use ˆ for quantification and ˜ for negation. The tag e stands for the equality automaton, rd for reflexive dominance and sing for singletonhood.

(∃x_{1})[x_{1} ≉ x_{2} ∧ x_{1} ⊲^{∗} x_{2}] (23)

(24)  (x^(~(e(x,y)) /\ rd(x,y)))
          (sing(1)*1 /\ 2^((((~e(2,1)*2)*2 /\
                 rd(2,1)*2)*2 /\ sing(2)*2)*2)*1)*1

(25)

(Sing(x_{2})^{1} ∧ ((∃x_{1})(((¬(x_{1} ≈ x_{2})^{2})^{2} ∧
(x_{1} ⊲^{∗} x_{2})^{2})^{2} ∧ Sing(x_{1})^{2})^{2}]^{2})^{1})^{1}

(26)

The first line (23) shows the logical formula and the second one (24) the corresponding input to our program. Line (25) shows the converted formula and the last one (26) the output pretty printed in logic with the number of free variables annotating the relevant brackets as powers. We have two basic automata with the alphabet size being two variables. After the first atomic formula has been negated, the two are conjoined. Before we leave the scope of the quantifier on 2, we have to ensure that it remains a singleton set. After the quantification, the scope of the alphabet has been reduced by one. It just remains to constrain 1 to be a singleton. The resulting formula provides all the information for the compiler to work efficiently.

3.4. The Compiler. In general the compiler works just like the inductive proof. We take our formula and generate inside out the appropriate tree automata. This means that after the preprocessing we again recursively traverse the formula. The base case means finding a tag such that a corresponding generic automaton is contained in our library. Then we create a concrete automaton with the right alphabet space and variable labeling in the described data-structure. On return of an automaton we can proceed with the boolean constructions. In this way we build the automaton recognizing the relation which the formula defines. After completion of the compilation we create a new generic automaton and output it. Additionally we allow the specification of a switch which triggers renaming of states. For debugging purposes it seems important to keep as much information as possible. Therefore the constructions can keep the complex state names formed, for example, in the various cross-product constructions or the subset construction. In the case of conjunction this means that the new automaton has pairs of the old states as state names. This enables us to see which conjunct provides which information to the overall automaton. On the other hand leads this bookkeeping to fairly large state names. If we want to work most efficiently it seems best to keep the state names small. In this case we rename the complex names to new atoms.

3.4.1. The Base Case. We start with the base case of the induction. In the proof we stated that we have automata for all the basic relations. The generic representations of those form the core of our library. And furthermore the proof allows us to add any compiled relation, i.e., tree automaton, to our signature. Transfered to the compiler, this means that we can add all the compiled automata to the library, too. Therefore the output of our program is a tree automaton in its generic representation.

To be able to identify the appropriate automaton, we use Prolog terms which represent the formula which is the source for the automaton, with their argument slots for the formula’s variables. As an example, consider the equality automaton in Figure 6 (repeated from Figure 5). Our tag for identifying the automaton is e(X,Y). Note that in case of a concrete query, the preprocessor produces concrete numbers instead of the variables, see (25). The automaton has separate clauses for the states, the final states, an initial transition encoding the initial state and the transition table.

When processing a formula we get the information from the preprocessor how big our alphabet has to be and which positions are occupied in the bit string by the variables. With this information and the generic automaton we are able to construct our tree-like representation by feeding the appropriate bitstrings to the clauses and recording all resulting transitions. The tree representation is then used in the inductive steps.

3.4.2. The Reachability Construction. It turns out that the central construction for the theorem prover is the reachability construction described in section 2.2.3. As we presented in the discussion on minimization, we can discard those states which are not reachable from the initial state. The reachability construction finds exactly the set of reachable states, so we use a variant of it in all the other constructions. The effect of this is that we never construct states which are not reachable. The details of

                states( e(_,_), [a0,a1,sink] ).
                finals( e(_,_), [a1] ).
                m( e(_,_), lambda, a0 ).
                m( e( X, Y ), S, A1, A2, A ) :-
                      pi( X, S, IBit ),
                      pi( Y, S, JBit ),
                      m0( e, IBit, JBit, A1, A2, A ).
                m0( e, 0, 0, a1, a0, a1 ).
                m0( e, 0, 0, a0, a1, a1 ).
                m0( e, 1, 1, a0, a0, a1 ).
                m0( e, 0, 0, a0, a0, a0 ).

Figure 6. The generic equality automaton in Prolog

how to incorporate the this construction into the other constructions is presented in the respective subsections.

We use for the reachability construction the “semi-naïve method” as presented in Ullman (1988) (and see O’Keefe (1990) for a Prolog version on which our code is actually based). This method is helpful when one needs to close a given set under some two-place operation. The essential idea is to keep track of just the truly new data items which are added to the output set on each pass. Supposing we have a current output set S, to which we have just added new data items ΔS. Our specification says that the next iteration should compute S ⊗ S. Naïvely this can be computed by a double recursion on S. The semi-naïve method uses the observation that this equals

(S ⊗ ΔS) ∪ (ΔS ⊗ S) ∪ (ΔS ⊗ ΔS)

which can be computed by an outer recursion on ΔS and an inner recursion on S, for example. When ΔS is typically much smaller than S, we can get very significant savings this way.

3.4.3. The Boolean Constructions. The implementation of the boolean constructions is, apart from the one for negation, straightforward. Both conjunction and disjunction are easily coupled to the reachability construction since they just represent cross products of the component automata.

The outer loop of the cross product construction is presented in Figure 7. Intuitively, the most basic version of this just takes two state lists initialized with the initial state and then finds the states that can be reached from these via the transition function and collects the results in a new list. If the list is non-empty, we continue with the newly added states plus the old ones and continue doing this until no new states have been added. We keep ordered lists of states since this facilitates the necessary operations. When initialized with the initial state, both state lists are identical. In further iterations of the predicate the first argument contains the states found during the last recursive step whereas the second argument contains the states collected so far in all iterations. The inner

  reach_cross_and( Agenda, States, UsedStates, TransA, TransB,
                   InTrans, OutTrans ) :-
        a_and_b( Agenda, States, TransA, TransB, Reachables, [],
                 InTrans, NewTrans ),
        sort( Reachables, SortedRs ),
        merge( SortedRs, States, NewStates, NewAgenda ),
        ( NewAgenda == [] ->
            UsedStates = States,
            OutTrans = NewTrans
        ;
            reach_cross_and( NewAgenda, NewStates, UsedStates,
                             TransA, TransB, NewTrans, OutTrans )
        ).

Figure 7. Cross-product construction for conjunction, outer loop.

loop searches for the transitions in the respective automata and adds the resulting pairs. For example if automaton 𝔄 has initial state a_{0} and automaton 𝔅 b_{0} then we start with the initial pair (a_{0}, b_{0}). Suppose there is a transition in 𝔄 from a_{0} and a_{0} to a_{1} using \underline{0}. And there is a transition in 𝔅 from b_{0} and b_{0} to b_{1} using \underline{0}. Then we can construct the new pair (a_{1}, b_{1}) which enters the construction itself on the next recursive step. Note that now we have to care for the alphabet symbol we use. In the reachability construction it does not matter by which alphabet symbol a new state was introduced, but now we are essentially running two automata in parallel so that a new state pair can only be constructed if both automata have a valid, i.e., non-sink transition on the same alphabet symbol. The implementation has to construct these pairs by generating

 % a_and_b( +NewStatePairs, +OldStatePairs,
 %          +TransitionsAutA, +TransitionsAutB,
 %          -AccReachables, +AccReachables,
 %          +AccNewTransitions, -AccNewTransitions )
 a_and_b( Set1, Set2, TransA, TransB, R0, R, In, Out ) :-
       ( Set1 = [] ->
           R0 = R,
           Out = In
       ;
           Set1 = [A1|RestSet1],
           a1_and_b( Set2, A1, TransA, TransB, R0, R1, In, Out1 ),
           a_and_b( RestSet1, Set2, TransA, TransB, R1, R, Out1,
                    Out)
       ).

Figure 8. The predicate a and b/8.

all transitions on two particular input state pairs and recording the successful ones. We do this by fetching the two balanced trees—one from each input automaton—and merging them. Essentially, from the pair of trees we extract a tree of pairs. We can improve on this by catching early on a number of special cases which entail that we do not have to do the pairing at all. An example of this is the case where one of the balanced trees is empty.

This describes only how to find the necessary new states, but in fact we also do all the work necessary to create the new transition table at the same time. Whenever we find a new pair of states we know which states and alphabet symbols contributed. By recording this information we can incrementally build the new conjunction automaton. For this we merge each newly created transition into our transition tree. The merging is accomplished by successively checking both levels of the respective trees for the occurrence of the relevant transition. So our loop has as arguments the transitions of the old automata, the state pairs generated in the last step of the loop and all the pairs generated previously, and accumulator pairs in which we construct the new pairs and the transition tree. The actual predicate can be seen in Figures 8–10.

The new final states are then just those pairs where both components were final states in the original automata. In the previous construction

a1_and_b( Set2, (A1,A2), TransA, TransB, R0, R, In, Out ) :-
( Set2 = [] ->
R0 = R,
Out = In
;
% Step 1:
Set2 = [(B1,B2)|RestSet2],
access( TransA, A1, B1, TupleA ),
access( TransB, A2, B2, TupleB ),
( TupleA == t ->
    R1 = R0,
    merge_tree( ((A1,A2),_Marker)-[], In, Out1 )
;
    ( TupleB == t ->
        R1 = R0,
        merge_tree( ((A1,A2),_Marker)-[], In, Out1 )
    ;
        pair_and( TupleA, TupleB, OutTuple, States ),
        ( OutTuple == t ->
            R1 = R0,
            merge_tree( ((A1,A2),_Marker)-[],
                        In, Out1 )
        ;
            append( States, R1, R0 ),
            merge_tree(
               ((A1,A2),_Marker)-[(B1,B2)-OutTuple],
               In, Out1 )
        )
    )
),

Figure 9. The inner loop of the conjunction construction: Step 1.

of the new transitions we constructed the appropriate markers for membership in the set of final states by reference to the information of the conjoined automata.

The disjunction construction works similarly. The obvious difference being that now we are essentially running one or the other automaton alternatively. The implementation changes only in respect to which states

           % Step 2:
           access( TransA, B1, A1, TupleC ),
           access( TransB, B2, A2, TupleD ),
           ( TupleC == t ->
               R2 = R1,
               merge_tree( ((B1,B2),_Marker1)-[], Out1, Out2 )
           ;
               ( TupleD == t ->
                   R2 = R1,
                   merge_tree( ((B1,B2),_Marker1)-[], Out1, Out2 )
               ;
                   pair_and( TupleC, TupleD, OutTuple1, States1 ),
                   ( OutTuple1 == t ->
                       R2 = R1,
                       merge_tree( ((B1,B2),_Marker1)-[],
                                   Out1, Out2 )
                   ;
                       append( States1, R2, R1 ),
                       merge_tree(
                          ((B1,B2),_Marker1)-[(A1,A2)-OutTuple1],
                          Out1, Out2 )
                   )
               )
           ),
           a1_and_b( RestSet2, (A1,A2), TransA, TransB, R2, R,
                     Out2, Out )
           ).

Figure 10. The inner loop of the conjunction construction: Step 2.

are now recognized as being valid, i.e., any state pair where we have at least one valid transition.

The only problem is the negation automaton. The problem is due to the partial character of our automaton representation. In principle all negation does is to flip the markers of the states: final becomes nonfinal and nonfinal becomes final. This means that all the transitions which are not present are valid since sink is now a final state. The result is that we have to identify the new sink state, if it exists, and remove all transitions involving it, and also add explicit transitions to the old sink state. This is the price we have to pay for our data-structure. With a total transition function we just have to complement the markers and are done.

Again we use a variant of the reachability construction to find our new sink state(s). We compute both the bottom up fixpoint as before and the top down fixpoint. This means we start from the final states and see which states are reachable working backwards. The implementation of the top down reachability contains nothing different from what we presented so far, therefore we skip it here. The intersection of those two lists of states are the states which can actually be used in a computation with our automaton. The ones which are not used are the new sink states. Since we want to keep the sink state unique, we eliminate all of them and add a new sink state. Since the old atom sink is now a final state, we rename it to a new atom and use sink for the new sink state. With our list of used states we can then reconstruct our transition table. This is fairly simple and involves just one traversal of our transition function since we just have to go through the old table and add those transitions which are not present and eliminate those which contain one of the new sink states. We think that the saving in space is worth this complication.

3.4.4. Other Constructions. The constructions we deal with in this section are projection and the auxiliary ones of minimization, determinization and truncation.

As mentioned before we arrange our variable numbering in such a way that we always project the biggest (remaining) number. We have to traverse our transition table once to alter the alphabet symbols. This is done with the following formula (see Figure 11).

          % project( +AlphSymb, +PosToProject, -AlphSymb )
          project( Symb1, Pos, Symb2 ) :-
                Symb2 is Symb1 /\ ( exp(2,(Pos-1)) - 1 ).

Figure 11. The projection predicate

Input is the old key and the position to be projected, output the new key. Intuitively what happens is that we zero out the relevant position.

If the projection leads to nondeterminism, we actually have a set of new states as the result of a transition. Consider the following example.

(27)  α(\underline{0}\underline{0})(a_{0})(a_{1}) = a_{1}
(28)  α(\underline{0}\underline{1})(a_{0})(a_{1}) = a_{0}
(29)  α(\underline{0})(a_{0})(a_{1}) = \{a_{0}, a_{1}\}

The transitions in (27) and (28) collapse to the single transition in (29) when we project the rightmost bit. Internally this is represented as a list of states in the argument slot reserved for the result in the balanced tree. This means it is necessary to find all transitions on a pair of states before assigning the result into our balanced tree. But again, this does not seem harmful since it just means a reordering of work which has to be done anyway.

To cope with quantification in our logical language we need two more constructions, truncation and determinization. Truncation is a straightforward variant of the reachability construction. Recall that all we need is to collect all states which are reachable by transitions on alphabet symbols consisting of only \underline{0}’s to close the language recognized by the automaton under our encoding. After addition of those states to the initial state our automaton recognizes the right encoding. All that changes internally is that now we have to keep a list of initial states.

In fact, we have two kinds of automata. The standard deterministic ones and the nondeterministic ones resulting from the previously described constructions. But as discussed in section 2.4, complementation does not work for nondeterministic automata. It is an as yet open question when we do absolutely have to determinize our automata or when we can leave them nondeterministic. To do it only when necessary saves much work since the worst case complexity of the underlying subset construction is exponential. Considering the formulas to be in prefix normal form,^{8} we only have to determinize in case there is an alternation in the color of the quantifier, i.e., universal versus existential. We did not implement this yet. So far the program determinizes after every quantification. We are currently investigating how to work with nondeterministic automata as long as possible, i.e., for all constructions apart from negation and only to determinize the automaton in case we have to complement it.

The subset construction will again be tied to the reachability construction. But note that this does not overcome the worst case complexity.

Again the reachability construction is initialized with those subsets of the state set which contain the initial states. Since in our determinized automaton sets of states serve as states, i.e., in a certain sense we use the subsets as complex meaningful names, these form the new initial state. From there reachability takes over and constructs the reachable subsets and the new transition trees. The final states are then just those subsets which contain a final state. The result is a new deterministic automaton with more complex names, but recognizing the same language. Internally the subsets are kept as ordered lists of states, so a little care is required to distinguish real lists of states and these new complex names.

8Although we do not want to imply that this has to be the case. Rather the contrary, since pushing the quantifiers in as far as possible helps in reducing the size of the automata.

The last construction we have to present is minimization. We do this in two steps. The first one finds those states which behave identically and the second one constructs the appropriate quotient automaton. Note that we coded some minimization into the other constructions by keeping the sink state unique. Practical tests have shown that most of the states which are removed by minimization are indeed copies of the sink state. So they are reachable, but they do not contribute in finding solutions. We talked about this only for negation, but we have incorporated heuristics to eliminate some of them into all the other constructions as well. Note that in all cases a unique state sink is only necessary if we are not dealing with a transition function without a sink state. In our data-structure this corresponds to a total transition function, i.e., transition trees in which nothing was removed. The worst case for testing is a traversal of the tree structure with checks whether all states appear at all levels and all alphabet symbols are apparent. This is implemented in such a way that we stop looking for a total transition function if we can find a sublist or balanced tree which is not of the appropriate length or size respectively. If this predicate fails, i.e., all states appear at all levels and all balanced trees are of the complete size, then we are dealing with a total function. Having sink in all transition trees regardless would mean that we can have a unreachable state in the automaton. Since most of the automata we deal with have a sink state, we almost never have to deal with the worst case sketched above. Therefore we think that it is better to test for the totality of the transition representation than to have unreachable states.

Conjunction produces a number of easily identified sink states since every pair which contains sink does not represent a valid transition. We did not even construct those. So the reachability construction does not add any identifiable sink state at all. Nevertheless there might be pairs of states which turn out to be sink states. Disjunction does produce just one sink state namely the pair containing both of the old sink states.

Projection and truncation do not affect the sink state.^{9} But determinization might require a new unique sink state if the transition tree is not total. So far we do not have a heuristic to eliminate subsets which might be sink states. Here we really need minimization.

9If there is a \underline{0} labeled transition into the sink state, then truncation may add the sink state to the initial states, but that does not change it being a sink state.

So we come back to the first step necessary to minimize an automaton. We have to partition the state set into equivalence classes. Note that it is important in which position a state is used with which result. States that are equivalent have to behave identically both as a right and a left state. We start out by separating the final from the non-final states. Then we have to refine each of those partitions further. We do this by assuming that all states in our partition are equal and testing them against the whole state set. If we can find a behavioral difference, we eliminate this possibility. The crucial predicate is shown in Figure 12.

  % equiv( +StateList, +EquivPair, +Transitions, +PreviousEquivs )
  equiv( [], _, _, _).
  equiv( [ QNX | States ], Q1-Q2, Trans, Equivs ) :-
        access( Trans, QNX, Q1, Tuple1 ),
        access( Trans, QNX, Q2, Tuple2 ),
        equiv_tuple( Tuple1, Tuple2, Equivs ),
        access( Trans, Q1, QNX, Tuple3 ),
        access( Trans, Q2, QNX, Tuple4 ),
        equiv_tuple( Tuple3, Tuple4, Equivs ),
        equiv( States, Q1-Q2, Trans, Equivs ).

Figure 12. The central equivalence predicate

In this predicate we recurse on the state list against a pair of states which is assumed to be equivalent. Then we access the relevant balanced trees both with the states as the right and the left state and check those against the equivalence statements constructed so far. If we find a difference, the predicate fails and we are done with this hypothesis. We have to keep on doing this until no more changes in our equivalence partitioning can be discovered. Again we implement it by a loop using the semi-naïve method (see Figure 13).

After we fully partitioned our state set, we form our equivalence classes with the smallest state being the representative, i.e., the mother node of an ordered tree with all the daughters being equivalent states. The only exception is the sink state where not the smallest, but the atom sink is the representative. This representation allows a better access of the representative and the current state.

The second step of forming the quotient automaton is achieved by traversing the transition tree and putting in the relevant representatives into the transitions headed by a representative and removing all the other transitions headed by equivalent states.

  % equiv_states(+EquivPairs,+StateList,+Transitions,-EquivStates)
  equiv_states( Pairs, States, Trans, Equivs ) :-
        equiv_states_aux(Pairs,States,Trans,Pairs,RemPairs,Diff ),
        ( Diff == [] ->
            Equivs = Pairs
        ;
            equiv_states( RemPairs, States, Trans, Equivs)
        ).

Figure 13. The equivalence loop

3.4.5. Properties of the Compiler. After this description of the compiler we want to present some of its properties. We already noted that the worst case complexity is non-elementary. But by tying all constructions to the reachability constructions we achieve a much better behaviour in the average case.

The coupling of the reachability construction and minimization means at the same time that our automata are as compact as possible. This is especially interesting in case we recognize no trees or all trees. In the first case that we recognize no trees, we have only the sink state and no final states. In this sense the compiler represents a theorem prover. If the resulting automaton is empty, the (existential closure of the) formula is not a theorem of our language. On the other hand the automaton which recognizes all trees has just one state which is initial and final at the same time. If the compilation generates such an automaton it means that the (existential closure of the) formula represents a tautology in our language. In all other cases the resulting automaton means that the (existential closure of the) formula is a theorem of our language.

An interesting open question is the connection between types of formulas and the size of the corresponding automata. In the paragraph above we noted that tautologies and contradictions have very small automata. But what about the other cases. Are there particular sets of formulas that produce small automata? One advantage of specifying syntax via logic is the conciseness of the representations. When we switch with our representation to automata, under which conditions do we lose this property? And since we use Prolog as our implementation language, what happens due to our representation of these automata in (a special form of) logic?

Last let us note that the automata, after they have been generated, specify a very efficient means of processing natural language since they are deterministic finite state devices. The ideal scenario allows the specification of a grammar along the lines of Roger’s formalization of most of Rizzi’s Relativized Minimality (Rizzi 1990). Then we can compile this grammar in an offline process into a tree automaton. If this works – we come back to the problems involved in section 3.5 – we can use the automaton as a very efficient means to process further queries relative to the grammar. The obvious task to address here is parsing. Recognition of a given tree is trivial since this just means running the automaton on a specific tree. For recognition of a string, (which amounts to parsing in this setting) we have to conjoin our grammar with the formula representing the input string. In case it is a theorem we get a new non-empty tree automaton in return. Running this tree automaton as a generator then results in assignment trees which allow the construction of a parse analysis.^{10} So in fact, we can use these automata not just as recognizers but as parsers as well.

3.5. Summary. In this paper we presented MoSeL, a compiler from monadic second order logic on trees to tree automata. We hope that it helps to use L_{K,P}^{2} for natural language processing. We can compile (parts of) our grammar offline into a deterministic finite state tree automaton which can be used efficiently as a recognition and generation device. And in fact, the compiler does theorem proving already. Due to the incorporation of reachability and minimization, any generated automaton which does have a final state represents a theorem of our language.

Despite its apparently staggering complexity bound, we think that its average behavior and the fact that we want to use it offline, make it into an interesting tool for natural language processing. But we are well aware that so far MoSeL only represents a prototype. It was designed mainly with a focus on correctness, although it does allow the specification of predicates and libraries. But it does not incorporate all possible optimizations. For example, looking at the implementation of MONA, we do not fully incorporate their ideas of using BDDs and their corresponding operations.

10We have to be a bit careful since the number of resulting assignment trees can be infinite. Remember that we did not define a unique minimal tree, but the closure under our relation. In generation we have to employ something like iterative deepening on the \underline{0} labeled transitions, so that we generate first the trees without \underline{0} labeled nodes, then the trees with just one \underline{0} labeled node, etc. We then can stop at any point in the generation.

Apart from these technical points there is a real issue left. Since our main application is to be sought in the realm of natural language processing, we have to be able to cope with alphabets of large size. Considering that each lexical entry and each feature in a formalization has to be represented by a new free variable, we face for a grammar of realistic coverage real problems since – looking at the way our alphabet is coded – this means that we have to consider too many possibilities to be able to get automata of any reasonable size. Even the data-structure proposed for MONA faces pointers of an immense depth. It is an open question whether these large amounts of free variables can be handled efficiently. In the following, we will point out some possible solutions to this problem.

One direction for optimization seems to lie in using generic automata throughout all the constructions. This depends on whether an appropriate data structure for the projections on the transitions can be found and implemented.

A different solution – and in fact the third use of MoSeL – consists in embedding it as a constraint solver into a constraint logic programming scheme. In Morawietz (1997) we describe our first attempt using a standard Höhfeld and Smolka scheme (Höhfeld and Smolka 1988). Thus it becomes possible to consider one lexical entry at a time. The idea is that we try to split the work into components in such a way that our constraint logic programming component handles the control structure of the compilation process by parameterizing it to the particular input.

The embedding into an constraint logic programming scheme suggests that we might be able to handle the problem caused by features and lexical entries by employing a different constraint solver when dealing with these. We would have a hierarchy of constraint solvers depending on the level of the problem we are working on. Outermost would be the clp interpreter, followed by MoSeL which in turn would use another solver in the appropriate places. This corresponds roughly to a layering of logics discussed for example in Blackburn and de Rijke (1994). But the exploration of this is beyond the scope of the paper and left for further research.

Appendix A. Additional Examples

A.1. Some Example Constructions. Given the nature of the decidability proof, we observe immediately that we can extend our language with any relation symbols which can be defined using our tree automata.

For example, we can define the subset relation directly by the following automaton construction. Here is the automaton definition for 𝔞𝔲𝔱(X_{1} ⊆ X_{2}).

𝔞𝔲𝔱(X_{1} ⊆ X_{2}) = 𝔄 = ({a_{0}, a_{1}}, α, {a_{0}})
α(λ) = a_{0}
α(σ)(a_{0}, a_{0}) = a_{0}, for σ ∈ \{\underline{0}\underline{0}, \underline{0}\underline{1}, \underline{1}\underline{1}\}

everything else maps to a_{1}

We consider now, in light of this definition, the automata for the following simple formulas.

(∃X_{2}) ¬X_{1} ⊆ X_{2} (30)

¬( ∃X_{2}) X_{1} ⊆ X_{2} (31)

¬( ∃X_{2}) ¬X_{1} ⊆ X_{2} (32)

This example may help to elucidate how our automata constructions take care of the rather tricky problem of scope.

Tackling the automaton for (30) first, we apply the complementation construction to 𝔄 and then we apply the projection construction to it, removing the second position of the node labels. The complement construction simply inverts the final states. So the relation defined by ¬X_{1} ⊆ X_{2} is just

T (({a_{0}, a_{1}}, α, {a_{1}})).

Since all the leaf nodes are assigned state a_{0}, the only way to get into state a_{1} is to encounter somewhere in the tree a node labeled \underline{1}\underline{0}, that is, which is assigned to the denotation of X_{1} but not to X_{2}. Note that this means that some node must be labeled with a \underline{1} in the first position. This is what we would expect: since the empty set is a subset of every set, it cannot be the first term in any tuple in the not-subset relation.

We now construct the projection automaton. Transitions on \underline{1}\underline{0} and \underline{1}\underline{1} now collapse together, as do transitions on \underline{0}\underline{0} and \underline{0}\underline{1} (which were never in fact distinct).

𝔄_{2} = ({a_{0}, a_{1}}, β, {a_{1}})

β(λ) = {a_{0}}
β(\underline{0})(a_{0}, a_{0}) = \{a_{0}\}

β(\underline{1})(a_{0}, a_{0}) = \{a_{0}, a_{1}\}

everything else maps to {a_{1}}

The formula defines the set of sets which are not subsets of everything, that is, the set of sets distinct from the empty set. The implementation is correct, then, just in case only trees which have some \underline{1}-labeled nodes in them are accepted: these are the representatives of the non-empty sets. This is obviously the case: the only way into state a_{1} is via a node labeled \underline{1}. The trivial tree λ is assigned a_{0}, and so, by a simple induction, is every tree labeled only with \underline{0}’s. Any tree with at least one \underline{1} in it obviously defines a non-empty set of nodes, and, correspondingly, there is an accepting run of 𝔄_{2} for every such tree.

According to our account of quantification we should now determinize this automaton, but since we are done and, in particular, we are not under the scope of a negation, we need not construct this further automaton which is, after all, equivalent. This step is needed in the next construction, however, and we discuss it there.

We now turn to the second formula, (31). Here we first construct the projection, and then we must complement it; but we cannot complement it until we have first determinized it. The projection automaton has the same underlying algebra as 𝔄_{2}; only the final states are different.

𝔄_{3} = ({a_{0}, a_{1}}, β, {a_{0}})

The formula which we have just implemented, (∃X_{2}) X_{1} ⊆ X_{2}, defines the set of all (finite) sets of nodes (under the weak interpretation of the theory), and it is clear that the automaton does in fact implement this behavior. First, by the reasoning above, any tree which represents the empty set will have a run assigning a_{0} to the tree. The rest of the trees in T_{Σ^{1}} are in the set by the following reasoning. Every node labeled \underline{1} and dominating only nodes labeled \underline{0} or λ can be assigned a_{0}. This furnishes the base of a simple inductive argument which shows that we can always find a run assigning a_{0} to any tree.

When we apply the complementation construction to this automaton, then, we had better derive an automaton which recognizes no trees at all. And this is in fact what happens. First, the determinized automaton can be described compactly by the following rules:

𝔄_{4} = ({∅, {a_{0}}, {a_{1}}, {a_{0}, a_{1}}}, β̂, {{a_{0}}, {a_{0}, a_{1}}})
β̂(λ) = {a_{0}}

β̂(\underline{0})(Q_{1}, Q_{2}) = Q ⟺
(a_{1} ∈ Q_{1} ∨ a_{1} ∈ Q_{2} ⇒ a_{1} ∈ Q) ∧
(a_{0} ∈ Q_{1} ∧ a_{0} ∈ Q_{2} ⇒ a_{0} ∈ Q)
β̂(\underline{1})(Q_{1}, Q_{2}) = Q ⟺
(a_{1} ∈ Q) ∧
(a_{0} ∈ Q_{1} ∧ a_{0} ∈ Q_{2} ⇒ a_{0} ∈ Q)

The final states of the complement automaton are those states of 𝔄_{4} which do not have a_{0} as a member, that is,

{∅, {a_{1}}}

Clearly, the trivial tree λ is not accepted by this automaton. The tree \underline{0}λλ is assigned state \{a_{0}\}, so it is not in the set, and the tree \underline{1}λλ is assigned {a_{0}, a_{1}}, so it too is not in the set. It should be clear that there is now no way to get a_{0} out of the set assigned by the transition function, for any tree. So indeed, the language of this automaton is empty as desired.

We turn now to our final formula, (32). Note that this is equivalent to the universally quantified formula

(∀X_{2}) X_{1} ⊆ X_{2}

This formula defines the set containing only the empty set, so the automaton we construct ought to accept only trees representing the empty set, that is, the trivial tree λ and any tree containing only \underline{0}-labeled interior nodes.

We have already constructed 𝔞𝔲𝔱((∃X_{2}) ¬X_{1} ⊆ X_{2}), so all we have to do is negate it. But of course to do this we must first determinize it. Once again, we have already done the work: the desired transition function is just β̂. But now the final states are just those states which do not contain a_{1}. Clearly the tree λ is accepted. Then it is easy to show that every tree labeled only with \underline{0} will have a_{0} in the state it is assigned. Finally, any tree with at least one node labeled \underline{1} will be assigned a state containing a_{1}, so it will be rejected. So indeed these constructions seem to work as we would hope.

A.2. More Detailed Example Constructions. We consider here a rather more involved example. In (33) we see the axiom of rootedness.

(∃x_{1})(∀x_{2})[x_{1} ⊲^{∗} x_{2}] (33)

\underline{0}\underline{0} \underline{0}\underline{1} \underline{1}\underline{0} \underline{1}\underline{1}
a_{0}, a_{0} a_{0} a_{1} ⊥ b_{1}
a_{1} a_{1} ⊥ a_{2} ⊥
a_{2} a_{2} ⊥ ⊥ ⊥
b_{1} b_{1} ⊥ ⊥ ⊥
a_{1}, a_{0} a_{1} ⊥ a_{2} ⊥
a_{2}, a_{0} a_{2} ⊥ ⊥ ⊥
b_{1}, a_{0} b_{1} ⊥ ⊥ ⊥

Everything else goes to ⊥ Table 2. Transition table for α.

Converting individual variables to singleton set variables, we get (34).

(34) (∃X_{1})[Sing(X_{1}) ∧ (∀X_{2})[Sing(X_{2}) ⇒ X_{1} ⊲^{∗} X_{2}]] Finally, unpacking our various abbreviations, we get (35).

(35) (∃X_{1})[Sing(X_{1}) ∧ ¬(∃X_{2})[Sing(X_{2}) ∧ ¬(X_{1} ⊲^{+} X_{2} ∨ X_{1} ≈ X_{2})]] Let us suppose that we have automata 𝔄 and 𝔅 corresponding to the

⊲^{+} and ≈ formulas. We construct the automaton for the disjunction by the (disjoint) union operation, giving us the following combined automaton.^{11}

𝔄 = (A, α, A^{F})
A = {a_{0}, a_{1}, a_{2}, b_{1}, ⊥}
A^{F} = {a_{2}, b_{1}}
α(λ) = a_{0}

The transition function α is displayed in Table 2.

This automaton is deterministic, so the automaton for

¬(X_{1} ⊲^{+} X_{2} ∨ X_{1} ≈ X_{2})

is got by simply inverting the final states: ∼ A_{⊲^{∗}}^{F} = {a_{0}, a_{1}, ⊥} (36)

11Note that the initial states of the two automata are equivalent, as are the sink states, and we have collapsed them into a_{0} and ⊥, respectively. The transitions are now really given as a table. If the left column of the state pair is empty, it is supposed to be filled with the previous left state, e.g., in the transition Table 2 a_{0}.

The cross product automaton which we get from the conjunction

Sing(X_{2}) ∧ ¬(X_{1} ⊲^{+} X_{2} ∨ X_{1} ≈ X_{2})

contains a large number of useless states. This is because 𝔄_{⊲^{+}} has a certain amount of counting behavior built into it; in particular, it makes some definite response to each non-zero label. So, in particular, it makes no sense for the cross-product automaton to pretend that it can be in a state in which one of its component automata has responded to the presence of a label \underline{0}\underline{1} while the other has not. So, assuming that 𝔄_{Sing} is defined as follows (with the transition table as given in (11) on page 15),

𝔄_{Sing} = ({0, 1, ⊥}, β, {1})

we get a combined automaton like the following.

𝔄_{2} = (A_{2}, α_{2}, A_{2}^{F})
A_{2} = {(0, a_{0}), (1, a_{1}), (1, a_{2}), (1, b_{1}), (1, ⊥), (⊥, ⊥)}
A_{2}^{F} = {(1, a_{1}), (1, ⊥)}
α_{2}(λ) = (0, a_{0})

with the transitions as in Table 3.

We now construct the “raw” projected automaton, corresponding to

(∃X_{2})[Sing(X_{2}) ∧ ¬(X_{1} ⊲^{+} X_{2} ∨ X_{1} ≈ X_{2})]

This is very easy to construct: its state set A_{3} = A_{2}, and its final states are also the same: A_{3}^{F} = A_{2}^{F}. Its transition table can be got very simply from the table for α_{2} by collapsing the \underline{0}\underline{0} and \underline{0}\underline{1} columns into a \underline{0} column and by collapsing the \underline{1}\underline{0} and \underline{1}\underline{1} columns into a 1 column. We derive the following transitions, see Table 4.

After truncation, we derive the initial states.

{(0, a_{0}), (1, a_{1}), (⊥, ⊥)}

We are now ready to apply the subset construction. Before we do so, however, it is very helpful to rename our states. The state-names of the subset automaton will be large enough as is! Accordingly, we apply the following mapping.

(0, a_{0}) ↦ c_{0}  (0, ⊥) ↦ d_{0}
(1, a_{1}) ↦ c_{1}  (1, ⊥) ↦ d_{1}
(1, a_{2}) ↦ c_{2}  (⊥, ⊥) ↦ d_{2}
(1, b_{1}) ↦ c_{3}

\underline{0}\underline{0}  \underline{0}\underline{1}  \underline{1}\underline{0}  \underline{1}\underline{1}
(0, a_{0}), (0, a_{0}) (0, a_{0}) (1, a_{1}) (0, ⊥) (1, b_{1})
(0, ⊥) (0, ⊥) (1, ⊥) (0, ⊥) (1, ⊥)
(1, a_{1}) (1, a_{1}) (⊥, ⊥) (1, a_{2}) (⊥, ⊥)
(1, a_{2}) (1, a_{2}) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, b_{1}) (1, b_{1}) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, ⊥) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(0, ⊥), (0, a_{0}) (0, ⊥) (1, ⊥) (0, ⊥) (1, ⊥)
(0, ⊥) (0, ⊥) (1, ⊥) (0, ⊥) (1, ⊥)
(1, a_{1}) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, a_{2}) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, b_{1}) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, ⊥) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, a_{1}), (0, a_{0}) (1, a_{1}) (⊥, ⊥) (1, a_{2}) (⊥, ⊥)
(0, ⊥) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, a_{2}), (0, a_{0}) (1, a_{2}) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(0, ⊥) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, b_{1}), (0, a_{0}) (1, b_{1}) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(0, ⊥) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(1, ⊥), (0, a_{0}) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)
(0, ⊥) (1, ⊥) (⊥, ⊥) (1, ⊥) (⊥, ⊥)

Everything else goes to (⊥, ⊥)

Table 3. Transition table for α_{2}.

Our automaton now looks as follows.

𝔄_{4} = (A_{4}, α_{4}, A_{4}^{F})

A_{4} = {c_{0}, c_{1}, c_{2}, c_{3}, d_{0}, d_{1}, d_{2}}

A_{4}^{F} = {c_{1}, d_{1}}

The transition function α_{4} is described in Table 5.

There are 2^{7} states in the “raw” subset automaton. Fortunately, almost all of these sates are not reachable from the initial state. Considering only the reachable states, we cut things down to 4 states! They are the following.

{{c_{0}, c_{1}, d_{2}}, {c_{2}, c_{3}, d_{0}, d_{2}}, {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}}, {d_{0}, d_{1}, d_{2}}}

\underline{0}  \underline{1}
(0, a_{0}), (0, a_{0}) {(0, a_{0}), (1, a_{1})} {(0, ⊥), (1, b_{1})}
(0, ⊥) {(0, ⊥), (1, ⊥)} {(0, ⊥), (1, ⊥)}
(1, a_{1}) {(1, a_{1}), (⊥, ⊥)} {(1, a_{2}), (⊥, ⊥)}
(1, a_{2}) {(1, a_{2}), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, b_{1}) {(1, b_{1}), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, ⊥) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(0, ⊥), (0, a_{0}) {(0, ⊥), (1, ⊥)} {(0, ⊥), (1, ⊥)}
(0, ⊥) {(0, ⊥), (1, ⊥)} {(0, ⊥), (1, ⊥)}
(1, a_{1}) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, a_{2}) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, b_{1}) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, ⊥) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, a_{1}), (0, a_{0}) {(1, a_{1}), (⊥, ⊥)} {(1, a_{2}), (⊥, ⊥)}
(0, ⊥) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, a_{2}), (0, a_{0}) {(1, a_{2}), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(0, ⊥) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, b_{1}), (0, a_{0}) {(1, b_{1}), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(0, ⊥) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(1, ⊥), (0, a_{0}) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}
(0, ⊥) {(1, ⊥), (⊥, ⊥)} {(1, ⊥), (⊥, ⊥)}

Everything else goes to {(⊥, ⊥)}

Table 4. Transition table for α_{3}.

The initial state is {c_{0}, c_{1}, d_{2}}, and the final states are all the states containing either c_{1} or d_{1}, that is,

{{c_{0}, c_{1}, d_{2}}, {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}}, {d_{0}, d_{1}, d_{2}}}

The transition table is given as the table for α_{5}, in Table 6.

Now we can complement this automaton to give us the automaton for the formula

¬(∃X_{2})[Sing(X_{2}) ∧ ¬(X_{1} ⊲^{+} X_{2} ∨ X_{1} ≈ X_{2})]

All we have to do is invert the final states, giving us

∼ A_{5}^{F} = {{c_{2}, c_{3}, d_{0}, d_{2}}}

¿From Table 6 we see immediately that the final state is only reachable from the initial state {c_{0}, c_{1}, d_{2}}, So states {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}} and {d_{0}, d_{1}, d_{2}} are both sink states of this automaton. It should be clear

\underline{0}  \underline{1}
c_{0}, c_{0} {c_{0}, c_{1}} {d_{0}, c_{3}}
d_{0} {d_{0}, d_{1}} {d_{0}, d_{1}}
c_{1} {c_{1}, d_{2}} {c_{2}, d_{2}}
c_{2} {c_{2}, d_{2}} {d_{1}, d_{2}}
c_{3} {c_{3}, d_{2}} {d_{1}, d_{2}}
d_{1} {d_{1}, d_{2}} {d_{1}, d_{2}}
d_{0}, c_{0} {d_{0}, d_{1}} {d_{0}, d_{1}}
d_{0} {d_{0}, d_{1}} {d_{0}, d_{1}}
c_{1} {d_{1}, d_{2}} {d_{1}, d_{2}}
c_{2} {d_{1}, d_{2}} {d_{1}, d_{2}}
c_{3} {d_{1}, d_{2}} {d_{1}, d_{2}}
d_{1} {d_{1}, d_{2}} {d_{1}, d_{2}}
c_{1}, c_{0} {c_{1}, d_{2}} {c_{2}, d_{2}}
d_{0} {d_{1}, d_{2}} {d_{1}, d_{2}}
c_{2}, c_{0} {c_{2}, d_{2}} {d_{1}, d_{2}}
d_{0} {d_{1}, d_{2}} {d_{1}, d_{2}}
c_{3}, c_{0} {c_{3}, d_{2}} {d_{1}, d_{2}}
d_{0} {d_{1}, d_{2}} {d_{1}, d_{2}}
d_{1}, c_{0} {d_{1}, d_{2}} {d_{1}, d_{2}}
d_{0} {d_{1}, d_{2}} {d_{1}, d_{2}}

Everything else goes to d_{2} Table 5. Transition table for α_{4}.

\underline{0}  \underline{1}
{c_{0}, c_{1}, d_{2}}, {c_{0}, c_{1}, d_{2}} {c_{0}, c_{1}, d_{2}} {c_{2}, c_{3}, d_{0}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{2}}  {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}} {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{1}, d_{2}} {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}} {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{2}}, {c_{0}, c_{1}, d_{2}}  {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}} {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{2}}  {d_{0}, d_{1}, d_{2}}  {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{1}, d_{2}}  {d_{0}, d_{1}, d_{2}}  {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{1}, d_{2}}, {c_{0}, c_{1}, d_{2}}  {c_{2}, c_{3}, d_{0}, d_{1}, d_{2}} {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{2}}  {d_{0}, d_{1}, d_{2}}  {d_{0}, d_{1}, d_{2}}
{c_{2}, c_{3}, d_{0}, d_{1}, d_{2}}  {d_{0}, d_{1}, d_{2}}  {d_{0}, d_{1}, d_{2}}

Everything else goes to {d_{0}, d_{1}, d_{2}} Table 6. Transition table for α_{5}.

𝔄 = (A, α, A_{F})
A = {∅, {a_{0}}, {a_{s}}, {a_{0}, a_{s}}}
A_{F} = {∅, {a_{s}}}
α(λ) = {a_{0}}

\begin{matrix}α(\underline{0})(∅, ∅) = ∅ & α(\underline{1})(∅, ∅) = \{a_{s}\} \\ α(\underline{0})(∅, \{a_{0}\}) = ∅ & α(\underline{1})(∅, \{a_{0}\}) = \{a_{s}\} \\ α(\underline{0})(∅, \{a_{s}\}) = \{a_{s}\} & α(\underline{1})(∅, \{a_{s}\}) = \{a_{s}\} \\ α(\underline{0})(∅, \{a_{0}, a_{s}\}) = \{a_{s}\} & α(\underline{1})(∅, \{a_{0}, a_{s}\}) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}\}, ∅) = ∅ & α(\underline{1})(\{a_{0}\}, ∅) = \{a_{s}\} \\ α(\underline{0})(\{a_{s}\}, ∅) = \{a_{s}\} & α(\underline{1})(\{a_{s}\}, ∅) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}, a_{s}\}, ∅) = \{a_{s}\} & α(\underline{1})(\{a_{0}, a_{s}\}, ∅) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}\}, \{a_{0}\}) = \{a_{0}\} & α(\underline{1})(\{a_{0}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} \\ α(\underline{0})(\{a_{0}\}, \{a_{s}\}) = \{a_{s}\} & α(\underline{1})(\{a_{0}\}, \{a_{s}\}) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} & α(\underline{1})(\{a_{0}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} \\ α(\underline{0})(\{a_{s}\}, \{a_{0}\}) = \{a_{s}\} & α(\underline{1})(\{a_{s}\}, \{a_{0}\}) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}, a_{s}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} & α(\underline{1})(\{a_{0}, a_{s}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} \\ α(\underline{0})(\{a_{s}\}, \{a_{s}\}) = \{a_{s}\} & α(\underline{1})(\{a_{s}\}, \{a_{s}\}) = \{a_{s}\} \\ α(\underline{0})(\{a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{s}\} & α(\underline{1})(\{a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}, a_{s}\}, \{a_{s}\}) = \{a_{s}\} & α(\underline{1})(\{a_{0}, a_{s}\}, \{a_{s}\}) = \{a_{s}\} \\ α(\underline{0})(\{a_{0}, a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} & α(\underline{1})(\{a_{0}, a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} \end{matrix}

Figure 14. A determinized but unminimized automaton.

that this automaton does indeed only recognize sets X_{1} which contain only the root. Since the root is unique in any case, the extra call to Sing is superfluous here. The set of singleton sets containing only the root is nonempty, and so the original sentence

(∃x_{1})(∀x_{2}) x_{1} ⊲^{∗} x_{2}

is determined to be true, as we would have hoped!

A.3. Some Minimization Examples.

A.3.1. ¬(∃X_{2})[X_{1} ⊆ X_{2}]. Consider the determinized automaton 𝔄 for the formula ¬(∃X_{2}) X_{1} ⊆ X_{2}, given in Figure 14. If we limit automaton 𝔄 to the reachable states, we get the automaton 𝔄′ exhibited in Figure

𝔄′ = (A′, α′, A′_{F})
A′ = {{a_{0}}, {a_{0}, a_{s}}}
A′_{F} = ∅
α′(λ) = {a_{0}}

\begin{matrix}α′(\underline{0})(\{a_{0}\}, \{a_{0}\}) = \{a_{0}\} & α′(\underline{1})(\{a_{0}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} \\ α′(\underline{0})(\{a_{0}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} & α′(\underline{1})(\{a_{0}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} \\ α′(\underline{0})(\{a_{0}, a_{s}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} & α′(\underline{1})(\{a_{0}, a_{s}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} \\ α′(\underline{0})(\{a_{0}, a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} & α′(\underline{1})(\{a_{0}, a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} \end{matrix}

Figure 15. Restriction to reachable states.

The congruences are very simple (f ∈ ET (𝔄′)):

{a_{0}} ≡_{0} {a_{0}, a_{s}} (37)

since both are final.

{a_{0}} ≡_{1} {a_{0}, a_{s}} (38)

since (37) holds and f({a_{0}}) and f({a_{0}, a_{s}}) are in ≡_{0} .

So we cannot distinguish {a_{0}} and {a_{0}, a_{s}}, and the resulting automaton is 𝔄′′, see Figure 16.

𝔄′′ = (A′′, α′′, A′′_{F})
A′′ = {[{a_{0}}]}
A′′_{F} = ∅
α′′(λ) = [{a_{0}}]
α′′(\{\underline{0}, \underline{1}\})([\{a_{0}\}], [\{a_{0}\}]) = [\{a_{0}\}]

Figure 16. Final output of minimization.

This automaton really reflects the intuitions about a minimal automaton which recognizes the empty language. The only state we need is the sink state and we stay in it, no matter what happens. If we complement it, the only state becomes final and everything is recognized.

A.3.2. ¬(∃X_{2}) [¬X_{1} ⊆ X_{2}]. Now we consider the same nucleus under universal quantification. Letting 𝔅 be the automaton for

¬(∃X_{2}) [¬X_{1} ⊆ X_{2}]

we have

𝔅 = (B, β, B_{F})
B = {∅, {a_{0}}, {a_{s}}, {a_{0}, a_{s}}}
B_{F} = {∅, {a_{0}}}

The full transition table is identical to the one for the automaton in example (A.3.1).

The same states are reachable, i.e., 𝔅′ looks as in Figure 17.

𝔅′ = (B′, β′, B′_{F})
B′ = {{a_{0}}, {a_{0}, a_{s}}}
B′_{F} = {{a_{0}}}
β′(λ) = {a_{0}}

\begin{matrix}β′(\underline{0})(\{a_{0}\}, \{a_{0}\}) = \{a_{0}\} & β′(\underline{1})(\{a_{0}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} \\ β′(\underline{0})(\{a_{0}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} & β′(\underline{1})(\{a_{0}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} \\ β′(\underline{0})(\{a_{0}, a_{s}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} & β′(\underline{1})(\{a_{0}, a_{s}\}, \{a_{0}\}) = \{a_{0}, a_{s}\} \\ β′(\underline{0})(\{a_{0}, a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} & β′(\underline{1})(\{a_{0}, a_{s}\}, \{a_{0}, a_{s}\}) = \{a_{0}, a_{s}\} \end{matrix}

Figure 17. Automaton 𝔅 restricted to its reachable states.

Since {a_{0}} is final, but {a_{0}, a_{s}} is not, we cannot refine this automaton any further. Again the resulting automaton reflects the intuition that the only set which is a subset of every other set is the empty set. This is achieved by going into the sink state \{a_{0}, a_{s}\} as soon as one symbol \underline{1} is read.

References

Backofen, R., Rogers, J. and Vijay-Shanker, K. (1995). A first-order axiomatization of the theory of finite trees, Journal of Logic, Language, and Information 4: 5–39.

Biehl, M., Klarlund, N. and Rauhe, T. (1996). Algorithms for guided tree automata, Proc. WIA ’96, LNCS, Springer-Verlag.

Blackburn, P. and de Rijke, M. (1994). Zooming in, zooming out, CLAUS

report 48, University of the Saarland. Büchi, J. R. (1960). Weak second-order arithmetic and finite automata,

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

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

of Computer and System Sciences 4: 406–451. Gécseg, F. and Steinby, M. (1984). Tree Automata, Akadémiai Kiadó,

Budapest. 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. Morawietz, F. (1997). Monadic second order logic, tree automata and con-

straint logic programming, SFB 340-Report 86, University of Tübingen. O’Keefe, R. (1990). The Craft of Prolog, MIT Press, Cambridge, Mass. Rabin, M. O. (1969). Decidability of second-order theories and automata

on infinite trees, Transactions of the American Mathematical Society 141: 1–35.

Rabin, M. O. (1970). Weakly definable relations and special automata, in Y. Bar-Hillel (ed.), Mathematical Logic and Foundations of Set Theory, North-Holland, Amsterdam, pp. 1–23.

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.

SIC (1995). SICStus Prolog User’s Manual, release 3 # 2 edn. 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.

Ullman, J. D. (1988). Principles of Database and Knowledge-base systems, Vol. 1, Computer Science Press.

Seminar für Sprachwissenschaft, SFB 340, Projekt A8, Universität Tübingen, Wilhelmstrasse 113, D-72074 Tübingen, Germany

E-mail address: {frank,cornell}@sfs.nphil.uni-tuebingen.de