LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:set_constraints_for_algebraic_datatype_inference [2008/05/22 12:11]
vkuncak
sav08:set_constraints_for_algebraic_datatype_inference [2015/04/21 17:30] (current)
Line 24: Line 24:
  
 We infer the subset of formulas returned by this function using set constraints. ​ Introduce set for each case of pattern matching expression. ​ Let '​res'​ denote the set of values that can be returned by the function. ​ We obtain the system of constraints:​ We infer the subset of formulas returned by this function using set constraints. ​ Introduce set for each case of pattern matching expression. ​ Let '​res'​ denote the set of values that can be returned by the function. ​ We obtain the system of constraints:​
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
    atom \subseteq S_1 \\    atom \subseteq S_1 \\
Line 32: Line 32:
    res = S_1 \cup S_2 \cup S_3 \cup S_4    res = S_1 \cup S_2 \cup S_3 \cup S_4
 \end{array} \end{array}
-\]+\end{equation*}
  
 We can prove that the least fixpoint is the same as the least fixpoint of We can prove that the least fixpoint is the same as the least fixpoint of
-\[+\begin{equation*}
     res = atom \cup and(res,​res) \cup not(res)     res = atom \cup and(res,​res) \cup not(res)
-\]+\end{equation*}
 the last expression is a description of the solution set.  We can use it later on to prove that the result does not mention '​or'​ syntax tree node. the last expression is a description of the solution set.  We can use it later on to prove that the result does not mention '​or'​ syntax tree node.