Eigenstuff, diagrammatically

Last Tuesday, September 5 2017, I gave a tutorial on Graphical Linear Algebra at CONCUR 2017 the 28th International Conference on Concurrency Theory, which this year was held in Berlin.

I have a personal history with CONCUR. It was the first comp sci conference I attended (CONCUR 2001, Aalborg, Denmark). I gave my first comp sci talk the year after at a satellite event of CONCUR 2002 (Brno, Czech Republic).  Another year passed and I had a paper accepted at CONCUR 2003 (Marseille, France), even if it was mostly my brilliant coauthor’s Bartek Klin‘s  work. It was, and remains, a community with a particular way of looking at the world, and it has definitely shaped my own thinking.

So it was a real honour for me to be invited to give a tutorial at CONCUR 2017. I had a problem though: how to talk about the stuff on this blog to a community in which linear algebra is not, per se, a topic of interest.


One of the main research threads of CONCUR is process algebra. Process algebra is the study of idealised programming languages. Idealised here means two things: first, one strips away many features that would need to be included in a real-world programming language (I/O, fancy control flow, etc.) and leaves only a few fundamental ways of expressing some computational primitives, say synchronising communication, sequencing and recursion (CCS, the Calculus of Communicating Systems), or asynchronous communication with name passing, sequencing and recursion (Asynchronous π-calculus).

The basic idea is that stripping away irrelevant constructs makes a language more logically/mathematically tractable: a process algebra is thus the distillation of some computationally-inspired artefacts into a mathematically rigorous playground, allowing for the study of the expressivity of those primitives that remain and the interesting ways they interact, without interference from extraneous elements. An analogy can be made with chemistry: in order to study some fundamental reaction between compounds, one works with pure solutions in order to obtain meaningful results. That’s the basic, motivating idea, in any case.

The second meaning of the word idealised is that – unlike ordinary programming languages – process algebras allow you to write specifications as well as implementationsI won’t attempt to give a formal definition of what these words mean, but I’ll try to give some intuition.

An implementation has to be able to run: at some level of abstraction it must be able to compute outputs from inputs on some notion of computing machine. The mathematical analogy is with (total) functions X → Y. A function must be able to deal with every element of X and, given some x ∈ X, unambiguously evaluate to an element f(x) of Y.

On the other hand, a specification may be partial: it can be undefined on some inputs, where there isn’t any proscribed behaviour and the details are left to the programmer. Similarly, it may be the case that for some inputs we allow several possible results without giving any way of determining which one is preferable or how to arrive at any one particular output – this is known as non-determinism. The analogy here is with a relation R from X to Y. Since a relation is simply a subset of X×Y, it does not need to be total (i.e. there may be some x ∈ X for which there is no y ∈ Y such that (x,y) ∈ R) and it does not need to be single-valued (there may be some x ∈ X and two different elements of Y, say y1 and y2, with y1≠y2 such that both (x,y1) and (x,y2) are in R).

Graphical linear algebra feels like a specification language for linear algebra. Once you start using it, matrices feel like low-level implementations; the diagrammatic language gives you a higher-level way of expressing yourself. Of course, the equational theory means that we can “compile” down to the low-level stuff. A nice example of this idea in action is the diagrammatic way of dealing with the concepts of an eigenstuff (eigenspaces, eigenvalues, eigenvectors, eigenbasis) and spectral decomposition.


A linear transformation, defined by some n×n matrix A, has an eigenspace E with eigenvalue λ when for each vector vE, we have

Av = λv.

By isolating an eigenspace/eigenvalue pair (E, λ), we are saying that A has a particularly simple description on the sub-domain defined by E, where it is just scalar multiplication by λ. We can say this graphically as follows:

eigenspace

We will use the above equation as a diagrammatic definition of the concept of an eigenspace, eigenvalue pair (E, λ). It’s an important equality, so let’s go through the individual bits in detail.

E is a diagram from n to 0, therefore, it defines a subspace of Qn. The diagram on the left is the linear relation that results from restricting the domain of A to E. Using traditional notation, the left-hand side is the linear relation

{ (e, Ae) | eE }

and the right-hand side is the linear relation

{ (e, λe) | eE }. 

The above diagrammatic equation thus says precisely that A, when restricted to E, is the same as simply multiplying by λ.


 

Suppose that we can find a decomposition of the entire domain (Qn) of A into eigenspaces. That is, suppose we have E1, …, Ek such that

decomp

and for each Ei, we have an eigenvalue λi, that is

eigenvalue

Such a collection (Ei, λi) is called the spectral decomposition of A. Given a spectral decomposition, we can write A as a sum of the constituent behaviours, in the following sense:

spectral.gif

It is useful to think of the right hand side of the equation above as a specification. Indeed, we are defining a linear transformation by declaring what it should do on each of its eigenspaces. Continuing this analogy, the left hand side is a matrix, an implementation of the specification.

Here’s a proof of the above equality, using diagrammatic reasoning. In the second step we use the third-to-last diagram above, which says that the entire domain of A can be decomposed as a sum of eigenspaces. The third step is a simple exercise in graphical linear algebra, to which we will return below. In the fourth step we pull A across the addition, and then rearrange the diagram. In the last step, we simply use the diagrammatic defining equation of eigenspaces/eigenvalues.

proof.gif

To dot all the i’s and cross all the t’s, let’s come back to the third equation in the above derivation. It relies on the following lemma

mixedassociativity.gif

which can be proved by induction, starting with the following equality as the base case.

base.gif

I’ll leave this last bit as a fun exercise.


 

Let’s go through a concrete computation that demonstrates how to turn a linear algebra specification into a matrix implementation.

So suppose we want to construct a function that acts on the following two subspaces

subspace1

subspace2

by multiplying by 5 and -1, respectively. In more traditional set-theory language, these subspaces are { (x,y) | x,y ∈ Q, x+2y = 0 } and { (a, 2a) | a ∈ }. You can read off the set theoretical descriptions directly from the diagrams by reading the first from left to right, and the second from right to left, using our standard intuitions for the meaning of the white and black dots.

Notice that the two diagrams are the colour-inverse of one another, and therefore they are orthogonal as subspaces. In general, for an implementation to result in a matrix specification, we don’t necessarily need to start with mutually orthogonal subspaces: it suffices that they add up to give the whole domain and, pairwise, have a trivial intersection, i.e.

pointwiseint.gif

whenever i≠j.

Since our chosen eigenvalues are 5 and -1, the first eigenspace/eigenvalue combination lets us write down the first part of the specification.

firstcomp

The second is then

secondcomp

Summing up the two components gives us the entire specification:

speca

We should now be able to compile this thing to a matrix. Let’s start by getting the middle bit to be all black.

spec.gif

Now we can move the numbers out of the way

spec3

We are left with two connected black networks in the middle. Here we can use the spider theorem to simplify further.

spec4

The diagram above thus consists of a “backwards” matrix

mat1

followed by the matrix

mat2

If this is unclear, take another look at the episode that describes the connection between diagrams and matrices.

Now a “backwards” matrix, going from right to left, is the same thing as its inverse going from left to right, so the entire thing can be written as:

matrixform

We can calculate the inverse in any way we like, including using graphical linear algebra. The final result of inverting and multiplying is

res

and this is the implementation of our original spec.


 

Let’s use diagrammatic reasoning to work derive the standard “textbook formula” for doing this kind of thing with matrices.

Suppose that A is an n×n matrix, and that we can find an eigenbasis: a basis of its domain Qn that consists of n eigenvectors e1, e2, …, en, each ei with eigenvalue λi. Using the diagrammatic definition, this means simply that:

eigenvector

Here it’s useful to put some numbers on the wires, to make clear that each eigenvector ei is a column vector, i.e. a diagram from 1 to n.

Now let’s add up all of the components to get the specification for A:

speceigenvector

We can now use diagrammatic reasoning to get this thing into something more familiar:

derivation

The last diagram can be written in matrix form. Let E be the n×n matrix with e1,e2, …, en as its column vectors. Then the first part of the final diagram above is E backwards, followed by a diagonal matrix D with the λ1, λ2, …, λn on its diagonal, finally followed by E. We therefore get the standard textbook change-of-basis formula:
formula


 

This is the story I used in order to explain graphical linear algebra to people from the CONCUR community: we can think of the diagrammatic language as a specification language for linear algebra. If we pursue this analogy, as I did above, it is natural to think of matrices as implementations, implementing simple linear programs (linear transformations) on the “abstract machine” where the states come from a finite-dimensional vector space.

But graphical linear algebra is more expressive than matrices: we can give partial specifications of behaviour, as demonstrated with the diagrammatic definition of the eigenspaces/eigenvalues, as well as non-deterministic specifications. Non-determinism gives rise to the idea of refinement: how to go from a non-deterministic specification to a (non-unique) implementation that  does the job. I had a paper about this at CONCUR this year, presented by my PhD student Joshua Holland (who, by the way, applied for his PhD last year using the link on this blog!) and co-authored with Filippo Bonchi and Dusko Pavlovic. I will write more about non-determinism and refinement soon.


 

Last week was particularly busy. After my CONCUR tutorial in Berlin, I flew back to the UK for the inaugural STRING meeting, the 1st Workshop on String Diagrams in Computation, Logic, and Physics, which was held on Friday and Saturday (8-9 September 2017), co-located with the HDRA workshop on higher-dimensional rewriting and applications. The meeting was held in the upstairs gig area of the Jericho Tavern in Oxford.

You never know how much interest you’ll get in a brand new event, but I have to say that  it exceeded my expectations: it was a full house, with more than 60 people in the audience, enjoying an exciting programme full of great talks. I loved it.

IMG_1712

Paul-André Mèllies giving his invited talk.

IMG_1717

The back of the room, the Jericho was totally packed!

It was also really fun to meet a few blog readers who decided to attend. Some told me to get off my ass and write more articles. It’s definitely given me some extra motivation, so watch this space!

If you enjoyed this article, please subscribe to get email updates when new articles are published. You will find a subscription link at the bottom of this page.

Advertisements

One thought on “Eigenstuff, diagrammatically

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s