This is a crosspost from my personal blog
Suppose your name is x and you have a very important state machine N_x : S_x \times \Sigma \to \mathcal{P}(S_x) that you cherish with all your heart. Because you love this state machine so much, you don’t want it to malfunction and you have a subset P \subseteq S_x which you consider to be safe. If your state machine ever leaves this safe space you are in big trouble so you ask the following question. If you start in some subset I \subseteq P will your state machine N_x ever leave P? In math, you ask if
\mu (\blacksquare(-) \cup I) \subseteq P
where \mu is the least fixed point and \blacksquare(-) indicates the next-time operator of the cherished state machine (c.f. Def. 2 of this post).
In a perfect world you could use these definitions to ensure safety using the formula
\mu (\blacksquare(-) \cup I) = \bigcup_{n=0}^{\infty} (\blacksquare ( - ) \cup I)^n
or at least check safety up to an arbitrary time-step n by computing this infinite union one step at a time.
Unfortunately there is a big problem with this method! Your state machine does not exist in isolation. You have a friend whose name is y with their own state machine N_y : S_y \times \Sigma \to \mathcal{P} (S_y). y has the personal freedom to run their state machine how they like but there are functions
N_{xy} : S_x \times \Sigma \to \mathcal{P}(S_y) and N_{yx} : S_y \times \Sigma \to \mathcal{P}(S_x)
which allow states of your friend’s machine to change the states of your own and vice-versa. Making matters worse, there is a whole graph G whose vertices are your friends and whose edges indicate that the corresponding state machines may effect each other. How can you be expected to ensure safety under these conditions?
Don’t worry, category theory comes to the rescue. We can:
-
Define a functor which encodes the state machines of you and you and your friends as well as the connections between them.
-
Take the Grothendieck construction to get a recipe to ensure local safety in your global context by keeping track of the possible paths between you and your friends.
I’ve already done 1 in my previous post: How to stay safe when you and your friends share a giant computer (Part 1: we are a functor). Next time I’ll show you how to do 2. Thanks for reading!