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:51]
vkuncak
sav08:definition_of_set_constraints [2008/05/22 11:55]
vkuncak
Line 109: Line 109:
 Let us simplify this expression: Let us simplify this expression:
 \[ \[
-    f^{-2}(f(S,T)) =+    f^{-1}(f(S,T)) =
 \] \]
 ++| ++|
 \[ \[
-   = f^{-2}(\{ f(s,t) \mid s \in S, t \in T \}) +   = f^{-1}(\{ f(s,t) \mid s \in S, t \in T \}) 
 \] \]
 ++ ++
Line 131: Line 131:
 ++ ++
  
-An important property we would like to have in this semantic is a very intuitive one : \[ [[f^{-1}(f(S_1S_2))]] = [[S_1]] ​\] +Consider conditional constraints of the form 
-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_1t_2| t_1 \in [[S_1]] \wedge t_2 \in \emptyset \rbrace)]] = [[f^{-1}(\emptyset)]] = \emptyset ​\] +    T \neq \emptyset \rightarrow ​S_1 \subseteq ​S_2 
- +\] 
-The correct interpretation of this property is : +We can transform it into 
-\begin{displaymath} [[f^{-1}(f(S_1S_2))]] = \left\{ \begin{array}{ll} +\[ 
- ​\emptyset & if [[S_2]] = \emptyset & +    ​f(S_1,T) \subseteq ​f(S_2,T) 
-[[S_1]] & otherwise \\ +\] 
-\end{array} \right \end{displaymath} +for some binary function symbol $f$.   Thuswe can introduce such conditional constraints without changing expressive power or decidability.