Lab for Automated Reasoning and Analysis 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*}
 ++ ++
 +
 +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