Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
cartesianproducts [2015/04/21 17:41] wikiadmin |
cartesianproducts [2015/04/21 17:44] wikiadmin |
||
---|---|---|---|
Line 65: | Line 65: | ||
This is readily expressible thanks to the set operators: | This is readily expressible thanks to the set operators: | ||
- | \[EvenNode \cap OddNode = \emptyset \] | + | \begin{equation*}EvenNode \cap OddNode = \emptyset \end{equation*} |
- | \[EvenNode \cup OddNode = Node \] | + | \begin{equation*}EvenNode \cup OddNode = Node \end{equation*} |
==== Analyzing patterns ==== | ==== Analyzing patterns ==== | ||
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) | ||