Events / Oxford Seminar
Sweedler Theory for Systems
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.