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 [2015/04/21 17:30] (current)
Line 7: Line 7:
 ==== Syntax of Set Constraints ==== ==== Syntax of Set Constraints ====
  
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
   S ::= v | S \cap S | S \cup S | S \setminus S | f(S, ..., S) | f^{-i}(S) \\   S ::= v | S \cap S | S \cup S | S \setminus S | f(S, ..., S) | f^{-i}(S) \\
   F ::= S \subseteq S \mid F \land F   F ::= S \subseteq S \mid F \land F
 \end{array} \end{array}
-\]+\end{equation*}
 where  where 
   * $v$ - set variable   * $v$ - set variable
Line 28: Line 28:
 === Example1 === === Example1 ===
  
-\[+\begin{equation*}
     f(\{a,​f(b,​b)\},​\{b,​c\}) = \{ f(a,​b),​f(a,​c),​f(f(b,​b),​b),​ f(f(b,b),c) \}     f(\{a,​f(b,​b)\},​\{b,​c\}) = \{ f(a,​b),​f(a,​c),​f(f(b,​b),​b),​ f(f(b,b),c) \}
-\]+\end{equation*}
  
 === Example2 === === Example2 ===
  
-\[+\begin{equation*}
     f^{-2}(\{a,​f(a,​b),​f(f(a,​a),​f(c,​c))\}) = \{b,​f(c,​c)\}     f^{-2}(\{a,​f(a,​b),​f(f(a,​a),​f(c,​c))\}) = \{b,​f(c,​c)\}
-\]+\end{equation*}
  
 === Example3 === === Example3 ===
  
 What is the least solution of constraints What is the least solution of constraints
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
   a \subseteq S \\   a \subseteq S \\
   f(f(S)) \subseteq S    f(f(S)) \subseteq S 
 \end{array} \end{array}
-\]+\end{equation*}
 where $a$ is constant and $f$ is unary function symbol. where $a$ is constant and $f$ is unary function symbol.
  
Line 52: Line 52:
  
 What is the least solution of constraints What is the least solution of constraints
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
   a \subseteq S \\   a \subseteq S \\
Line 58: Line 58:
   red(black(S)) \subseteq S   red(black(S)) \subseteq S
 \end{array} \end{array}
-\]+\end{equation*}
 where $a$ is constant, $red,back$ are unary function symbols. where $a$ is constant, $red,back$ are unary function symbols.
  
Line 71: Line 71:
  
 What does the least solution of these constraints represent (where $S$,$P$ are set variables): What does the least solution of these constraints represent (where $S$,$P$ are set variables):
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
   a_1 \subseteq P \\   a_1 \subseteq P \\
Line 81: Line 81:
   or(S,S) \subseteq S   or(S,S) \subseteq S
 \end{array} \end{array}
-\]+\end{equation*}
  
  
Line 87: Line 87:
  
 We were able to talk about "the least solution"​ because previous examples can be rewritten into form  We were able to talk about "the least solution"​ because previous examples can be rewritten into form 
-\[+\begin{equation*}
   (S_1,​\ldots,​S_n) = F(S_1,​\ldots,​S_n)   (S_1,​\ldots,​S_n) = F(S_1,​\ldots,​S_n)
-\]+\end{equation*}
 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). 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).
  
Line 95: Line 95:
  
 Previous example can be rewritten as Previous example can be rewritten as
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
   P = P \cup a_1 \cup \ldots a_n \\   P = P \cup a_1 \cup \ldots a_n \\
   S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S)   S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S)
 \end{array} \end{array}
-\]+\end{equation*}
  
 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.++
Line 108: Line 108:
  
 Let us simplify this expression: Let us simplify this expression:
-\[ +\begin{equation*} 
-    f^{-2}(f(S,T)) = +    f^{-1}(f(S,T)) = 
-\]+\end{equation*}
 ++| ++|
-\[ +\begin{equation*} 
-   = f^{-2}(\{ f(s,t) \mid s \in S, t \in T \})  +   = f^{-1}(\{ f(s,t) \mid s \in S, t \in T \})  
-\]+\end{equation*}
 ++ ++
 ++| ++|
-\[+\begin{equation*}
    = \{ s_1 \in S \mid \exists t_1 \in T \}    = \{ s_1 \in S \mid \exists t_1 \in T \}
-\]+\end{equation*}
 ++ ++
 ++| ++|
-\[+\begin{equation*}
    = \left\{ \begin{array}{rl} ​    = \left\{ \begin{array}{rl} ​
        S, \mbox{ if } T \neq \emptyset \\        S, \mbox{ if } T \neq \emptyset \\
Line 128: Line 128:
               \end{array}               \end{array}
      ​\right.      ​\right.
-\]+\end{equation*}
 ++ ++
  
-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]] \] +Consider conditional constraints of the form 
-This property is in fact not conserved as we can easily see using a very simple counter-example : +\begin{equation*} 
-\[ [[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 \] +    ​T ​\neq \emptyset \rightarrow ​S_1 \subseteq S_2 
- +\end{equation*} 
-The correct interpretation of this property is : +We can transform it into 
-\begin{displaymath} [[f^{-1}(f(S_1, ​S_2))]] = \left\{ \begin{array}{ll} +\begin{equation*} 
- ​\emptyset & if [[S_2]] = \emptyset & +    ​f(S_1,T) \subseteq f(S_2,T) 
-[[S_1]] & otherwise \\ +\end{equation*} 
-\end{array} \right \end{displaymath} +for some binary function symbol $f$.   Thus, we can introduce such conditional constraints without changing expressive power or decidability.