Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:definition_of_set_constraints [2008/05/22 11:50] 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 130: | 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]] \] | + | |
- | 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_1, t_2) | t_1 \in [[S_1]] \wedge t_2 \in \emptyset \rbrace)]] = [[f^{-1}(\emptyset)]] = \emptyset \] | + | |
- | + | ||
- | 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 & | + | |
- | [[S_1]] & otherwise \\ | + | |
- | \end{array} \right \end{displaymath} | + | |
+ | 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. | ||