# Differences

This shows you the differences between two versions of the page.

 sav08:homework12 [2008/05/15 10:08]vkuncak sav08:homework12 [2008/05/15 10:24]vkuncak Both sides previous revision Previous revision 2008/05/15 10:24 vkuncak 2008/05/15 10:23 vkuncak 2008/05/15 10:08 vkuncak 2008/05/15 10:06 vkuncak 2008/05/15 10:05 vkuncak 2008/05/14 20:08 vkuncak 2008/05/14 20:03 vkuncak 2008/05/14 19:59 vkuncak 2008/05/14 19:59 vkuncak 2008/05/14 19:58 vkuncak created Next revision Previous revision 2008/05/15 10:24 vkuncak 2008/05/15 10:23 vkuncak 2008/05/15 10:08 vkuncak 2008/05/15 10:06 vkuncak 2008/05/15 10:05 vkuncak 2008/05/14 20:08 vkuncak 2008/05/14 20:03 vkuncak 2008/05/14 19:59 vkuncak 2008/05/14 19:59 vkuncak 2008/05/14 19:58 vkuncak created Line 4: Line 4: Write a regular expression in alphabet $\{x,y,z\} \to \{0,1\}$ denoting relation $z = x + y$ using [[:Regular expressions for automata with parallel inputs]]. ​ Try to make your regular expression as concise and understandable as possible. Write a regular expression in alphabet $\{x,y,z\} \to \{0,1\}$ denoting relation $z = x + y$ using [[:Regular expressions for automata with parallel inputs]]. ​ Try to make your regular expression as concise and understandable as possible. + ===== Problem 2 ===== ===== Problem 2 ===== - In [[Quantifier elimination definition]] we noted that if the validity ​of first-order formulas in some theory is decidable, then we can extend the language of formulas so that we have quantifier elimination. ​ Previously we also observed that quantifier elimination implies the existence of interpolants (see the definition of [[interpolation for propositional logic]] as well as the [[Calculus of Computation Textbook]]). ​ We next apply these observations to weak monadic second-order logic over strings described in [[Lecture23]]. + Describe ​the set of all binary relations ​$r^s_F$ definable through singleton sets - + - Extend the language of monadic second-order logic over strings with new predicate symbols and describe an algorithm that, given formulas ​$P(x,y)$ and $Q(y,z)$ in this extension (where $x$,$y$,$z$ are $n$-tuples of set variables) checks whether + $\[ - ​\forall x,​y,​z. ​(P(x,y) \rightarrow Q(y,z)) + r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \}$ \] - holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$. + where $F$ are formulas of WS1S.  How does this set of $r^s_F$ compare to the set of all binary relations definable in Presburger arithmetic + $+ r^p_F = \{ (p,q) \mid G(p,q) \} +$ + where $G$ is a Presburger arithmetic formula.  Are the set of all $r^s_F$ and set of all $r^p_F$ equal, is one strict subset of the other, or are they incomparable?​ ===== Optional Problem 3 ===== ===== Optional Problem 3 ===== - Describe ​the set of all binary relations ​$r^s_F$ definable through singleton sets + In [[Quantifier elimination definition]] we noted that if the validity ​of first-order formulas in some theory is decidable, then we can extend the language of formulas so that we have quantifier elimination. ​ Previously we also observed that quantifier elimination implies the existence of interpolants (see the definition of [[interpolation for propositional logic]] as well as the [[Calculus of Computation Textbook]]). ​ We next apply these observations to weak monadic second-order logic over strings described in [[Lecture23]]. + + Extend the language of monadic second-order logic over strings with new predicate symbols and describe an algorithm that, given formulas ​$P(x,y)$ and $Q(y,z)$ in this extension (where $x$,$y$,$z$ are $n$-tuples of set variables) checks whether $\[ - r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \} + ​\forall x,​y,​z. ​(P(x,y) \rightarrow Q(y,z))$ \] - where $F$ are formulas of WS1S.  How does this set compare to the set of all binary relations definable in Presburger arithmetic? + holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$.