LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:definition_of_set_constraints [2008/05/22 11:38]
vkuncak
sav08:definition_of_set_constraints [2008/05/22 11:55]
vkuncak
Line 82: Line 82:
 \end{array} \end{array}
 \] \]
 +
  
 ===== Existence of Solutions ===== ===== Existence of Solutions =====
Line 101: Line 102:
 \] \]
  
-===== Conditional Constraints =====+Is every set expression in set constraints monotonic? ++|Set difference is not monotonic in second argument.++
  
-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]] \] 
-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 \] 
  
-The correct interpretation of this property is : +===== Conditional Constraints =====
-\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}+
  
 +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.