Source-linked AI summary
A Categorical Quantum Logic
Samson Abramsky, Ross Duncan
TL;DR
The paper addresses how to give logical syntax for strongly compact closed categories with biproducts while representing quantum processes. It develops a strongly normalising proof-net calculus that faithfully and fully represents the corresponding free category, with normalization supporting protocol reasoning. Its scope is limited when the generating category lacks additional multi-qubit structure, and scalar choices also constrain representable processes.
Problem
The paper addresses the need for explicit logical proof-net syntax capturing strongly compact closed categories with biproducts for quantum-process representation and reasoning.
Method
It develops a strongly normalising proof-net calculus whose formulas and proofs represent objects and arrows of the free strongly compact closed category with biproducts.
Results
The calculus is a faithful and fully complete representation, with confluent and terminating cut elimination and a faithfulness theorem relating equal denotations to β-equivalence.
Takeaways & Limitations
Proof-nets can represent and normalize quantum processes, supporting protocol reasoning and serving as a basis for quantum programming with entanglement-aware types.
Takeaways & Limitations
Without additional multi-qubit maps in the generating category, the free structure lacks operations such as controlled not and has limited expressivity; scalar choices also constrain processes.
Abstract
from arXiv · showhide
We define a strongly normalising proof-net calculus corresponding to the logic of strongly compact closed categories with biproducts. The calculus is a full and faithful representation of the free strongly compact closed category with biproducts on a given category with an involution. This syntax can be used to represent and reason about quantum processes.
1 Introduction
The paper develops proof-net syntax for the free strongly compact closed category with biproducts, connecting quantum structure, classical branching, and scalar amplitudes. It uses this syntax to represent, normalize, and reason about quantum protocols while identifying expressivity boundaries.
- For a category containing C2 with Pauli maps, the available preparations support entanglement swapping but not logic gate teleportation.
- The calculus faithfully and fully represents the free strongly compact closed category with biproducts generated by a category with an involution.
- Axiom links encode state preparations, cuts encode projections, and biproducts encode classical branching in proof-net representations of quantum processes.
- Cut-elimination removes measurements, preserves denotational equality, and can serve as a correctness proof for encoded quantum protocols.
- The framework is presented as a step toward a quantum programming language with an entanglement-aware type system.
2 An Example: Entanglement Swapping
The entanglement-swapping example models Bell-state preparation and Bell-basis projection as proof-net processes. Normalization computes the resulting state, while slices represent the measurement outcomes and classical information.
- Entanglement swapping lets Alice and Bob share a Bell state after Charlie performs a projective Bell-basis measurement on his two qubits.
- Bell states correspond to maps under the tensor–linear-map isomorphism, with Bell-basis elements related to Pauli maps up to global phase.
- Proof-nets represent states as processes, and normal proof-nets permit identifying a state with the process that prepares it.
- Normalizing the combined Bell-state preparations and projection computes the resulting state as the one coded by X.
- The four Bell-measurement outcomes are represented by distinct slices, while a gearstick records the classical outcome information.
3 Categorical Preliminaries
The categorical preliminaries define the compact-closed, biproduct, scalar, duality, and adjoint structures used by the proof-net calculus. FDHilb supplies the main quantum example, while Rel provides another model.
- Scalars are endomorphisms of the monoidal unit and act by scalar multiplication on morphisms.
- FDHilb uses the usual tensor product, complex scalars, dual spaces, and linear maps, while Rel is another strongly compact closed category with biproducts.
- Compact closure supplies names, conames, duals, and a categorical trace for morphisms.
- Biproducts combine products and coproducts, induce addition on hom-sets, and make composition bilinear; in FDHilb they are direct sums.
- Strong compact closure adds a covariant involutive action on duals, yielding an adjoint operation f† that preserves biproducts and is additive.
4 The Logic of SCCCBs
The logic uses formulas to represent objects and proofs to represent arrows of the free strongly compact closed category with biproducts. Its grammar reflects atoms, duals, tensor, biproduct, units, and cyclic structure.
- The logic’s formulas represent objects and its proofs represent arrows in the free strongly compact closed category with biproducts generated from a category with involution.
- The construction starts from a category with involution, whose objects become atomic formulas and whose arrows become non-logical axioms.
- The base-category involution lifts to the freely generated compact closed category, producing the required strongly compact closed structure.
- Formulas are generated from 0, I, atoms, duals, tensor, and biproduct, with restrictions enforcing strict behavior for the units.
- Cyclic structures and loops are included because compact closed categories require them in the syntax.
5 Proof-nets
The proof-net calculus gives a graphical, fully complete representation of the free strongly compact closed category with biproducts, with links encoding categorical structure and cut elimination providing normalization and semantic preservation.
- 5 Proof-nets: Proof-nets faithfully and fully completely represent the free strongly compact closed category with biproducts.The syntax represents arrows, while formulas represent objects of the generated category.
- 5 Proof-nets: Axiom links introduce atomic states, cuts encode projections, and biproduct links represent classical branching.Slices are finite oriented graphs of labelled links, and nets are finite multisets of slices sharing conclusions.
- 5 Proof-nets: Cut elimination is confluent and terminating, so every proof-net has a strongly normalising reduction process to normal forms.The only unreduced cuts occur in the specified atomic same-axiom case; interference cases are resolved using associativity or loop equivalence.
- 5 Proof-nets: Each reduction preserves denotation, allowing normalization to express protocol execution while retaining categorical equality.The semantics maps proof-nets to arrows, and the rewrite rules preserve those denotations.
- 5 Proof-nets: Faithfulness requires fixed conclusions, while full completeness ensures every arrow of the free category is denoted by some proof-net.Normal slices are characterized by connective choices, atom pairings, a functor into the ground category, and loop data.
6 Further Work
The paper identifies limited expressivity when freely generating over a category without additional multi-qubit structure and proposes extending the construction with scalar parameters.
- 6 Further Work: Without additional structure on the base category, the free model lacks controlled-not and other multi-qubit operations, limiting expressivity.The authors propose freely generating over a category with a given symmetric monoidal structure as a next step.
- 6 Further Work: Choosing a semiring of scalars can tune representable quantum processes and potentially support concrete probabilities and other quantitative information.The authors note that Rel lacks enough scalars to represent teleportation and defer this development to future work.
A Proof of full completeness
The full-completeness proof combines matrix constructions, normal forms, strongly compact closed structure, and proof-net construction to represent every arrow of the free category.
- A Proof of full completeness: The matrix construction lifts to strongly compact closed categories, providing the categorical factorization used in the completeness argument.The factorization is stated as F = B ◦FSCC and is used as a structural basis for the proof.
- A Proof of full completeness: Every functor built from tensors and biproducts is naturally isomorphic to a normal functor by distributivity.The construction proceeds recursively over biproduct and tensor cases.
- A Proof of full completeness: Arrows between normal functors are reconstructed recursively by decomposing biproduct matrices and reducing components to arrows of the free strongly compact closed category.The proof handles biproducts in three cases and uses Proposition 24 to place nonzero components in the strongly compact closed subcategory.
- A Proof of full completeness: The free strongly compact closed category inherits an involution and is itself strongly compact closed when the generating category has an involutive functor.The involution is extended using the Kelly–Laplaza description of morphisms.
- A Proof of full completeness: Each arrow of the free strongly compact closed category is represented by a proof-net whose axiom links encode labelled involutions and whose loop data become closed axiom links.Kelly–Laplaza data provide the proof-net construction, while tensor links connect the formula subcomponents.
- A Proof of full completeness: Proof-nets for component arrows can be combined through biproduct structure to construct a proof-net denoting their biproduct arrow.The construction combines slices for each component and proves JπK = ⌜f1 ⊕f2⌝; Figure 3 illustrates the construction for lemma 29.