Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
ws1s_expressive_power_and_quantifier_elimination [2007/06/29 11:24] vaibhav.rajan |
ws1s_expressive_power_and_quantifier_elimination [2007/06/29 17:12] vaibhav.rajan |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | * why the problem is interesting | + | Introduction: |
| + | We know that Weak Monadic Second-order theory of 1 Successor (WS1S) is decidable through automata, that is, the set of satisfying interpretations of a subformula is represented by a finite-state automaton [Buc60b, Elg61]. The decision procedures (using the automata technique) have been implemented efficiently (for WS1S with certain restrictions) in MONA. | ||
| + | The main problem with this approach is exponential blow-up in the states of the automaton due to nested quantifiers [Kla01]. | ||
| + | We were interested in finding another way of deciding WS1S without using the automata. We began by investigating whether we can characterize relations in WS1S in a way that helps us eliminate quantifiers. Since we couldn't get any substantial results, we began looking at a subset of WS1S. This paper describes the key results that we obtained. | ||
| - | deciding WS1S - done through automata construction (mona)\\ | + | Conclusions and Future Directions: |
| - | main problem: quantifier elimination\\ | + | In the course of our mini-project we proved an interesting result about the lengths of words of a regular language. We used this result to characterize relations in the language $L^R$. We hope that this is a step in the direction of our original aim: characterizing relations in WS1S. |
| - | is there another way of QE? - can we characterize relations in WS1S in some other way?\\ | + | |
| - | WS1S too big: look at a smaller subset of the language\\ | + | |
| - | our L: characterize unary relations, binary relations,...n-ary\\ | + | |
| - | * what was done before | ||
| - | p-recognizability | ||
| - | * what the main idea is | ||
| - | |||
| - | * what you did (precise description) | ||
| - | |||
| - | * the most surprising/interesting things you found | ||
| - | |||
| - | * limitations | ||
| - | |||
| - | * future directions | ||
| - | |||
| - | look at other subsets of WS1S, whole of WS1S | ||
| **START** | **START** | ||
| Line 176: | Line 163: | ||
| - | **The binary case for the W-problem** Consider a binary relation $R(x,y)$ in $L_R$ and the corresponding formula $F(x,y)$ with two free variables $x$ and $y$. $F(x,y)$ defines a set $Q=\{(x,y)|\ F(x,y)\}$. Elements of the set $Q$ are recognized by an automaton $A$ with parallel inputs and input alphabet $\Sigma = \{\binom{0}{0},\binom{0}{1},\binom{1}{0},\binom{1}{1}\}$. The language L of A is a subset of the regular language corresponding to $\binom{0}{0}^*\binom{1}{0}\binom{0}{0}^*\binom{0}{1}\binom{0}{0}* + \binom{0}{0}^*\binom{0}{1}\binom{0}{0}^*\binom{1}{0}\binom{0}{0}^* + \binom{0}{0}^*\binom{1}{1}\binom{0}{0}^*$. Thus the input string to the automaton is of the form $\binom{0}{0}^{k_1}\binom{1}{0}\binom{0}{0}^{k_2}\binom{0}{1}\binom{0}{0}^{k_3}$ or $\binom{0}{0}^{k_4}\binom{0}{1}\binom{0}{0}^{k_5}\binom{1}{0}\binom{0}{0}^{k_6}$ or $\binom{0}{0}^{k_7}\binom{1}{1}\binom{0}{0}^{k_8}$.\\ | + | **The binary case for the W-problem** Consider a binary relation $R(x,y)$ in $L_R$ and the corresponding formula $F(x,y)$ with two free variables $x$ and $y$. $F(x,y)$ defines a set $Q=\{(x,y)|\ F(x,y)\}$. Elements of the set $Q$ are recognized by an automaton $A$ with parallel inputs and input alphabet $\Sigma = \{\binom{0}{0},\binom{0}{1},\binom{1}{0},\binom{1}{1}\}$. The language L of A is a subset of the regular language corresponding to $\binom{0}{0}^*\binom{1}{0}\binom{0}{0}^*\binom{0}{1}\binom{0}{0}^* + \binom{0}{0}^*\binom{0}{1}\binom{0}{0}^*\binom{1}{0}\binom{0}{0}^* + \binom{0}{0}^*\binom{1}{1}\binom{0}{0}^*$. Thus the input string to the automaton is of the form $\binom{0}{0}^{k_1}\binom{1}{0}\binom{0}{0}^{k_2}\binom{0}{1}\binom{0}{0}^{k_3}$ or $\binom{0}{0}^{k_4}\binom{0}{1}\binom{0}{0}^{k_5}\binom{1}{0}\binom{0}{0}^{k_6}$ or $\binom{0}{0}^{k_7}\binom{1}{1}\binom{0}{0}^{k_8}$.\\ |
| **Claim** A pair $(x,y)$ belongs to some set $Q=\{(x,y)|\F(x,y)\}$ for some $F$ iff the sets $\{k_i\}_i$ of possible lengths of the exponents $k_i$ are ultimately periodic.\\ | **Claim** A pair $(x,y)$ belongs to some set $Q=\{(x,y)|\F(x,y)\}$ for some $F$ iff the sets $\{k_i\}_i$ of possible lengths of the exponents $k_i$ are ultimately periodic.\\ | ||
| **Proof** | **Proof** | ||
| Line 184: | Line 171: | ||
| (a)$\binom{0}{0}^{k_1}\binom{1}{0}\binom{0}{0}^{k_2}\binom{0}{1}\binom{0}{0}^{k_3}$ \\ | (a)$\binom{0}{0}^{k_1}\binom{1}{0}\binom{0}{0}^{k_2}\binom{0}{1}\binom{0}{0}^{k_3}$ \\ | ||
| (b)$\binom{0}{0}^{k_7}\binom{1}{1}\binom{0}{0}^{k_8}$\\ | (b)$\binom{0}{0}^{k_7}\binom{1}{1}\binom{0}{0}^{k_8}$\\ | ||
| - | case (a): We want to show that the sets {k_1}, {k_2} and {k_3} are ultimately periodic. Due to the little problem, it is sufficient to show that the language generated by the unary alphabet $\binom{0}{0}$: $\binom{0}{0}^{k_i}, i = 1,2,3$ is regular. | + | case (a): We want to show that the sets $\{k_1\}$, $\{k_2\}$ and $\{k_3\}$ are ultimately periodic. Due to the little problem, it is sufficient to show that the language generated by the unary alphabet $\binom{0}{0}$: $\binom{0}{0}^{k_i}, i = 1,2,3$ is regular. |
| - | We show that $\binom{0}{0}^{k_2}$ is regular by constructing an accepting automaton, $A = (\Sigma, \delta, s, f, S)$. Let $M = (\Sigma^{'}, \delta^{'}, s^{'}, f^{'}, S^{'})$ be the automaton that accepts the original input string (a). Let $q$ be the accepting run in $M$. In $q$, there exists a unique state $s$ such that $\delta^{'}(m, \binom{1}{0}) = n$ where $m$,$n$ are states in $q$. Define $s = n$. Similarly there exists $\delta^{'}(g, \binom{0}{1}) = h$. Define $f = g$. $S$ contains all the states of $S^{'}$ that are in $q$ between $s$ and $f$. And, $\delta$ is the restriction of $\delta^{'}$ to the transitions in $q$ between $s$ and $f$. $\Sigma = \{\binom{0}{0}\}$. Thus the automaton is defined unambiguously. | + | We show that $\binom{0}{0}^{k_2}$ is regular by constructing an accepting automaton, $A = (\Sigma, \delta, s, f, S)$. Let $M = (\Sigma^{'}, \delta^{'}, s^{'}, f^{'}, S^{'})$ be the automaton that accepts the original input string (a). Let $q$ be the accepting run in $M$. In $q$, there exist unique states $m$ and $n$ such that $\delta^{'}(m, \binom{1}{0}) = n$. Define $s = n$. Similarly there exist unique $g, h$ such that $\delta^{'}(g, \binom{0}{1}) = h$. Define $f = g$. $S$ contains all the states of $S^{'}$ that are in $q$ between $s$ and $f$. And, $\delta$ is the restriction of $\delta^{'}$ to the transitions in $q$ between $s$ and $f$. $\Sigma = \{\binom{0}{0}\}$. Thus the automaton is defined unambiguously. |
| We can similarly construct automata for the languages $\binom{0}{0}^{k_1}$ and $\binom{0}{0}^{k_3}$. In the former case, the start state corresponds to $s^{'}$ and the final state is the state (in $q$) from which there is a transition on consuming $\binom{1}{0}$. In the latter case, the final state corresponds to $f^{'}$ and the start state is that state in $q$ that is reached after consuming $\binom{0}{1}$. | We can similarly construct automata for the languages $\binom{0}{0}^{k_1}$ and $\binom{0}{0}^{k_3}$. In the former case, the start state corresponds to $s^{'}$ and the final state is the state (in $q$) from which there is a transition on consuming $\binom{1}{0}$. In the latter case, the final state corresponds to $f^{'}$ and the start state is that state in $q$ that is reached after consuming $\binom{0}{1}$. | ||
| - | The construction of the automata for case (c) are along the same lines. | + | The construction of the automata for case (c) is along the same lines. |
| Line 197: | Line 184: | ||
| The above reasoning can be extended to the n-ary case. The input string has n non-zero elements and n+1 expressions of the form $(\{(0...0)^{-1}\})^k$. A tuple $(x_1, x_2,...x_n)$ belongs to an n-ary relation iff the possible values of each exponent $k$ forms an ultimately periodic set. | The above reasoning can be extended to the n-ary case. The input string has n non-zero elements and n+1 expressions of the form $(\{(0...0)^{-1}\})^k$. A tuple $(x_1, x_2,...x_n)$ belongs to an n-ary relation iff the possible values of each exponent $k$ forms an ultimately periodic set. | ||
| + | References:\\ | ||
| + | [Buc60a] Julius Richard Buchi. On a decision method in restricted second-order arithmetic. In Proc. Internat. Cong. on Logic, Methodol., and Philos. of Sci. Stanford University Press, 1960.\\ | ||
| + | [Elg61] Calvin C. Elgot. Decision problems of Finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21{52, 1961.\\ | ||
| + | [Kla01] Nils Klarlund, Anders Moller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, 2001.\\ | ||