• English only

# Differences

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

vkuncak
Line 14: Line 14:

A language containing arbitrary function symbols and constants. ​ If $GT$ is set of ground terms over ${\cal L}$, we consider the class of interpretations $I = (GT, \alpha)$ where A language containing arbitrary function symbols and constants. ​ If $GT$ is set of ground terms over ${\cal L}$, we consider the class of interpretations $I = (GT, \alpha)$ where
-$+\begin{equation*} \alpha(f)(t_1,​\ldots,​t_n) = \alpha(f)(t_1,​\ldots,​t_n) = -$+\end{equation*}

The question of whether terms are unifiable, The question of whether terms are unifiable,
-$+\begin{equation*} r(x,f(x,y)) \doteq r(f(a,​v),​f(f(u,​b),​f(u,​u))) r(x,f(x,y)) \doteq r(f(a,​v),​f(f(u,​b),​f(u,​u))) -$+\end{equation*}
becomes the truth value of becomes the truth value of
-$+\begin{equation*} \exists x,y,u, v. r(x,f(x,y)) = r(f(a,​v),​f(f(u,​b),​f(u,​u))) \exists x,y,u, v. r(x,f(x,y)) = r(f(a,​v),​f(f(u,​b),​f(u,​u))) -$+\end{equation*}
in this theory. ​ We can express more complex constraints. in this theory. ​ We can express more complex constraints.

Line 50: Line 50:

* [[http://​theory.stanford.edu/​~tingz/​papers/​jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]]   * [[http://​theory.stanford.edu/​~tingz/​papers/​jacm07.html|The Decidability of the First-order Theory of Knuth-Bendix Order]]
+

===== Products of Structures admiting QE ====== ===== Products of Structures admiting QE ======

-Fefeman-Vaught theorem: ​if we have decidable theories.+Fefeman-Vaught theorem: ​
+  * reduce the truth value of quantified formulas over sequences of elements to truth value of formulas over elements
+  * the operations on sequences are defined point-wise

* [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]]   * [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakRinard03TheoryStructuralSubtyping.html|On the Theory of Structural Subtyping]]
+
+**Example:​** Consider logic that quantifies over pairs of integers and where addition is given by
+\begin{equation*}
+   (x,y) + (u,v) = (x+u,y+v)
+\end{equation*}
+\begin{equation*}
+   (x,y) < (u,v) \ \leftrightarrow\ ​ (x < y \land y < v)
+\end{equation*}
+Formulas in such logic, where variables range over pairs, can be reduced to Presburger arithmetic.
+
+Moreover, such reduction can be done even when variables range over infinite sequences of integers

===== Positive Integers with Multiplication ===== ===== Positive Integers with Multiplication =====
Line 62: Line 77:

Consider prime factor representation of integers: Consider prime factor representation of integers:
-$+\begin{equation*} x = \prod_{i=1}^n p_i^{\alpha_i} x = \prod_{i=1}^n p_i^{\alpha_i} -$+\end{equation*}
where $p_1,​p_2,​\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$. where $p_1,​p_2,​\ldots$ is sequence of prime numbers and $\alpha_i \ge 0$.

Line 84: Line 99:

Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$,​ Linear arithmetic over rationals ($+$, $\le$, multiplication by rational constants) with operator, for $x \in \mathbb{Q}$,​
-$+\begin{equation*} \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \} \lfloor x \rfloor = \max \{ y \in \mathbb{Z} \mid y \le x \} -$+\end{equation*}

Observe that this also subsumes Presburger arithmetic. Observe that this also subsumes Presburger arithmetic.