Sweedler Theory for Systems
Events / Oxford Seminar
Starting from theories of interaction, or Application Programming Interfaces with laws, we ask how one such theory, T, can be implemented inside another, R, by a stateful mechanism. Described via monoids in a duoidal setting, Sweedler theory supplies a universal object, M(T, R), whose coalgebras are precisely such mechanisms. These are known as runners. Our central systems-theoretic proposal is to organise theories, direct interpretations, stateful runners, and transformations of runners into a double-categorical architecture Run(D), relative to a given duoidal Sweedler setting D. Tight maps say how operation languages are reinterpreted in each other. Loose maps say how one operation language is realised by a stateful mechanism in another. Run(D) affords us a rich structure to investigate systems composition and behaviour. Varying D allows us to cover a wide range of circumstances, such as systems with certificates, costed, smooth, probabilistic and higher-dimensional systems.