How to stay safe when you and your friends share a giant computer (Part 1: we are a functor)

Suppose that you and your friends all work together to run a giant computer. Suppose that this computer is modeled by an NFA.

Def: A non-deterministic finite automaton is a function $ \tau : S \times A \to \mathcal{P}(S)$ where S is the set of states, A is the input alphabet, and $ \mathcal{P}$ is the powerset operator.

Let's get specific. Let F be the set of these friends and let $ H: X \times A \to \mathcal{P}(X)$ be the giant NFA that you are collectively running. Each friend $ x \in F$ has access only to a local set of states called D(x). The problem with dividing H up in this way is that the local states are not self contained: a state $ a \in D(x)$ may transition under H to a state that you no longer have access to (say $ b \in D(y))$. In this case we say that there is a two-legged NFA connecting x's states to y's.

Def 1: A two-legged NFA from S to S' is a function $ S \times A \to \mathcal{P}(S')$.

Now suppose that you and your friends are all very concerned about safety. You have a set of possible inital states $ I \subseteq X$ and a set $ P \subseteq X$ which represents your "safe space". If your automaton ever takes a state from I and brings it outside P, then there is a nuclear meltdown (we want to avoid this). We may formalize this problem as follows:

Def 2: Given a transition system $ H : X \times A \to \mathcal{P}(X)$ there is a monotone operator

$ \hat{H} : \mathcal{P}(X) \to \mathcal{P}(X)$ given by

$ \hat{H} (B) = \{ y \in S \, | \, \text{ there exists } a \in A, x \in B \text{ with } y \in H(x, a) \}$

So an element is contained in $ \hat{H}(B)$ if it is a successor of an element of B.

Def 3: The safety problem for H asks: given subsets $ I, P \subseteq X$, is

$ \mu (\hat{H}\cup I) \subseteq P $

where $ \mu(\hat{H} \cup I) = \bigcup_{n=0}^{\infty} (\hat{H}\cup I)^n (\phi)$ is the least fixed point of the operator $ \hat{H}(-) \cup I$.

Let's return to the giant computer that you and you're friends are running. We can solve the safety problem for H compositionally by using a functor

$ E : FG \to \mathsf{Poset}$

Let's unpack:

• G is a directed graph whose vertex set is your set of friends.
• There is an edge in G from friend x to friend y if there exists $ a \in D(x)$ and $ b \in D(y)$ such that b is a successor of a under H. In other words, there's an edge from x to y if D(x) and D(y) are connected in H.
• $ \mathsf{Poset}$ is the category of posets and monotone functions between them.

A functor from a free category is uniquely defined by its image on generating morphisms (in this case the edges of G). We will define these edges and their images as follows:

• A vertex x of G is sent to $ E(x) = \mathcal{P}(D(x))$ where $ D(x)$ is the set of states that friend D has access to.
• For each edge $ e : x \to y$, the big automaton restricts to a two-legged automaton $ H|_{e} : D(x) \times A \to \mathcal{P}(D(y))$ given by precomposing with the inclusions $ D(x), D(y) \hookrightarrow S$. The functor E should map e to a monotone operator $ E(e): \mathcal{P}(D(x)) \to \mathcal{P}(D(y))$. This is defined similarly to Definition 2.

Def 4: Given a two-legged transition system $ \tau : D(x) \times A \to \mathcal{P}(D(y))$ there is a monotone operator $ \hat{\tau} : \mathcal{P}(D(x)) \to \mathcal{P}(D(y))$ given by

$ \hat{\tau}( B) = \{b \in D(y) | \text{ there exists } a \in B, \, l \in A \text{ where }b \in \tau(a,l)\}$

We define $ E$ by $ E(e) = \hat{\tau}$.

This defines the functor. Note that it captures all the relevant data of our big computer H and how it is decomposed among our friends. What is the point of modelling this situation with a functor? The point is that we can take the Grothendieck construction of this functor. In the next post, I'll explain how this Grothendieck construction gives a compositional solution to the safety problem. Stay tuned!