Strengthening agent shapes

[kris-brown]

In the wiring diagram formalism for agent-based programs, it is possible to weaken an agent shape $A$ (i.e. the guarantee of having a distinguished map $A\rightarrow X$ into some state of the world $X$) to some agent shape $B$ by precomposing the distinguished $A$ with a map $A \leftarrow B$.

If we want to strengthen the agent shape via a map $A\rightarrow B$, AlgebraicRewriting currently has a Strengthen box but this works by pushout: it adds to the world in order to guarantee that given one has a distinguished $A$ that one will get a distinguished $B$.

What we need is a way to strengthen a distinguished $A$ to a distinguished $B$ via $f:A\rightarrow B$ without mutating the world state. There are two problems with this: 1.) there may be no way of extending $A\rightarrow X$ along $f$, 2.) there might be many ways of doing so. The first case is addressed by having a "failure" output wire also typed $A$. The second case can be addressed by making a uniformly random choice. Call the box which does this StrengthenChoice.

This feature is very common and has historically been modeled via abuse of the Query box: that box is meant to be used by running some algorithm for every such match of a certain shape, with the subroutine feeding back into a special input port which signals to switch to the next match. We abuse this by never closing the loop: enter the query box, pick an arbitrary match (which could strengthen the agent shape) and then just continue along, never to loop back. While this has the same semantics to StrengthenChoice, it has different performance characteristics and is overkill (e.g. it's nice when all the boxes in a rewrite program are stateless).

To motivate this with a particular example inspired by Nate Osgood and Xiaoyan Li, consider modeling contract rate semantics:

We come in with a distinguished infected person. We pick another person at random (not knowing whether they are infected or not). We then check whether they are susceptible or not (if they are, this information gets promoted to the "type level", i.e. the agent shape records that if we are in the top wire of the second box then we are guaranteed to have a distinguished infected and distinguished susceptible person). Then we can flip a biased coin given this choice of arbitrary other person who happens to be susceptible and if heads execute an infection event.