Algebraic Theory of Concurrency

The last thing I posted about a year ago was the beginning of work I've subsequently pursued to a concrete result. That result is an algebraic theory of concurrency, which I can use to construct a logic, and from that, a type system, both of which can reason about concurrency. There's a very strong connection to quantum theory in all this, which I'll discuss later on.

For now, I'll give an overview of the algebra. What I'm describing represents some of what is, and some of the directions I'd like to take things, so it's not necessarily mathematically rigorous. This is meant to introduce the basics of the algebra; the complete equational theory is in the tech report I wrote.

First, we need to describe states. I do this in a manner that is compatible with linear algebra. A state space is a collection of distinct elements called "states", which are closed under scalar multiplication by identity and zero. We write states using notation similar to Dirac's notation: | s > and < s |. The inner product < s | s' > is a mapping from two states to identity or zero (which I write using id and ⊥ instead of 1 and 0) such that < s | s' > = id iff s = s' and ⊥ otherwise. We can describe any memory state over a fixed address space by taking the elements of the state space to be maps from addresses to values. Also, note that any inner-product vector space can also give rise to a state space.

For any two state spaces S and T, there exists a product space S ⊗ T. We write elements of the product space using the tensor product s ⊗ t. This allows us to reason about disjoint portions of a state.

Actions represent the single, atomic actions that make up concurrent programs (such as atomic reads, writes, and more complex primitives). The algebra of actions gives us a way to sequentially compose actions into larger actions. We will use this to reason about how processes behave when running in isolation. An action is a set of strict, (Scott-)continuous functions from a given state space onto itself. I'll discuss the constructors for actions briefly.

The most basic action is the outer product, | s >< s' |, which represents a mapping some state t to the state < t | s > s'. Note that if t = s, then the result will be s', otherwise, it will be ⊥. As with quantum mechanics, we can thus reason about the composition of outer products using inner products in a straightforward manner. For example | s >< s' | composed with | t >< t ' | is | s >< s' | t >< t '|, which we can reduce by evaluating < s' | t >.

There exists an identity action id which maps each state onto itself. We will be able to give a precise definition of this later on. The empty function space is represented by ⊥ (this is distinct from the scalar ⊥, but scalar multiplication of any action by ⊥ yields the ⊥ action). The total function space is represented by ⊤.

As with states, actions are closed under tensor products. Tensor products distribute with respect to outer products as one would expect, ie. | s ⊗ t >< s' ⊗ t' | = | s >< s' | ⊗ | t >< t' |. Tensor products also have the identity property with id, ie. A ⊗ id = A.

We can represent branching and "intelligent" nondeterminism using the pointwise join of the function spaces represented by two actions. We write this as A ⊔ B. Not surprisingly, A ⊔ ⊥ = A and A ⊔ ⊤ = ⊤. The pointwise meet of two function spaces models the behavior one sees in real parallelism (or what theorists call "alternation), where if any possibility can fail, then the system can fail. We write this as A ⊓ B. Not surprisingly, A ⊓ ⊥ = ⊥, and A ⊓ ⊤ = A. Both meet and join distribute over eachother, and both distribute with tensor products. The rules for distribution with outer products are more intricate. In essence, we have that (A ⊔ B)(A' ⊓ B') = (A ⊓ B)(A' ⊔ B') = (AA' ⊔ AB' ) ⊓ (BA' ⊔ BB').

Lastly, it is often useful to talk about the differences of actions. We can model these as set differences, and the algebraic rules are exactly those from the algebra of sets (with meet and join substituted for intersection and union).

Finally, we model actual concurrent programs with processes. The main purpose of processes is to reason about how actions interleave, and to permit some notion of reasoning about isolation of portions of state. For starters, every action is also a process. There are also constructors for processes that correspond to the constructors for actions. There are meet and join constructors, tensor products, and a sequence constructor ⋅ (which corresponds to composition). These are not the same as the operators on actions, however; we cannot reduce processes by the action rules unless we know the state on which it operates to be isolated.

We represent this notion of isolation with closure. The closure operator is written as Cl[P] (normally I write a superscript denoting the state space being closed over). Closure maps processes to actions by substituting corresponding constructors. We can think of the process versions of the constructors as "frozen".

We can model recursion with recursively-defined processes. More importantly, we can model real concurrency with a derived operator ⋈, which is defined as (P1 ⋅ P2) ⋈ P = P ⋈ (P1 ⋅ P2) = ((P1 ⋈ P) ⋅ P2) ⊓ (P1 ⋅ (P ⋈ P2)) and A ⋈ A' = (A ⋅ A') ⊓ (A' ⋅ A). In other words, ⋈ represents all possible interleavings.

This finally gets us an acceptable notion of bisimilarity. Formally, we write it as follows P1 ≈ P2 iff ∀P. Cl[P1 ⋈ P] = Cl[P2 ⋈ P]. In other words, P1 is bisimilar to P2 if it behaves the same when running beside all other possible processes.

It is possible to formulate a similar reasoning system in a higher-order predicate logic (such as ECC), which can then be incorporated into a type system to allow reasoning about concurrency. I will discuss this later.