Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
complexity [2007/10/04 23:15] philippe.suter |
complexity [2007/10/04 23:18] philippe.suter |
||
|---|---|---|---|
| Line 62: | Line 62: | ||
| \[ (S_1 \times \ldots \times S_n) \subseteq (A_1 \times \ldots \times A_n) \cup (\ldots) \cup (Z_1 \times \ldots \times Z_n) \] | \[ (S_1 \times \ldots \times S_n) \subseteq (A_1 \times \ldots \times A_n) \cup (\ldots) \cup (Z_1 \times \ldots \times Z_n) \] | ||
| - | When checking completeness, the set $(S_1 \times \ldots \times S_n)$ is the domain of the scrutinee, when checking reachability, it is the set of the observed pattern. (Note that this is in fact checking subsumption. Proper reachability checking would include verifying that the pattern set is a subset of the scrutinee set, but this does not introduce any additional complexity.) Also note that the sets over which the union is taken corresponds to patterns which satisfy one of these properties: | + | When checking completeness, the set $(S_1 \times \ldots \times S_n)$ is the domain of the scrutinee, when checking reachability, it is the set of the observed pattern. (Note that this is in fact checking subsumption. Proper reachability checking would include verifying that the pattern set is a subset of the scrutinee set, but this does not introduce any additional complexity.) Also note that the sets over which the union is taken correspond to patterns which satisfy one of the following properties: |
| * the pattern has no guard | * the pattern has no guard | ||
| * the pattern has a guard, but there exists a set of patterns with the same signature such that the disjunction of their guards is equivalent to the true statement | * the pattern has a guard, but there exists a set of patterns with the same signature such that the disjunction of their guards is equivalent to the true statement | ||