A Categorical Model for a Quantum Circuit Description Language
A Categorical Model for a Quantum Circuit Description Language
Rios and Selinger give Proto-Quipper-M a categorical model of parameters and state, with type safety, soundness, and adequacy results.
Paper information (2018, EPTCS 266, pp. 164–178; preprint: 2017) — Francisco Rios and Peter Selinger. DOI; arXiv:1706.02630
Work
The paper formalizes a small but useful fragment of Quipper, Proto-Quipper-M. It distinguishes parameters known during circuit generation from state known only during circuit execution, and describes families of morphisms in arbitrary symmetric monoidal categories, of which quantum circuits are one instance. The authors build a categorical model first, then define the language and its operational and denotational semantics.
Contributions
- A categorical model of parameters and state for Proto-Quipper-M.
- A type-safe circuit-description language with operational and denotational semantics.
- Type-safety, soundness, and adequacy results connecting the language and model.
- A generalization from quantum circuits to families of morphisms in symmetric monoidal categories.
Limits
Proto-Quipper-M is a core fragment of Quipper, not a complete industrial language or backend compiler. The categorical model gives semantic guarantees but does not solve noise, gate sets, device connectivity, resource costs, or all engineering problems of a higher-order host language. Safety and adequacy depend on the chosen model and language assumptions.
Connections
The paper supplies a semantic core for Quipper and, like QWIRE, studies an embeddable circuit language with type safety. Compared with QML and Dagger Compact Closed Categories and Completely Positive Maps, it makes the distinction between circuit-generation parameters and execution-time state explicit.
Original paper
Francisco Rios and Peter Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266, 164–178 (2018), DOI: 10.4204/EPTCS.266.11. arXiv:1706.02630