Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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