Differences
This shows you the differences between two versions of the page.
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. | ||