A Functional Quantum Programming Language
A Functional Quantum Programming Language
Altenkirch and Grattage propose QML, combining finite types, linear logic, and categorical semantics for reversible and irreversible quantum computation.
Paper information (formal version: 2005, LICS, pp. 249–258; preprint: 2004) — Thorsten Altenkirch and Jonathan Grattage. DOI; arXiv:quant-ph/0409065
Work
The paper introduces QML, a functional language for quantum computation on finite types. Programs are interpreted as morphisms in a category of finite quantum computations, so the semantics covers both reversible quantum gates and irreversible computations such as measurement. QML uses first-order strict linear logic, making weakening explicit as a resource operation; strict programs are free from decoherence and can preserve superpositions and entanglement.
Contributions
- A QML design combining functional syntax, quantum data, and finite types.
- A categorical semantics for reversible and irreversible computations realizable by quantum gates.
- A strict linear-logic discipline that distinguishes quantum resources that may be used, discarded, or must be preserved.
- An account of how decoherence-free strict programs preserve superposition and entanglement.
Limits
QML focuses on finite types and an idealized quantum-computation model; its categorical semantics is not a compiler or noise model for a particular device. Linear rules constrain resource use but do not by themselves prove algorithmic complexity, numerical accuracy, or hardware correctness. The implementation cost of irreversible operations, measurement, and disposal requires separate analysis.
Connections
The paper develops the typed-language direction of QPL through a functional and categorical lens, and shares the resource motivation of the quantum lambda calculus. Compared with A Lambda Calculus for Quantum Computation with Classical Control, QML emphasizes finite types, reversibility, and strict programs. Its compositional semantics can also be compared with A Categorical Semantics of Quantum Protocols.
Original paper
Thorsten Altenkirch and Jonathan Grattage, A Functional Quantum Programming Language, in LICS 2005, pp. 249–258, DOI: 10.1109/LICS.2005.1. arXiv:quant-ph/0409065