tailieunhanh - Báo cáo khoa học: "Representing Constraints with Automata"

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 second order (MSO) logic are represented by tree a u t o m a t a recognizing the assignments which make the formulas true. We show that this allows an efficient representation of knowledge about the content of constraints which can be used as a practical tool for grammatical theory verification. We achieve this by using the intertranslatability of formulae of MSO logic and tree a u t o m a t a. | Representing Constraints with Automata Frank Morawietz and Tom Cornell Seminar fur Sprachwissenschaft Universităt Tubingen Wilhelmstr. 113 72074 Tubingen Germany frank cornell @ 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 second 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 constraints 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 interest in computational linguistics in both model theoretic syntax and finite state techniques. In this paper 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 applications we only need to quantify over finite sets so the weaker theory is enough and the techniques cor respondingly The decidability proof works by showing a correspondence between formulas in the language of WS2S and tree automata developed in such a way that the formula is satisfiable iff the set of trees .