# Differences

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

 sav08:definition_of_set_constraints [2008/05/22 11:51]vkuncak sav08:definition_of_set_constraints [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/05/22 11:55 vkuncak 2008/05/22 11:51 vkuncak 2008/05/22 11:51 vkuncak 2008/05/22 11:50 vkuncak 2008/05/22 11:50 vkuncak 2008/05/22 11:41 vkuncak 2008/05/22 11:38 vkuncak 2008/05/22 11:36 vkuncak 2008/05/22 11:29 vkuncak 2008/05/22 11:28 vkuncak 2008/05/22 11:24 vkuncak 2008/05/22 11:05 vkuncak 2008/05/22 10:52 vkuncak 2008/05/22 10:50 vkuncak 2008/05/22 10:48 vkuncak 2008/05/22 10:38 vkuncak 2008/05/22 10:37 vkuncak 2008/05/22 10:37 vkuncak 2008/05/22 10:36 vkuncak 2008/05/22 10:20 vkuncak 2008/05/22 00:10 vkuncak created Next revision Previous revision 2008/05/22 11:55 vkuncak 2008/05/22 11:51 vkuncak 2008/05/22 11:51 vkuncak 2008/05/22 11:50 vkuncak 2008/05/22 11:50 vkuncak 2008/05/22 11:41 vkuncak 2008/05/22 11:38 vkuncak 2008/05/22 11:36 vkuncak 2008/05/22 11:29 vkuncak 2008/05/22 11:28 vkuncak 2008/05/22 11:24 vkuncak 2008/05/22 11:05 vkuncak 2008/05/22 10:52 vkuncak 2008/05/22 10:50 vkuncak 2008/05/22 10:48 vkuncak 2008/05/22 10:38 vkuncak 2008/05/22 10:37 vkuncak 2008/05/22 10:37 vkuncak 2008/05/22 10:36 vkuncak 2008/05/22 10:20 vkuncak 2008/05/22 00:10 vkuncak created 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.