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:42]
wikiadmin [Using sets] 		cartesianproducts [2015/04/21 17:44]
wikiadmin
Line 91: Line 91:
  
 The set of values for the scrutinee which **will** be matched by a given pattern can now be seen as a subset of $s$ expressed by constraints. Recall that each extractor $ex$ has a corresponding set $EX$ which defines all values which it matches. A pattern will successfully match a value if all extractors in it match what they are submitted with. In other words, for a pattern with calls to extractors $ex_1,​ex_2,​\ldots$ is a cartesian product of the same dimension as $s$, where the positions corresponding to the extractors are "​replaced"​ with the proper sets: The set of values for the scrutinee which **will** be matched by a given pattern can now be seen as a subset of $s$ expressed by constraints. Recall that each extractor $ex$ has a corresponding set $EX$ which defines all values which it matches. A pattern will successfully match a value if all extractors in it match what they are submitted with. In other words, for a pattern with calls to extractors $ex_1,​ex_2,​\ldots$ is a cartesian product of the same dimension as $s$, where the positions corresponding to the extractors are "​replaced"​ with the proper sets:
-\[ EX_1 \times B \times EX_2 \times \ldots \]. Note that by construction of the types $A,​B,​\ldots$,​ this is always a subset of $s$.+\begin{equation*} ​EX_1 \times B \times EX_2 \times \ldots \end{equation*}. Note that by construction of the types $A,​B,​\ldots$,​ this is always a subset of $s$.
  
 === Completeness,​ disjointness and the like === === Completeness,​ disjointness and the like ===
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)