Differences

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

--- sav08:definition_of_set_constraints [2008/05/22 11:36]
vkuncak
+++ sav08:definition_of_set_constraints [2008/05/22 11:55]
vkuncak
@@ Line 18: / Line 18: @@
   * $f \in L$ - function symbol
   * in $f^{-i}$, $i$ is an integer between 1 and arity of $f$
 ==== Semantic ====
@@ Line 97: / Line 92: @@
 where $F (2^{S})^n \to (2^{S})^n$ is a $\sqcup$-morphism (and therefore monotonic and $\omega$-continuous).  The least solution can therefore be computed by fixpoint iteration (but it may contain infinite sets).
-===== Conditional Constraints =====
+=== Example ===
-An important property we would like to have in this semantic is a very intuitive one : \[ [[f^{-1}(f(S_1, S_2))]] = [[S_1]] \]
+Previous example can be rewritten as
-This property is in fact not conserved as we can easily see using a very simple counter-example :
+\[
-\[ [[f^{-1}(f(S_1, \emptyset))]] = [[f^{-1}(\lbrace f(t_1, t_2) | t_1 \in [[S_1]] \wedge t_2 \in \emptyset \rbrace)]] = [[f^{-1}(\emptyset)]] = \emptyset \]
+\begin{array}{l}
+  P = P \cup a_1 \cup \ldots a_n \\
+  S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S)
+\end{array}
+\]
-The correct interpretation of this property is :
+Is every set expression in set constraints monotonic? ++|Set difference is not monotonic in second argument.++
-\begin{displaymath} [[f^{-1}(f(S_1, S_2))]] = \left\{ \begin{array}{ll}
- \emptyset & if [[S_2]] = \emptyset &
-[[S_1]] & otherwise \\
-\end{array} \right \end{displaymath}
+===== Conditional Constraints =====
+Let us simplify this expression:
+\[
+    f^{-1}(f(S,T)) =
+\]
+++|
+\[
+   = f^{-1}(\{ f(s,t) \mid s \in S, t \in T \})
+\]
+++
+++|
+\[
+   = \{ s_1 \in S \mid \exists t_1 \in T \}
+\]
+++
+++|
+\[
+   = \left\{ \begin{array}{rl}
+       S, \mbox{ if } T \neq \emptyset \\
+       \emptyset, \mbox{ if } T = \emptyset
+              \end{array}
+     \right.
+\]
+++
+Consider conditional constraints of the form
+\[
+    T \neq \emptyset \rightarrow S_1 \subseteq S_2
+\]
+We can transform it into
+\[
+    f(S_1,T) \subseteq f(S_2,T)
+\]
+for some binary function symbol $f$.   Thus, we can introduce such conditional constraints without changing expressive power or decidability.