University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > New reasoning techniques for monoidal algebras

New reasoning techniques for monoidal algebras

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jonathan Hayman.

In this talk, I will discuss the interaction of two prominent tools one uses to study algebraic structures in monoidal categories: PRO Ps and string diagram rewriting. PRO Ps are small symmetric monoidal categories which totally capture a certain algebraic structure (they are the “walking X”), but their application is typically limited to structures that we understand well. On the other hand, rewriting with string diagrams allows one to immediately get a handle on even those structures which have very complicated presentations, but it provides little in the way of powerful “meta-rules” describing the global behaviour of the structure.

To bridge this gap, one needs to find more sophisticated ways of expressing and reasoning about infinite families of diagrams. In this talk, I will introduce ”!-box notation”, which gives a particularly simple means of doing just that. While the expressive power of !-boxes is fairly limited, when combined with the notions of !-graph rewriting and induction, one can state and prove a surprisingly rich family of theorems, and sometimes even recapture the kind of global behaviour we would expect from a PROP -based approach. I will illustrate this by giving a purely graphical proof of a recent representation theorem for interacting bialgebras, and show this theorem in action in the graphical proof assistant Quantomatic.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity