Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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*}
 ++ ++
 +
 +Consider conditional constraints of the form
 +\begin{equation*}
 +    T \neq \emptyset \rightarrow S_1 \subseteq S_2
 +\end{equation*}
 +We can transform it into
 +\begin{equation*}
 +    f(S_1,T) \subseteq f(S_2,T)
 +\end{equation*}
 +for some binary function symbol $f$.   Thus, we can introduce such conditional constraints without changing expressive power or decidability.
  
 
sav08/definition_of_set_constraints.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice