Representing Constraints with Automata

Representing Constraints with Automata Frank Morawietz and Tom Cornell Seminar fiir Sprachwissenschaft Universit£t Tiibingen Wilhelmstr. 113 72074 Tiibingen, Germany {frank, cornell}~sfs, nphil, uni-tuebingen, de Abstract In this paper we describe an approach to constraint based syntactic theories in terms of finite tree automata. The solutions to constraints expressed in weak monadic sec- ond order (MSO) logic are represented by tree automata recognizing the assignments which make the formulas true. We show that this allows an efficient representation of knowledge about the content of con- straints which can be used as a practical tool for grammatical theory verification. We achieve this by using the intertrans- latability of formulae of MSO logic and tree automata and the embedding of MSO logic into a constraint logic programming scheme. The usefulness of the approach is discussed with examples from the realm of Principles-and-Parameters based parsing. 1 Introduction In recent years there has been a continuing inter- est in computational linguistics in both model theo- retic syntax and finite state techniques. In this pa- per we attempt to bridge the gap between the two by exploiting an old result in logic, that the weak monadic second order (MSO) theory of two successor functions (WS2S) is decidable (Thatcher and Wright 1968, Doner 1970). A "weak" second order theory is one in which the set variables are allowed to range only over finite sets. There is a more powerful result available: it has been shown (Rabin 1969) that the strong monadic second order theory (variables range over infinite sets) of even countably many successor functions is decidable. However, in our linguistic ap- plications we only need to quantify over finite sets, so the weaker theory is enough, and the techniques cor- respondingly simpler3 The decidability proof works by showing a correspondence between formulas in the language of WS2S and tree automata, devel- oped in such a way that the formula is satisfiable iff the set of trees accepted by the corresponding au- tomaton is nonempty. While these results were well known, the (rather surprising) suitability of this for- malism as a constraint language for Principles and Parameters (P&P) based linguistic theories has only recently been shown by Rogers (1994). It should be pointed out immediately that the translation from formulas to automata, while effec- tive, is just about as complex as it is possible to be. In the worst case, the number of states can be given as a function of the number of variables in the input formula with a stack of exponents as tall as the number of quantifier alternations in the for- mula. However, there is a growing body of work in the computer science literature motivated by the success of the MONA decision procedure (Henriksen et al. 1995) 2 on the application of these techniques in computer science (Basin and Klarlund 1995, Kelb et al. 1997), which suggests that in practical cases the extreme explosiveness of this technique can be effectively controlled. It is one of our goals to show that this is …

Content truncated to 500 words