See the previous post for Weeks 3 and 4.
This week I’ve been mostly doing background reading. This post is mostly a summary of what I learned.
In short, unification is the process of finding substitutions of variables within two terms two terms to make them identical. For example, if we have the expressions and , the substitution is a unifier, since applying the substitution to both expressions makes gives us the identical expression of . While this particular substitution includes variables from both expressions, we’re mostly interested in rules involving substitutions of variables from just one expression (a case of unification known as matching). Several well-known algorithms for unification already exist.
Unification in SymPy
SymPy also has an implementation of a unification algorithm that is able to take the commutativity of operations into account. Suppose we wanted to unify the matrix expressions
. This is essentially the problem of finding a substitution that makes these two expressions equal. Using the
sympy.unify.usympy module, we can discover what this substitution is:
We’ve reduced this to a matching problem in which the variables are specified only in
e2. What’s important to note here is that the matching rule within
e2 we specified (
) was a compound expression. This is something that is currently not possible for non-commutative expressions (such as matrix multiplication) using SymPy’s
unify allows use to express substitution rules that are able to match across sub-expressions in matrix multiplication.
Through unification, we can express substitution rules for optimization as a simple term-rewriting rule. In my previous blog post, I mentioned rewriting the matrix multiplication
as a solving operation of
MatSolve(A, x) under certain assumptions. The actual implementation is restricted to cases where both the
A and the
x are matrix symbols, and the optimization can’t identify cases where either the
A or the
x is a compound expression. With unification, we can identify the same pattern in more complex subexpressions. If we’re given the matrix expression
, a unification based transformer can produce
MatSolve(AB, x), provided that the shapes of the matrices match the given rule.
I also looked into generating C and Fortran code from SymPy matrix expressions. For the purposes of code generation, SymPy has a relatively new
array_utils module. The AST nodes in this module express generalizations of operations on matrices, which require a bit of background in tensors.
Many array operations (including matrix multiplication) involve contraction along an axis. Contractions are a combination of multiplication and summation along certain axis of a tensor1. In assigning the matrix multiplication to the matrix , we can explicitly write the summations (using subscripts for indexing matrix elements) as
is contracted, as it is shared between both
, and describing this summation operation as a whole boils down to which indices are shared between the matrices. This is essentially what the
array_utils classes do. This is what happens when we use
array_utils to convert the matrix multiplication to an equivalent contraction operation:
We’re given a new
CodegenArrayContraction object that stores, along with the variables
B, tuples of integers representing contractions along certain indices. Here, the
(1, 2) means that the variable at index 1 and index 2 (indices start at 0) are shared. We can confirm this by looking at the above summation, since both the second and third indices out of all indices that appear in the expression are
For next week, I’ll try to re-implement the rewriting optimization in terms of
unify. This will both make it easier to express rules and extend to sub-expressions as well. I’ll also start with implementing additional printers for the C and Fortran printers. The printer will probably just print naive
for loops to keep things simple (and it would probaly be better to use something like Theano for highly optimized code).
For our purposes, we can think of tensors as just -dimensional arrays. Most of my reading on tensors was Justin C. Feng’s The Poor Man’s Introduction to Tensors.↩