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:29] vkuncak |
sav08:definition_of_set_constraints [2008/05/22 11:55] vkuncak |
||
---|---|---|---|
Line 18: | Line 18: | ||
* $f \in L$ - function symbol | * $f \in L$ - function symbol | ||
* in $f^{-i}$, $i$ is an integer between 1 and arity of $f$ | * in $f^{-i}$, $i$ is an integer between 1 and arity of $f$ | ||
- | |||
- | |||
- | |||
- | |||
- | |||
==== Semantic ==== | ==== Semantic ==== | ||
Line 87: | Line 82: | ||
\end{array} | \end{array} | ||
\] | \] | ||
+ | |||
===== Existence of Solutions ===== | ===== Existence of Solutions ===== | ||
- | ===== Conditional Constraints ===== | + | We were able to talk about "the least solution" because previous examples can be rewritten into form |
+ | \[ | ||
+ | (S_1,\ldots,S_n) = F(S_1,\ldots,S_n) | ||
+ | \] | ||
+ | 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). | ||
- | 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]] \] | + | === Example === |
- | 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 : | + | Previous example can be rewritten as |
- | \begin{displaymath} [[f^{-1}(f(S_1, S_2))]] = \left\{ \begin{array}{ll} | + | \[ |
- | \emptyset & if [[S_2]] = \emptyset & | + | \begin{array}{l} |
- | [[S_1]] & otherwise \\ | + | P = P \cup a_1 \cup \ldots a_n \\ |
- | \end{array} \right \end{displaymath} | + | S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S) |
+ | \end{array} | ||
+ | \] | ||
+ | Is every set expression in set constraints monotonic? ++|Set difference is not monotonic in second argument.++ | ||
+ | |||
+ | |||
+ | ===== Conditional Constraints ===== | ||
+ | |||
+ | Let us simplify this expression: | ||
+ | \[ | ||
+ | f^{-1}(f(S,T)) = | ||
+ | \] | ||
+ | ++| | ||
+ | \[ | ||
+ | = f^{-1}(\{ f(s,t) \mid s \in S, t \in T \}) | ||
+ | \] | ||
+ | ++ | ||
+ | ++| | ||
+ | \[ | ||
+ | = \{ s_1 \in S \mid \exists t_1 \in T \} | ||
+ | \] | ||
+ | ++ | ||
+ | ++| | ||
+ | \[ | ||
+ | = \left\{ \begin{array}{rl} | ||
+ | S, \mbox{ if } T \neq \emptyset \\ | ||
+ | \emptyset, \mbox{ if } T = \emptyset | ||
+ | \end{array} | ||
+ | \right. | ||
+ | \] | ||
+ | ++ | ||
+ | |||
+ | Consider conditional constraints of the form | ||
+ | \[ | ||
+ | T \neq \emptyset \rightarrow S_1 \subseteq S_2 | ||
+ | \] | ||
+ | We can transform it into | ||
+ | \[ | ||
+ | f(S_1,T) \subseteq f(S_2,T) | ||
+ | \] | ||
+ | for some binary function symbol $f$. Thus, we can introduce such conditional constraints without changing expressive power or decidability. | ||