## 3  The useful clause problem

We express pattern matching anomalies in the matrix framework.

Definition 4 (Exhaustiveness)   Let P be a pattern matrix. Matrix P is exhaustive, if and only if, for all value vectors v of the appropriate type, there exists a row in P that filters v in the sense of Definition 2.
Definition 5 (Useless clause)   Let P be a pattern matrix. Row number i in P is useless, if and only if there does not exists a value vector v that matches row number i in the sense of Definition 2.

Useless clauses are sometimes called redundant. In our opinion, “useless” is more precise, since it conveys the semantical nature of the concept better.

Example 2   Let P and Q be the following two pattern matrices.
P =

 Nil _ _ Nil

Q =

 Nil _ _ Nil One(_) _ _ One(_) Cons (_,_) _ _ Cons(_,_)

Matrix P is not exhaustive, since, for instance, vector v = (One (0) One (0)) does not match any row of P.

By contrast, matrix Q is exhaustive. Let us consider any value vector v of the appropriate type. Then, v1 and v2 are instances of the patterns Nil, One(_), or Cons(_,_). That is, we may partition values into nine sets denoted by nine different pattern vectors. It turns out that this partition is precise enough to apply Definition 2.

 If v→  is an instance of… then, v→  matches row number… (Nil Nil)   (Nil One(_))   (Nil Cons(_,_)) 1 (One(_) Nil)   (Cons(_,_) Nil) 2 (One(_) One(_))   (One(_) Cons(_,_)) 3 (Cons(_,_) One(_)) 4 (Cons(_,_) Cons(_,_)) 5

As another consequence, one may observe that row number 6 of matrix Q is useless.

Because we use the ML definition of pattern matching (Definition 2) we claim that the two definitions above express what is generally understood by “an exhaustive match” and “an useless clause”, However it is intuitively clear that the two questions are quite similar, and in fact they can be expressed using the following definition.

Definition 6 (Useful clause)   Let P be a pattern matrix of size m × n and let q be a pattern vector of size n. Vector q is useful with respect to matrix P, if and only if
∃
 → v
P ⋠
 → v
∧
 → q
≼
 → v
.
We write U(P,q ) for the formula above We also note M(P, q ) the following set of matching value vectors:
M(P
 → q
) = {
 → v
∣ P ⋠
 → v
∧
 → q
≼
 → v
}.
Thus, U(P,q ) simply means that M(P, q ) is not empty.
Proposition 1
1. Matrix P is exhaustive, if and only if U(P,(_⋯_)) is false.
2. Row number i in matrix P is useless, if and only if U(P[1…i),p i) is false.
Proof: Corollary of definitions.□

Our framework of two separate definitions 2 and 3 exposes that, as far as pattern matching anomalies are concerned, the matching predicate can be simplified. More precisely, it is important to notice that v matches some row in P (Definition 2) is equivalent to Pv (Definition 3). In other words, the order of rows in P is irrelevant while computing U(P,q ).

### 3.1  Solving the useful clause problem

In this section we compute U recursively. We proceed by first defining a recursive function Urec and then showing U = Urec. The definition of Urec owes much to the traditional compilation of ML pattern matching to decision trees — Pettersson [1992] gives a modern presentation of this quite ancient compilation scheme.

Let thus P be a pattern matrix of size m × n and q  be a pattern vector of size n. Induction proceeds by decomposing P and q along first column.

Base case
If there is no column (i.e. n=0), then the value of Urec(P, ()) depends upon the number of rows m of matrix P.
1. If P has some rows (i.e. m > 0), we define Urec(( ), ()) to be false.
2. If m is zero, then we define Urec(∅,()) to be true. More generally, although not really necessary, we can define Urec(∅,q ) to be true for any vector q of any size n.
Base cases are summarized as follows:
Urec(

, ()) = False          Urec(∅ ,
 → q
) = True.
Induction
If there are columns (n > 0), then there are three sub-cases depending upon the nature of pattern q1.
1. Pattern q1 is a constructed pattern, that is q1 = c(r1, … , ra). From matrix P, we extract the new specialized matrix S(c,P). The new matrix S(c,P) is of width a+n−1 and its rows are defined from the rows of P, according to the first component of these rows.
p1iS(c,P)
c(r1, … , ra)r1rap2ipni
c′(r1, … , ra)   (c′ ≠ c)No row
___p2ipni
(r1r2)
S(c,

 r1 p2i ⋯ pni r2 p2i ⋯ pni

)
Notice that a given row p i, may induce one, none or several rows in S(c, P). In the following, we note S(c, q ) the application of S to a vector, when it yields a vector.
S(c, (c(r1, … , raq2qn))=(r1⋯ ra   q2⋯ qn)
S(c, (_ q2qn))=
(

 _⋯ _ ◥ ▼ ◤
a times
q2⋯ qn)
We also consider specialization of value vectors when relevant, that is when v1 = c(w1, … , wa).

Finally, in the case where q1 is c(r1, … , ra), we define:

Urec(P
 → q
) = Urec(S(c,P), S(c,
 → q
)).
2. Pattern q1 is a wildcard. Let Σ = {c1, c2, … , cz} be the set of constructors that appear as root constructors of the patterns of P’s first column (and also as root constructors of their arguments when they are or-patterns). The computation of Urec depends on whether set Σ is a complete signature or not. In the former case, any instance v of q  necessarily possesses a first component whose root constructor belongs to Σ. In the latter case, it turns out that it suffices to examine those constructors that do not belong to Σ. Here, computing Urec significantly departs from compilation to decision trees, which of course has to take all constructors into account.
1. Set Σ constitutes a complete signature. Then we define:
Urec(P
 → q
)  =
 z ∨ k=1
Urec(S(ck,P),S(ck
 → q
)).
2. Set Σ is not a complete signature. From P, we extract the new default matrix D(P) of width n−1.
p1iD(P)
ck(t1, … , tak)No row
_p2i ⋯ pni
(r1r2)
D(

 r1 p2i ⋯ pni r2 p2i ⋯ pni

)
Matrix D(P) is defined in all situations, whether Σ is a complete signature or not. However, D(P) is useful for computing Urec only in the latter case. We define:
 Urec(P, (_ q2⋯qn)) = Urec(D(P), (q2⋯qn)).
Observe that when Σ is empty, i.e. when the first column of P is made of wildcards and of or-patterns thereof, then Σ is not a complete signature. Thus the definition above also apply.
3. When pattern q1 is an or-pattern (r1r2), we define:
 Urec(P,((r1∣r2) q2⋯qn)) = Urec(P,(r1 q2⋯qn)) ∨ Urec(P,(r2 q2⋯qn)).

We now establish a few “key” properties of matrix specialization (1 below) and of the default matrix (2 to 4 below). Basically, the key property of specialization expresses that matching by P and S(c, P) are equivalent for value vectors whose first component admits c as a root constructor; while the key properties of the default matrix express the equivalence of matching by P and D(P) in more detailed situations.

Lemma 1 (Key properties)   For any matrix P, constructor c, and value vector v such that v1 = c(w1, … , wa) (all being of the appropriate types), we have:
P ⋠
 → v
⇐⇒ S(cP) ⋠S(c
 → v
).      (1)
Additionally, for any value vector v, we have:
 P ⋠(v1 v2⋯vn) =⇒ D(P) ⋠(v2⋯vn).      (2)
Furthermore, given any matrix P, let Σ be set of the root constructors of P’s first column. If Σ is not empty, then for any constructor c not in Σ and any value vector (w1wa   v2vn), we have:
 D(P) ⋠(v2⋯vn) =⇒ P ⋠(c(w1, … , wa) v2⋯vn).      (3)
If Σ is empty, then, for any value vector v, we have instead:
 D(P) ⋠(v2⋯vn) =⇒ P ⋠(v1 v2⋯vn).      (4)
Proof: Mechanical application of definitions.□

We could of course have formulated the key properties by reversing implications and by using ≼ in place of ⋠. However, we adopt the negated formulation, to match Definition 2. Nevertheless, we shall also consider (1) when P has exactly one row. In that case, for any value vector v such that v1 = c(w1, … , wa), we write more directly:

 → q
≼
 → v
⇐⇒ S(c
 → q
) ≼ S(c,
 → v
).
Proposition 2   For any matrix P and pattern vector q of appropriate sizes and types, we have:
U(P
 → q
) = Urec(P
 → q
).
Proof: Base cases are easy. Let first q  be the empty pattern vector, written (). The set of q  instances consists of the unique empty value vector, also written (). If P’s rows exist and are empty, then P’s first row filters the value vector ().
 M( ⎛ ⎝ ⎞ ⎠ , ()) = ∅.
Moreover, if P has no rows, then it cannot filter any value, We have:
M(∅,
 → q
) = {
 → v
∣
 → q
≼
 → v
}.
And we conclude, since q  has at least one instance for any q.

To prove inductive cases, it suffices to show that U meets the equations that define Urec.

1. If q1 = c(r1, … , ra) for some constructor c, then we need prove:
U(P,
 → q
) = U(S(cP), S(c
 → q
)).
However, by (1) applied to both P and q, we have the stronger result:
M(P,
 → q
) =

 → v
∣ S(c
 → v
) ∈ M(S(cP), S(c
 → q
))

.
Namely, remember that U(P, q ) means that the set M(P, q) of matching values is not empty (Definition 6).
2. If q1 is a wildcard, then let Σ = {c1, …, cz} be as in the definition of Urec.
1. If Σ is a complete signature. For any ck in Σ, we define the set Mk:
Mk = M(S(ckP), S(ck
 → q
)).
By typing, for any value v1 of the appropriate type, we have q1v1, if and only if there exists a constructor ck in Σ and values w1, …, wak such that v1 = ck(w1, … , wak). Thus, by property (1), one easily shows:
M(P
 → q
) =
 z ∪ k=1

 → v
∣ S(ck
 → v
)∈ Mk

.
And we can conclude:
U(P
 → q
) =
 z ∨ k=1
U(S(ck,P), S(c,
 → q
)).
2. In all situations, we have (by (2)):
M(P
 → q
) ⊆

 → v
∣ (v2vn) ∈ M(D(P), (q2qn))

.
In the case where Σ is empty, the reverse inclusion holds — by (4). And we can conclude, by the “type are not empty” axiom.

It is worth noticing that the reverse inclusion does not hold when Σ is non-empty. Namely, when considering sets of matching values M, we have to take all possible values into account. Anyway, by the inclusion above, we have: U(P, q ) =⇒ U(D(P), (q2qn)).

Conversely, assume U(D(P), (q2qn)) = True, and let t be the type of the first component of tested value vectors. Then, there exists (v2vn) such that D(P) ⋠(v2vn) and (q2qn) ≼ (v2vn). Furthermore, by the hypothesis “Σ does not hold all the constructors of type t” we know that there exists some constructor c of type t1 × ⋯ × tat such that c ∉Σ. Thus, by our axiom “types are not empty”, there exist values w1,… , wa of respective types t1,…, ta. Then, vector v = (c(w1, … , wav2vn) is a witness of the validity of U(P, q ), by (3) and q1 = _ ≼ v1.

3. If qi is an or-pattern (r1r2), then, by definition of ≼ for or-patterns, we have:
 M(P, ((r1∣r2) q2⋯qn)) = M(P, (r1 q2⋯qn)) ⋃ M(P, (r2 q2⋯qn)).

### 3.2  Detecting the anomalies

Since we know how to compute U, we can detect pattern matching anomalies. Given some expression match … with p1 -> e1 | p2 -> e2 | … | pm -> em, exhaustiveness is checked by computing:

Urec(

 p1 p2 ⋮ pm

, (_));

while the usefulness of clause number i is checked by computing:

Urec(

 p1 p2 ⋮ pi−1

, (pi)).