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
Last revision Both sides next revision
sav07_lecture_6_skeleton [2007/03/30 19:57]
vkuncak 		sav07_lecture_6_skeleton [2007/03/30 20:53]
vkuncak
Line 25: Line 25:
  
 We typically do not write universal quantifiers either, because we know that all variables in a clause are universally quantified. We typically do not write universal quantifiers either, because we know that all variables in a clause are universally quantified.
 +
  
  
Line 54: Line 55:
  
 **Herbrand'​s theorem**: If a set of clauses in language L is true in some interpretation with domain D, then it is true in an interpretation with domain Term(L). **Herbrand'​s theorem**: If a set of clauses in language L is true in some interpretation with domain D, then it is true in an interpretation with domain Term(L).
 +
 **Proof sketch**: If set $S$ of clauses is true in interpretation $e$, then define interpretation $e_T$ with domain Term(L) by evaluating functions as in the term model $[[f]](t_1,​t_2) = f(t_1,​t_2)$,​ and defining the value of relations by $[[R]]e_T = \{(t_1,​t_2)\mid [[R(t_1,​t_2)]]e = \mbox{true} \}$ (end of sketch). **Proof sketch**: If set $S$ of clauses is true in interpretation $e$, then define interpretation $e_T$ with domain Term(L) by evaluating functions as in the term model $[[f]](t_1,​t_2) = f(t_1,​t_2)$,​ and defining the value of relations by $[[R]]e_T = \{(t_1,​t_2)\mid [[R(t_1,​t_2)]]e = \mbox{true} \}$ (end of sketch).
  
Line 187: Line 189:
  
  
 +==== Background on Lattices ====
  
 +Recall notions of [[preorder]],​ [[partial order]], [[equivalence relation]].
  
 +Partial order where each two element set has 
 +  * supremum (least upper bound, join, $\sqcup$)
 +  * infimum (greatest lower bound, meet, $\sqcap$)
 +
 +So, we have
 +\begin{equation*}
 +\begin{array}{ll}
 +  x \sqsubseteq x \sqcup y & \mbox{(bound)} \\
 +  y \sqsubseteq x \sqcup y & \mbox{(bound)} \\
 +  x \sqsubseteq z \ \land\ y \sqsubseteq z\ \rightarrow\ x \sqcup y \sqsubseteq z & \mbox{(least)}
 +\end{array}
 +\end{equation*}
 +and dually for $\sqcap$.
 +
 +See also [[wk>​Lattice (order)]]
 +
 +Example [[wk>​Hasse diagram]]s for powerset of {1,2} and for constant propagation.
 +
 +Properties of a lattice
 +  * finite lattice
 +  * finite ascending chain lattice
  
 ==== Basic notions of abstract interpretation ==== ==== Basic notions of abstract interpretation ====
Line 218: Line 243:
  
 This is the most important condition for abstract interpretation. This is the most important condition for abstract interpretation.
- 
-When equality holds, we have the "best abstract transformer"​ (the most precise one) for a given $\gamma$. 
  
 One way to find $sp\#$ it is to have $\alpha$ that goes the other way One way to find $sp\#$ it is to have $\alpha$ that goes the other way
Line 239: Line 262:
   sp\#(a,r) = \alpha(sp(\gamma(a),​r))   sp\#(a,r) = \alpha(sp(\gamma(a),​r))
 \end{equation*} \end{equation*}
- +and we call this "the best transformer".
-All else being same, the best transformer ​is better, because it gives as precise results as we can get with a given analysis domain. ​ But sometimes it can be more expensive so we use a weaker one. +
- +
-==== Lattices ==== +
- +
-Partial order where each two element set has  +
-  * supremum (least upper bound, join, $\sqcup$) +
-  * infimum (greatest lower bound, meet, $\sqcap$) +
- +
-So, we have +
-\begin{equation*} +
-\begin{array}{ll} +
-  x \sqsubseteq x \sqcup y & \mbox{(bound)} \\ +
-  y \sqsubseteq x \sqcup y & \mbox{(bound)} \\ +
-  x \sqsubseteq z \ \land\ y \sqsubseteq z\ \rightarrow\ x \sqcup y \sqsubseteq z & \mbox{(least)} +
-\end{array} +
-\end{equation*} +
-and dually for $\sqcap$. +
- +
-See also [[wk>​Lattice (order)]] +
- +
-Example [[wk>​Hasse diagram]]s for powerset of {1,2} and for constant propagation. +
- +
-Properties of a lattice +
-  * finite lattice +
-  * finite ascending chain lattice+