Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_22 [2007/06/14 22:49] simon.blanchoud |
sav07_lecture_22 [2015/04/21 17:32] (current) |
||
---|---|---|---|
Line 43: | Line 43: | ||
===== Notion of set constraints ===== | ===== Notion of set constraints ===== | ||
+ | |||
==== Syntax ==== | ==== Syntax ==== | ||
Line 52: | Line 53: | ||
where $c$ is a constant, $v$ is a terminal (it can be a variable or function symbol), $f$ is an application function and $f^{-i}$ is the projection of th $i^{th}$ parameter of $f$. | where $c$ is a constant, $v$ is a terminal (it can be a variable or function symbol), $f$ is an application function and $f^{-i}$ is the projection of th $i^{th}$ parameter of $f$. | ||
- | When using the set contraints as it is here we might encounter problems with the substraction term ($\setminus$) as it is not monotonic. The problem is that monotonicity is needed in order to converge to a fixed point (and that is what we are looking for). | + | Note: set difference ($\setminus$) as it is not monotonic, so its use is restricted if we want to ensure existence of solutions. |
- | * Proof : | + | |
- | - In our lattice, we are trying to find a sequence of the type \[ \perp \sqsubseteq F(\perp) \sqsubseteq F(F(\perp)) \sqsubseteq ... \sqsubseteq F(x^*) = x^* \] | + | |
- | - We always have that $\perp \sqsubseteq F(\perp)$ as $\perp$ is by definition the lowest element of the lattice | + | |
- | - But inferring from there $F(\perp) \sqsubseteq F(F(\perp))$ can be done only if $F$ is monotonic. | + | |
==== Semantic ==== | ==== Semantic ==== | ||
- | We define the semantic of our syntax recursively by defining each of its elements over a language $L = \lbrace a, \ldots, f_1, \ldots, g_1, \ldots \rbrace$. We first have that : \[ [[S]] \in H \] where $H$ is the Herbrand univers, or "set of all ground terms", or also called the "term model". As we already saw, it's the set of all possibly constructed trees using language $L$ : \[ H = \lbrace a, f_1(a, a), f_1(g_1(a, a), a), \ldots \rbrace \] | + | We define the semantic of our syntax recursively by defining each of its elements over a language $L = \lbrace a, \ldots, f_1, \ldots, g_1, \ldots \rbrace$. We first have that : \begin{equation*} [[S]] \in H \end{equation*} where $H$ is the Herbrand univers, or "set of all ground terms", or also called the "term model". As we already saw, it's the set of all possibly constructed trees using language $L$ : \begin{equation*} H = \lbrace a, f_1(a, a), f_1(g_1(a, a), a), \ldots \rbrace \end{equation*} |
Given that, if the meaning of $v$ is given (i.e. we have $[[v]] = \alpha(v) \subseteq H$), then we can estimate the meaning of our language as following : | Given that, if the meaning of $v$ is given (i.e. we have $[[v]] = \alpha(v) \subseteq H$), then we can estimate the meaning of our language as following : | ||
Line 80: | Line 77: | ||
==== ==== | ==== ==== | ||
- | 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]] \] | + | An important property we would like to have in this semantic is a very intuitive one : \begin{equation*} [[f^{-1}(f(S_1, S_2))]] = [[S_1]] \end{equation*} |
This property is in fact not conserved as we can easily see using a very simple counter-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 \] | + | \begin{equation*} [[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 \end{equation*} |
The correct interpretation of this property is : | The correct interpretation of this property is : | ||
Line 146: | Line 143: | ||
From this we can deduce, as we defined previously, the following contraints : | From this we can deduce, as we defined previously, the following contraints : | ||
- | \[\begin{array}[c] | + | \begin{equation*}\begin{array}[c] |
\left { \lambda_x \right } \subseteq [[\lambda x.x]] \\ | \left { \lambda_x \right } \subseteq [[\lambda x.x]] \\ | ||
\left { \lambda_y \right } \subseteq [[\lambda y.y]] \\ | \left { \lambda_y \right } \subseteq [[\lambda y.y]] \\ | ||
\lambda_x \subseteq [[\lambda x.x]] \Rightarrow \left ( [[\lambda y.y]] \subseteq [[x]] \wedge [[x]] \subseteq [[\left ( \lambda x.x \right ) \lambda y.y]] \right ) \\ | \lambda_x \subseteq [[\lambda x.x]] \Rightarrow \left ( [[\lambda y.y]] \subseteq [[x]] \wedge [[x]] \subseteq [[\left ( \lambda x.x \right ) \lambda y.y]] \right ) \\ | ||
\lambda_y \subseteq [[\lambda x.x]] \Rightarrow \left ( [[\lambda y.y]] \subseteq [[y]] \wedge [[y]] \subseteq [[\left ( \lambda x.x \right ) \lambda y.y]] \right ) | \lambda_y \subseteq [[\lambda x.x]] \Rightarrow \left ( [[\lambda y.y]] \subseteq [[y]] \wedge [[y]] \subseteq [[\left ( \lambda x.x \right ) \lambda y.y]] \right ) | ||
- | \end{array} \] | + | \end{array} \end{equation*} |
Which leads to the following solutions : | Which leads to the following solutions : | ||
Line 185: | Line 182: | ||
[[S_1]] & otherwise \\ | [[S_1]] & otherwise \\ | ||
\end{array} \right \} \subseteq S_2 \end{displaymath} | \end{array} \right \} \subseteq S_2 \end{displaymath} | ||
+ | |||
===== Shape analysis of algebraic data types ===== | ===== Shape analysis of algebraic data types ===== | ||
+ | |||
+ | Not seen in class, have a look at the papers ! | ||
+ | |||
===== Using unary functions for interprocedural analysis ===== | ===== Using unary functions for interprocedural analysis ===== | ||
- | ===== Solving set constraints ===== | + | Not seen in class, have a look at the papers ! |
+ | ===== Solving set constraints ===== | ||
+ | |||
+ | Not seen in class, have a look at the papers ! | ||