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
Next revision Both sides next revision
sav08:definition_of_set_constraints [2008/05/22 11:41]
vkuncak
sav08:definition_of_set_constraints [2008/05/22 11:51]
vkuncak
Line 103: Line 103:
  
 Is every set expression in set constraints monotonic? ++|Set difference is not monotonic in second argument.++ Is every set expression in set constraints monotonic? ++|Set difference is not monotonic in second argument.++
 +
  
 ===== Conditional Constraints ===== ===== Conditional Constraints =====
  
-An important property we would like to have in this semantic is a very intuitive one : \[ [[f^{-1}(f(S_1S_2))]] [[S_1]] ​\] +Let us simplify ​this expression: 
-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 ​\] +    ​f^{-2}(f(S,T)) = 
- +\] 
-The correct interpretation of this property is : +++| 
-\begin{displaymath} ​[[f^{-1}(f(S_1,​ S_2))]] ​= \left\{ \begin{array}{ll+\[ 
- \emptyset & if [[S_2]] = \emptyset ​& +   ​= ​f^{-2}(\{ f(s,t\mid s \in S, t \in \} 
-[[S_1]] & otherwise ​\\ +\] 
-\end{array} \right \end{displaymath} +++ 
 +++| 
 +\[ 
 +   = \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
 +\] 
 +++