Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav07_lecture_22 [2007/06/14 22:50]
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 :
 
sav07_lecture_22.txt · Last modified: 2015/04/21 17:32 (external edit)
 
© EPFL 2018 - Legal notice