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]
Line 1: Line 1:
-===== Definition of Set Constraints ===== 
- 
-Set constraints are a logic used in program analysis. ​ In set constraints,​ each variable denotes a set of ground terms. 
- 
-Let $L$ be a language of function symbols and constants. ​ We write $f \in L$ for an element of $L$.  Let $GT$ be the set of ground terms in language $L$. 
- 
-==== Syntax of Set Constraints ==== 
- 
-\[ 
-\begin{array}{l} 
-  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 
-\end{array} 
-\] 
-where  
-  * $v$ - set variable 
-  *  $\cap,​\cup,​\setminus,​\subseteq$ - standard set operations and relations 
-  * $f \in L$ - function symbol 
-  * in $f^{-i}$, $i$ is an integer between 1 and arity of $f$ 
- 
-==== Semantic ==== 
- 
-  * $v$ - set variable, subset of $GT$ 
-  * $\cap,​\cup,​\setminus,​\subseteq$ - standard set operations and relations 
-  * $f(S_1,​\ldots,​S_n) = \{ f(t_1,​\ldots,​t_n) \mid t_1 \in S_1,\ldots, t_n \in S_n \}$ 
-  * $f^{-i}(S) = \{ t_i \mid f(t_1,​\ldots,​t_n) \in S \}$ 
- 
-=== Example1 === 
- 
-\[ 
-    f(\{a,​f(b,​b)\},​\{b,​c\}) = \{ f(a,​b),​f(a,​c),​f(f(b,​b),​b),​ f(f(b,b),c) \} 
-\] 
- 
-=== Example2 === 
- 
-\[ 
-    f^{-2}(\{a,​f(a,​b),​f(f(a,​a),​f(c,​c))\}) = \{b,​f(c,​c)\} 
-\] 
- 
-=== Example3 === 
- 
-What is the least solution of constraints 
-\[ 
-\begin{array}{l} 
-  a \subseteq S \\ 
-  f(f(S)) \subseteq S  
-\end{array} 
-\] 
-where $a$ is constant and $f$ is unary function symbol. 
- 
-=== Example4 === 
- 
-What is the least solution of constraints 
-\[ 
-\begin{array}{l} 
-  a \subseteq S \\ 
-  black(S) \subseteq S \\ 
-  red(black(S)) \subseteq S 
-\end{array} 
-\] 
-where $a$ is constant, $red,back$ are unary function symbols. 
- 
-=== Example5 === 
- 
-Let $L = \{a_1,​\ldots,​a_n,​ not, and, or, implies\}$ where  
-  * $a_1,​\ldots,​a_n$ are constants representing propositional constants 
-  * $not$ is unary function symbol representing negation in abstract syntax tree 
-  * $and,​or,​implies$ are binary function symbols representing $\land,​\lor,​\rightarrow$ in syntax tree 
- 
-Then the set of ground terms $GT$ represents propositional formulas. 
- 
-What does the least solution of these constraints represent (where $S$,$P$ are set variables): 
-\[ 
-\begin{array}{l} 
-  a_1 \subseteq P \\ 
-  \ldots \\ 
-  a_n \subseteq P \\ 
-  P \subseteq S \\ 
-  not(P) \subseteq S \\ 
-  and(S,S) \subseteq S \\ 
-  or(S,S) \subseteq S 
-\end{array} 
-\] 
- 
- 
-===== Existence of Solutions ===== 
- 
-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). 
- 
-=== Example === 
- 
-Previous example can be rewritten as 
-\[ 
-\begin{array}{l} 
-  P = P \cup a_1 \cup \ldots a_n \\ 
-  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^{-2}(f(S,​T)) = 
-\] 
-++| 
-\[ 
-   = f^{-2}(\{ 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. 
-\] 
-++