Applying Quantitative Semantics to Higher-Order Quantum Computing

Paper information (2014, POPL; preprint: 2013) — Michele Pagani, Peter Selinger, and Benoît Valiron. arXiv:1311.2290

Work

The paper addresses denotational semantics for higher-order quantum computation while retaining recursion, infinite data types, and entanglement. It uses constructions from quantitative semantics and linear logic to model a quantum lambda calculus, responding to earlier approaches that either restricted the language to a small finitary fragment or lost important quantum features.

Contributions

• A denotational semantics for higher-order quantum lambda calculus with recursion and infinite data types.
• An application of quantitative linear-logic constructions to quantum computation.
• A higher-order semantic model that retains the ability to represent quantum phenomena such as entanglement.
• A setting in which higher-order functions, recursion, and quantum resources can be discussed together.

Limits

The semantics is a theoretical model, not a complete compiler or hardware implementation for a higher-order quantum language. Recursion, infinite data, and entanglement require explicit domains, metrics, and approximation interpretations; existence of a semantics does not prove termination, efficiency, numerical accuracy, or device behavior.

Connections

The paper continues the functional quantum-language line of A Lambda Calculus for Quantum Computation with Classical Control and QML, and addresses the recursive-semantic concerns of QPL. Compared with Quantum Loop Programs, it focuses on higher-order functions and infinite data; compared with Dagger Compact Closed Categories and Completely Positive Maps, it treats higher-order recursive quantum programs.

Original paper

Michele Pagani, Peter Selinger, and Benoît Valiron, Applying Quantitative Semantics to Higher-Order Quantum Computing, in POPL 2014. arXiv:1311.2290