Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-12-03T15:56:00.317Z Has data issue: false hasContentIssue false
  • English
  • Français

On a measurement-free quantum lambda calculus with classical control

Published online by Cambridge University Press:  01 April 2009

UGO DAL LAGO ,
ANDREA MASINI  and
MARGHERITA ZORZI
UGO DAL LAGO
Affiliation:
Dipartimento di Scienze dell'Informazione, Università di Bologna Email: dallago@cs.unibo.it
ANDREA MASINI
Affiliation:
Dipartimento di Informatica, Università di Verona Email: andrea.masini@univr.it
MARGHERITA ZORZI
Affiliation:
Dipartimento di Informatica, Università di Verona Email: margherita.zorzi@univr.it
Get access Rights & Permissions [Opens in a new window]

Abstract

We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 2 , April 2009 , pp. 297 - 335
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aharonov, D., van Dam, W., Kempe, J., Landau, Z., Lloyd, S. and Regev, O. (2007) Adiabatic quantum computation is equivalent to standard quantum computation. SIAM J. Comput. 37 (1)166–194.CrossRefGoogle Scholar
Altenkirch, T, and Grattage, J. (2005) A functional quantum programming language. Proc. of the 20th Annual IEEE Symposium on Logic in Computer Science 249–258.Google Scholar
Arrighi, P. and Dowek, G. (2008) Linear-algebraic lambda-calculus: higher-order, encodings and confluence. Springer-Verlag Lecture Notes in Computer Science 5117 17–81.CrossRefGoogle Scholar
Basdevant, J. L. and Dalibard, J. (2005) Quantum mechanics, Springer-Verlag.Google Scholar
Bernstein, E. and Vazirani, U. (1997) Quantum Complexity Theory. SIAM J. Comput. 26 (5)1411–1473.CrossRefGoogle Scholar
Danos, V. and Kashefi, E. and Panangaden, P. (2007) The measurement calculus. Journal of the ACM 54 (2).CrossRefGoogle Scholar
Deutsch, D. (1985) Quantum theory, the Church–Turing principle and the universal quantum computer. Proceedings of the Royal Society of London Ser. A A400 97–117.Google Scholar
Feynman, R. P. (1982) Simulating physics with computers. Internat. J. Theoret. Phys. 21 (6–7)467–488.CrossRefGoogle Scholar
Grover, L. K. (1999) Quantum search on structured problems. In: Quantum computing and quantum communications (Palm Springs, CA, 1998). Springer-Verlag Lecture Notes in Computer Science 1509 126–139.CrossRefGoogle Scholar
Kleene, S. C. (1936) λ-definability and recursiveness. Duke Math. J. 2 (2)340–353.CrossRefGoogle Scholar
Knill, E. (1996) Conventions for quantum pseudocode. Tech. Rep. LAUR-96-2724, Los Alamos National Laboratory.CrossRefGoogle Scholar
Maymin, P. (1996) Extending the lambda calculus to express randomized and quantumized algorithms. arXiv:quant-ph/9612052.Google Scholar
Maymin, P. (1997) The lambda-q calculus can efficiently simulate quantum computers. arXiv:quant-ph/9702057.Google Scholar
Nielsen, M. A. and Chuang, I. L. (2000) Quantum computation and quantum information, Cambridge University Press.Google Scholar
Nishimura, H. and Ozawa, M. (2002) Computational complexity of uniform quantum circuit families and quantum Turing machines. Theor. Comput. Sci. 276 (1–2)147–181.CrossRefGoogle Scholar
Perdrix, S. (2007) Quantum Patterns and Types for Entanglement and Separability. Electr. Notes Theor. Comput. Sci. 170 125–138.CrossRefGoogle Scholar
Selinger, P. (2004) Towards a Quantum Programming Language. Mathematical Structures in Computer Science 14 (4)527–586.CrossRefGoogle Scholar
Selinger, P. and Valiron, B. (2006) A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16 (3)527–552.CrossRefGoogle Scholar
Shor, P. W. (1994) Algorithms for quantum computation: discrete logarithms and factoring. In: Proc. 35th Annual Symposium on Foundations of Computer Science 124–134.CrossRefGoogle Scholar
Simpson, A. (2005) Reduction in a linear lambda-calculus with applications to operational semantics. In: Proc. of Proc. of the 16th Annual Conference on Term Rewriting and Applications. Springer-Verlag Lecture Notes in Computer Science 3467 219–234.CrossRefGoogle Scholar
van Tonder, A. (2004) A lambda calculus for quantum computation. SIAM J. Comput. 33 (5)1109–1135.CrossRefGoogle Scholar
Wadler, P. (1994) A syntax for linear logic. In: Proc. of the 9th International Conference on Mathematical Foundations of Programming Semantics. Springer-Verlag Lecture Notes in Computer Science 802 513–529.CrossRefGoogle Scholar
Wadsworth, C. (1980) Some unusual λ-calculus numeral systems. In: Seldin, J. and Hindley, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press.Google Scholar
Yao, A. (1993) Quantum Circuit Complexity. In: Proc. 34th Annual Symposium on Foundations of Computer Science, IEEE 352–360.Google Scholar