dorsal/arxiv
View SchemaA Lambda Calculus for Quantum Computation
| Authors | Andre van Tonder |
|---|---|
| Categories | |
| ArXiv ID | quant-ph/0307150 |
| URL | https://arxiv.org/abs/quant-ph/0307150 |
| DOI | 10.1137/S0097539703432165 |
| Journal | SIAM J.Comput. 33 (2004) 1109-1135 |
Abstract
The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine, and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of Linear Logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.
{
"annotation_id": "a43a29a2-a5ce-478a-ac88-861b0f2ef3ce",
"date_created": "2026-03-02T18:01:59.755000Z",
"date_modified": "2026-03-02T18:01:59.755000Z",
"file_hash": "bd2a00111886127e095ffd1e12aec0fc94d76d413748b15266f629f930a38045",
"private": false,
"record": {
"abstract": "The classical lambda calculus may be regarded both as a programming language\nand as a formal algebraic system for reasoning about computation. It provides a\ncomputational model equivalent to the Turing machine, and continues to be of\nenormous benefit in the classical theory of computation. We propose that\nquantum computation, like its classical counterpart, may benefit from a version\nof the lambda calculus suitable for expressing and reasoning about quantum\nalgorithms. In this paper we develop a quantum lambda calculus as an\nalternative model of quantum computation, which combines some of the benefits\nof both the quantum Turing machine and the quantum circuit models. The calculus\nturns out to be closely related to the linear lambda calculi used in the study\nof Linear Logic. We set up a computational model and an equational proof system\nfor this calculus, and we argue that it is equivalent to the quantum Turing\nmachine.",
"arxiv_id": "quant-ph/0307150",
"authors": [
"Andre van Tonder"
],
"categories": [
"quant-ph",
"cs.LO",
"hep-th"
],
"doi": "10.1137/S0097539703432165",
"journal_ref": "SIAM J.Comput. 33 (2004) 1109-1135",
"title": "A Lambda Calculus for Quantum Computation",
"url": "https://arxiv.org/abs/quant-ph/0307150"
},
"schema_id": "dorsal/arxiv",
"source": {
"execution_id": "06282dfb-4c59-4bc2-8ce3-dce23fb2a393",
"id": "arXiv Dataset IDs",
"type": "Model",
"variant": "snapshot-2026-03-01",
"version": "0.1.0"
},
"user_id": 1000002
}