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
cartesianproducts [2015/04/21 17:43]
wikiadmin 		cartesianproducts [2015/04/21 17:44]
wikiadmin
Line 112: Line 112:
  
 The constraints on the patterns are: The constraints on the patterns are:
-\[p_1 = ENode \] +\begin{equation*}p_1 = ENode \end{equation*} 
-\[p_2 = ELeaf \]+\begin{equation*}p_2 = ELeaf \end{equation*}
  
 Completeness is expressed as $p_1 \cup p_2 \supseteq Tree$ and disjointness as $p_1 \cap p_2 = \emptyset$. Both are trivial with our axioms. Completeness is expressed as $p_1 \cup p_2 \supseteq Tree$ and disjointness as $p_1 \cap p_2 = \emptyset$. Both are trivial with our axioms.
Line 129: Line 129:
 Here we have two positions ("​annoted"​ [a] and [b]). The types A and B are both Tree. We hence have $s = Tree \times Tree$. Here we have two positions ("​annoted"​ [a] and [b]). The types A and B are both Tree. We hence have $s = Tree \times Tree$.
 The constraints on the patterns are: The constraints on the patterns are:
-\[p_1 = EvenNode \times OddNode \] +\begin{equation*}p_1 = EvenNode \times OddNode \end{equation*} 
-\[p_2 = EvenNode \times EvenNode \] +\begin{equation*}_2 ​= EvenNode \times EvenNode \end{equation*} 
-\[p_3 = OddNode \times Tree \] +\begin{equation*}p_3 = OddNode \times Tree \end{equation*} 
-\[p_4 = ELeaf \times Tree \]+\begin{equation*}p_4 = ELeaf \times Tree \end{equation*}
 (recall that when a position is not present in a pattern we use its general type) (recall that when a position is not present in a pattern we use its general type)