Subsumption Matrices and Transitive Closure

[User's Manual]
It has been shown (Aït-Kaci, 1989) that partially ordered types can be represented in the form of a bit-vector encoding.

Definition 1   Given a partially ordered set, $\langle P, \sqsubseteq\rangle$, and a total ordering of $P$'s elements, $p_1, p_2,\ldots , p_{\vert p\vert}$, the subsumption matrix, $S$, of $P$ is a $\vert P\vert\times\vert P\vert$ Boolean matrix, where $S_{i,j} = 1$ iff $p_i \sqsubseteq p_j$.

We can use the $i$th row of $S$ to encode the type $p_i$, with unification corresponding to a bit-wise AND. For instance, the subsumption matrix of the type hierarchy in Figure 3.1 is given in Figure 3.2. The AND of the rows for $a$ and $d$ yields the row $e$, for example.

Figure 3.1: An example partial order of types

Figure 3.2: The subsumption matrix, $S$, of Figure 3.1

In practice, however, we do not initially have access to this information and we need to compute that. What we do have access to is the immediate subsumption relation that is specified in type subsumption declarations, with reflexive transitive closure being implicit. We can build a base subsumption matrix, $H$, in the same way, by using the immediate subsumption relation. The question is then how to obtain $S$ from $H$ quickly. The base subsumption matrix in Figure 3.2 is given in Figure 3.3.

Figure 3.3: The base subsumption matrix, $H$, of Figure 3.1

One way to achieve this is a reflexive-transitive closure, by directly filling in the diagonal of $H$ with 1s (reflexive) and multiplying the result by itself until it reaches a fixed point, $S$ (transitive). This fixed point is reached after no more than $\vert P\vert$ iterations.