Differences

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

--- sav08:homework08 [2008/09/15 15:22]
vkuncak
+++ sav08:homework08 [2015/04/21 17:30] (current)
@@ Line 6: / Line 6: @@
 Consider a language $L$ that contains some terms whose values are interpreted as integers (to be concrete, the language of Presburger arithmetic, or the BAPA language).  Consider formulas interpreted over some theory $T$ that has an effective quantifier elimination algorithm $qe$.  Then show that there is an algorithm for solving optimization problems such as
-\[
+\begin{equation*}
     \max \{ t(x_1,\ldots,x_n) \mid F(x_1,\ldots,x_n) \}
-\]
+\end{equation*}
 where $t(x_1,\ldots,x_n)$ denotes a term of the language whose value is an integer, and where $F(x_1,\ldots,x_n)$ is an arbitrary formula in language $L$.  The meaning of //solution// for constraints is the following.  Let $S = \{ t(x_1,\ldots,x_n) \mid F(x_1,\ldots,x_n) \}$.  Then the solution is an element $y^*$ of $\mathbb{Z} \cup \{-\infty,+\ifnty\}$ such that
   * if $y^* = -\infty$ then $S=\emptyset$
@@ Line 15: / Line 15: @@
 Your answer will show, given $qe$, how to solve optimization problems for any theory that has quantifier elimination.  For example, taking Presburger arithmetic, we can solve linear optimization problems such as
-\[
+\begin{equation*}
     \max \{ 2x + 3y \mid x + y \le 10 \land (7 \mid y+1) \}
-\]
+\end{equation*}
 Taking BAPA as a theory with QE, we can solve problems such as finding
-\[
+\begin{equation*}
    \max \{ |A|+3|B|+|C|\ \mid\ C \subseteq A \cup B \land |A| \le |B| \land |C| \le 100 \}
-\]
+\end{equation*}
 By generalizing the objective function to reals, we can solve non-linear but polynomial optimization problems using quantifier elimination over reals.
@@ Line 28: / Line 28: @@
 Consider language ${\cal L} = \{ {\le} \}$ and the theory $T = Conseq(T_0)$ where $T_0$ is the set of following axioms (axioms of linear order):
-\[
+\begin{equation*}
 \begin{array}{l}
     \forall x.\forall y. x \le y \land y \le x \rightarrow x=y \\
@@ Line 34: / Line 34: @@
     \forall x.\forall y. x \le y \lor y \le x
 \end{array}
-\]
+\end{equation*}
 Observe that these axioms are true in the structures of integers, natural numbers, and rational numbers, where $\le$ is interpreted as the usual less-than-equal relation on such numbers.
@@ Line 41: / Line 41: @@
 If you cannot solve the problem in its entirety, write observations that you could obtain.  You are allowed (but not required) to use any references (books, papers) that you can find (but it may be easier to solve the problem on your own).  You must cite any references that you used.  You need not write down in great detail explanations of simple facts, but if you omit any proof steps make sure that they indeed simple.
-Added afterwards:
+Solution (added afterwards):
-  * {{sav08:laeuchlileonard66linearorder.pdf|Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109–116 (1966)}} (Thanks to Yuri Gurevich, who also mentions that result follows from decidability of S2S)
+  * {{sav08:laeuchlileonard66linearorder.pdf|Läuchli, H., Leonard, J.: On the elementary theory of linear order. Fund. Math. 59, 109–116 (1966)}}
-    * [[http://www.jstor.org/sici?sici=0022-4812%28196806%2933%3A2%3C287%3AOTETOL%3E2%2E0%2ECO%3B2-I&origin=euclid|review]], {{sav08:review-linearorder.pdf|review pdf}}
+  * {{sav08:rabin69s2s.pdf|Decidability of Second-Order Theories and Automata on Infinite Trees, by Michael O. Rabin}}
+Somewhat related papers:
   * {{sav08:ehrenfeuchtordergames.pdf|A. Ehrenfeucht. An application of games to the completeness problem for formalized theories}}. Fund. Math., 49:129–141, 1961.
   * {{sav08:gurevich-thesis.pdf|Y. Gurevich: Elementary Properties of Ordered Abelian Groups}}