String diagrams, a topological account of proofs and programs
Paul-André Melliès ( Laboratoire PPS, Paris VIII )
- 14:00 18th February 2010 ( week 5, Hilary Term 2010 )Lecture Theatre **A**, Computing Laboratory
In this introductory talk, I will explain some of the functorial ideas which recently appeared in the field of logic and programming language semantics. More specifically, I will explain how to see game semantics as a variant of functorial knot theory, where the ribbon category of knots is replaced by a monoidal category of formulas and proofs between them. By the wizardry of string diagrams in 3-categories, this category may be seen alternatively as a category of games and interactive strategies between them. Interestingly, this game construction defines the free symmetric monoidal category equipped with a logical duality. From this follows the idea of classifying the various notions of duality in monoidal categories, the usual duality of ribbon categories being one of them. For the fun of it, I will also describe how to compute the free monoid in that category of games, using a left Kan extension, and relate this construction to the ability to define recursive calls in programming languages. Finally, I will draw a beautiful connection between logic and algebra, first noticed by Ross Street, and explain in what sense this category of games may be seen as a lax notion of Frobenius algebra. Amusingly, this observation leads to a lax version of two-dimensional cobordism, where particles are replaced by game boards.
Share this:
