Exploring the Geometry of Computation & String-Diagram Programming in Monoidal Computers 🖥️

Talk given on November 3, 2021 on Zoom.


Abstract: A monoidal computer is a monoidal category with a distinguished type carrying the structure of a single-instruction programming language. The instruction would be written as "run", but it is usually drawn as a string diagram. Equivalently, the monoidal computer structure can be viewed as a typed lambda-calculus without lambda abstraction, even implicit. Any Turing complete programming language, including Turing machines and partial recursive functions, gives rise to a monoidal computer. We have thus added yet another item to the Church-Turing list of models of computation. It differs from other models by its categoricity. While the other Church-Turing models can be programmed to simulate each other in many different ways, and each interprets even itself in infinitely many non-isomorphic ways, the structure of a monoidal computer is unique up to isomorphism. A monoidal category can be a monoidal computer in at most one way, just like it can be closed in at most one way, up to isomorphism. In other words, being a monoidal computer is a property, not structure. Computability is thus a categorical property, like completeness. This opens an alley towards an abstract treatment of parametrized complexity, one-way and trapdoor functions on one hand, and of algorithmic learning in the other.