Abramsky-Coecke Semantics

Stream: Quantum information

[James Squires]

Hello everyone. Heads up: I'm very new to Lean4.

Has anyone thought about or explored formalizing Abramsky-Coecke semantics for quantum protocols? It seems like a formal verification of AC semantics would be useful for categorical quantum circuits, and I think there is now a Lean software for string diagrams? I might be naive, but mathlib seems to have a lot of category theory to work with. Has anyone thought about this/explored this? Even just formalizing dagger closed compact categories would be interesting. I'd love to do this down the line as I get better at Lean4.

Thank you

[Alex Meiburg]

I think this would be fantastic! We've been talking a bit about doing category theoretic treatment of quantum mechanics (as a subcategory of Hilb with the CPTP maps, and so on), but I'm not a category theorist by any stretch of the imagination so I have a hard time to imagine beyond that

[Alex Meiburg]

I'd be happy to chat some time? But maybe we should loop in someone who also knows the category theory in Mathlib better

[James Squires]

It would definitely be wise to find someone who's confident with categories in mathlib! I'm personally still learning category theory, Lean, and quantum protocols (I'm an undergrad), so I don't know how much help I can be, but I'd be happy to contribute what I can.

[Rodolfo Soldati]

I've been interested in learning about categoric quantum mechanics too, I would be happy to brainstorm

[Rodolfo Soldati]

what's the string diagram software you refer to?

[Chris Henson]

Maybe docs#Mathlib.Tactic.Widget.stringDiagram is what was meant?

[James Squires]

This is indeed what I was referring to.

[James Squires]

I'm happy to hear that. Here are the best resources I've found so far:
This is the Rosetta Stone of CQM from what I can tell (Abramsky-Coecke 2004): https://arxiv.org/abs/quant-ph/0402130
Here's a more pedagogical text that I've been using to learn CQM: https://www.cs.ox.ac.uk/files/10510/notes.pdf

I'd appreciate if other people gave suggestions/input though, as I'm by no means an expert.

Rodolfo Soldati said:

I've been interested in learning about categoric quantum mechanics too, I would be happy to brainstorm