LARA

Homework 12, Due May 21

Problem 1

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

Describe the set of all binary relations $r^s_F$ definable through singleton sets

\begin{equation*}
   r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \}
\end{equation*}

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

\begin{equation*}
   r^p_F = \{ (p,q) \mid G(p,q) \}
\end{equation*}

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

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

\begin{equation*}
    \forall x,y,z. (P(x,y) \rightarrow Q(y,z))
\end{equation*}

holds, and, if it holds, finds an interpolant for $P(x,y)$ and $Q(y,z)$.