Hostname: page-component-745bb68f8f-5r2nc Total loading time: 0 Render date: 2025-01-24T06:49:22.917Z Has data issue: false hasContentIssue false
  • English
  • Français

On quantum lambda calculi: a foundational perspective

Published online by Cambridge University Press:  17 November 2014

MARGHERITA ZORZI
MARGHERITA ZORZI*
Affiliation:
Dipartimento di Informatica, Università degli Studi di Verona, Strada Le Grazie 15, 37134, Verona, Italy Email: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper, we propose an approach to quantum λ-calculi. The ‘quantum data-classical control’ paradigm is considered. Starting from a measurement-free untyped quantum λ-calculus called Q, we will study standard properties such as confluence and subject reduction, and some good quantum properties. We will focus on the expressive power, analysing the relationship with other quantum computational models. Successively, we will add an explicit measurement operator to Q. On the resulting calculus, called Q*, we will propose a complete study of reduction sequences regardless of their finiteness, proving confluence results. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also propose a calculus which captures the three classes of quantum polytime complexity, showing an ICC-like approach in the quantum setting.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Issue 7 , October 2016 , pp. 1107 - 1195
Copyright
Copyright © Cambridge University Press 2014 

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

AA.VV. (2013) Website of the QML Project. Available at: http://fop.cs.nott.ac.uk/qml/.Google Scholar
Abramsky, S., Haghverdi, E. and Scott, P. J. (2002) Geometry of Interaction and Linear Combinatory Algebras. Mathematical Structures in Computer Science 12 (5) 625–665.Google Scholar
Aharonov, D., Kitaev, A. and Nisan, N. (1998) Quantum circuits with mixed states. In: Proceedings of the 30th Annual ACM Symposium on the Theory of Computing 20–30.Google Scholar
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 Journal on Computing 37 (1) 166–194.Google Scholar
Altenkirch, T. and Grattage, J. (2005) A functional quantum programming language. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science 249–258.Google Scholar
Altenkirch, T., Grattage, J., Vizzotto, J. and Sabry, A. (2007) An algebra of pure quantum programming. Electronic Notes in Theoretical Computer Science 210 (1) 23–47.Google Scholar
Arora, S. and Barak, B. (2009) Computational Complexity: A Modern Approach, Cambridge University Press.Google Scholar
Arrighi, P., Díaz-Caro, A., Gadella, M. and Grattage, G. (2008) Measurements and confluence in quantum Lambda calculi with explicit qubits. Electronic Notes in Theoretical Computer Science 270 (1) 59–74.Google Scholar
Arrighi, P., Díaz-Caro, A. and Valiron, B. (2012a) A system F accounting for scalars. Logical Methods in Computer Science 8 1–11.Google Scholar
Arrighi, P., Díaz-Caro, A. and Valiron, B. (2012b) A type system for the vectorial aspects of the linear-algebraic lambda-calculus. In: Proceedings of the 7th International Workshop on Developments of Computational Methods. Electronic Proceedings in Theoretical Computer Science 88 1–15.Google Scholar
Arrighi, P. and Dowek, G. (2008) Linear-algebraic lambda-calculus: Higher-order, encodings and confluence. In: Proceedings of the 19th Annual Conference on Term Rewriting and Applications 17–31.Google Scholar
Baillot, P., Coppola, P. and Dal Lago, U. (2011) Light logics and optimal reduction: Completeness and complexity. Information and Computation 209 (2) 118–142.Google Scholar
Baillot, P., Marion, Y.-J., Ronchi Della Rocca, S. (eds.) (2009) Special issue on implicit complexity. ACM Transactions on Computational Logic 10 (4).Google Scholar
Baillot, P. and Mogbil, V. (2004) Soft lambda-calculus: A language for polynomial time computation. In: Proceedings of the 7th International Conference Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science 2987 27–41.Google Scholar
Barebdregt, H. (1984) The lambda calculus: its Syntax and Semantics, North-Holland Publishing Co.Google Scholar
Basdevant, J. L. and Dalibard, J. (2005) Quantum Mechanics, Springer.Google Scholar
Benioff, P. (1980) The computer as a physical system: A microscopic quantum mechanical Hamiltonian model of computers as represented by Turing machines. Journal of Statistical Physics 5 563–591.Google Scholar
Bennett, C. H. and Landauer, R. (1985) The fundamental physical limits of computation. Scientific American 253 (1) 48–56.Google Scholar
Bernstein, E. and Vazirani, U. (1997) Quantum complexity theory. SIAM Journal on Computing 26 (5) 1411–1473.Google Scholar
Birkhoff, G. and Mac Lane, S. (1967) Algebra, The Macmillan Co. press.Google Scholar
Brassard, G. (1994) Cryptology column–quantum computing: The end of classical cryptography? SIGACT News 25 (4) 15–21.Google Scholar
Conway, J. (1990) A Course in Functional Analysis, Springer-Verlag.Google Scholar
Dalla Chiara, M. L., Giuntini, R. and Leporini, R (2003) Quantum computational logics. A survey. In: Proceedings of Trends in Logic. 50 Years of Studia Logica %, Hendricks, V. and Malinowski, J. (eds.), Kluwer.Google Scholar
Dal Lago, U., Masini, A. and Zorzi, M. (2009) On a measurement-free quantum lambda calculus with classical control. Mathematical Structures in Computer Science 19 (2) 297–335.Google Scholar
Dal Lago, U., Masini, A. and Zorzi, M. (2010) Quantum implicit computational complexity. Theoretical Computer Science 411 (2) 377–409.CrossRefGoogle Scholar
Dal Lago, U., Masini, A. and Zorzi, M. (2011) Confluence results for a quantum lambda calculus with measurements. Electronics Notes in Theoretical Computer Science 207 (2) 251–261.Google Scholar
Dal Lago, U. and Zorzi, M. (2012) Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications 46 (3) 413–450.CrossRefGoogle Scholar
Dal Lago, U. and Zorzi, M. (2013) Wave-style token machines and quantum lambda calculi. Long version available at: http://arxiv.org/abs/1307.0550.Google Scholar
Dal Lago, U. and Zorzi, M. (2014) Wave-style token machines and quantum lambda calculi. In: Informal Proceedings (with revision) of LINEARITY'14 (FloC'14), 13th July, Vienna 8 pp.Google Scholar
Danos, V., Kashefi, E. and Panangaden, P. (2005) Distributed measurement based quantum computation. Electronic Notes in Theoretical Computer Science 170 73–94.Google Scholar
Danos, V., Kashefi, E. and Panangaden, P. (2007) The measurement calculus. Journal of the ACM 52 (2) Article No. 8.Google Scholar
Danos, V., Kashefi, E., Panangaden, P. and Perdrix, S. (2009) Extended measurement calculus. In: Semantic Techniques in Quantum Computation. Cambridge University Press 235–310.CrossRefGoogle Scholar
Deutsch, D. (1985) Quantum theory, the Church–Turing principle and the universal quantum computer. In: Proceedings of the Royal Society of London A 400 97–117.Google Scholar
Deutsch, D., Ekert, A. and Lupacchini, R. (2000) Machines, logic and quantum physics. Bullettin of Symbolic Logic 6 (3) 265–283.Google Scholar
Delbecque, Y. (2011) Game semantics for quantum data. Electronics Notes in Theoretical Computer Science 270 (1) 41–57.Google Scholar
Dirac, P. (1947) Quantum theory, the Church–Turing principle and the universal quantum computer. In: Proceedings of the Royal Society of London A A400 97–117.Google Scholar
Einstein, A., Podolsky, B. and Rosen, N. (1935) Can quantum-mechanical description of physical reality be considered complete? Physical Review 47 777–780.Google Scholar
Feynman, R. P. (1982) Simulating physics with computers. International Journal of Theoretical Physics 21 (6–7) 467–488.Google Scholar
Gaboardi, M., Marion, J.-Y. and Ronchi Della Rocca, S. (2013) An implicit characterization of PSPACE. ACM Transactions on Computational Logic 13 (2) 18:1–18:36.Google Scholar
Gay, S. (2011) Bibliography on quantum programming languages. Available at: http://www.dcs.gla.ac.uk/simon/quantum/.Google Scholar
Gay, S. and Makie, I. (eds.) (2009) Semantic Techniques in Quantum Computation, Cambridge University Press.Google Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 (1) 1–102.Google Scholar
Girard, J.-Y., Scedrov, A. and Scott, P. (1992) Bounded linear logic: A modular approach to polynomial time computability. Theoretical Computer Science 97 1–66.Google Scholar
Girard, J.-Y. (1998) Light linear logic. Information and Computation 14 (3) 175–204.Google Scholar
Grattage, J. (2006) A Functional Quantum Programming Language, Ph.D. thesis, University of Nottingham.Google Scholar
Grattage, J. (2011) An overview of QML with a concrete implementation in Haskell. Electronic Notes in Theoretical Computer Science 270 (1) 165–174.Google Scholar
Grover, L. K. (1999) Quantum search on structured problems. Quantum Computing and Quantum Communications 1509 126–139.Google Scholar
Haghverdi, E. and Scott, P. J. (2002) Geometry of interaction and the dynamics of proof reduction: A tutorial. New Structures for Physics, Lectures Notes in Physics 813 357–417.Google Scholar
Hashuo, I. and Hoshino, N. (2011) Semantics of higher-order quantum computation via geometry of interaction. In: Proceedings of 26th Annual Symposium on Logic in Computer Science 237–246.Google Scholar
Hirvensalo, M. (2004) Quantum Computing, Springer-Verlag.Google Scholar
Isham, C. (1995) Lectures on Quantum Theory, Imperial College Press.Google Scholar
Jain, R., Ji, Z., Upadhyay, S. and Watrous, J. (2011) QIP=PSPACE. Journal of the ACM 58 (6) Article No. 30.Google Scholar
Jain, R., Upadhyay, S. and Watrous, J. (2009) Two-message quantum interactive proofs are in PSPACE. In: Proceedings of the 50th Annual IEEE Symposium on Foundations of Computer Science, IEEE Computer Society 534–543.Google Scholar
Kaye, P., Laflamme, R. and Mosca, M (2007) An Introduction to Quantum Computing, Oxford University Press.Google Scholar
Kitaev, A., Shen, A. and Vyalyi, M. (2002) Classical and Quantum Computation, AMS press.Google Scholar
Kleene, S. C. (1936) λ-definability and recursiveness. Duke Mathematical Journal 2 (2) 340–353.Google Scholar
Knill, E. (1996) Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory.Google Scholar
Lafont, Y. (2004) Soft linear logic and polynomial time. Theoretical Computer Science 318 163–180.Google Scholar
Lanzagorta, M. and Uhlmann, J. (2009) Quantum Computer Science, Morgan and Claypool Press.Google Scholar
Maccone, L. and Salasnish, L. (2008) Fisica moderna. Meccanica quantistica, caos e sistemi complessi, Carocci Press.Google Scholar
Masini, A., Viganò, L. and Zorzi, M. (2008) A qualitative modal representation of quantum register transformations. In: Proceedings of the 38th IEEE International Symposium on Multiple-Valued Logic (22–23 May 2008, Dallas, Texas, USA), IEEE CS Press 131–137.Google Scholar
Masini, A., Viganò, L. and Zorzi, M. (2011) Modal deduction systems for quantum state transformations. Multiple-Valued Logic and Soft Computing 17 (5–6) 475–519.Google Scholar
Maymin, P. (1996) Extending the λ-calculus to express randomized and quantumized algorithms. ArXiv:quant-ph/9612052. Unpublished.Google Scholar
Maymin, P. (1997) The lambda-q calculus can efficiently simulate quantum computers. ArXiv:quant-ph/9702057. Unpublished.Google Scholar
Nakahara, M. and Ohmi, T. (2008) Quantum Computing. From Linear Algebra to Physical Realizations, CRC Press.Google Scholar
Nielsen, M. A. (2003) Universal quantum computation using only projective measurement, quantum memory, and preparation of the 0 state. Physical Letters A 308 (2–3) 96–100.Google Scholar
Nielsen, M. A. and Chuang, I. L. (2000) Quantum Computation and Quantum Information. Physical Review, volume 308, Cambridge University Press.Google Scholar
Nishimura, H. and Ozawa, M. (2002) Computational complexity of uniform quantum circuit families and quantum Turing machines. Theoretical Computer Science 276 147–181.CrossRefGoogle Scholar
Nishimura, H. and Ozawa, M. (2009) Perfect computational equivalence between quantum Turing machines and finitely generated uniform quantum circuit families. Quantum Information Processing 8 (1) 12–24.CrossRefGoogle Scholar
Papadimitriou, C. (1994) Computational Complexity, Addison-Wesley.Google Scholar
Perdrix, S. (2006) Modèles formels du calcul quantique: Ressources, machines abstraites et calcul par mesure, Ph.D. thesis, Institut National Polytechnique de Grenoble.Google Scholar
Perdrix, S. (2007) Quantum patterns and types for entanglement and separability. Electronic Notes in Theoretical Computer Science 170 125–138.Google Scholar
Perdrix, V. and Jorrand, P., (2006) Classically controlled quantum computation. Mathematical Structures in Computer Science 16 (4) 601–620.Google Scholar
Preskill, J. (2006) Quantum Information and Computation, Lecture Notes in Physics volume 229, Rinton Press.Google Scholar
Roman, S. (2008) Advanced Linear Algebra, Springer.Google Scholar
Selinger, P. (2004) Towards a quantum programming language. Mathematical Structures in Computer Science 14 (4) 527–586.Google Scholar
Selinger, P. and Valiron, B. (2006) A λ-calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16 (3) 527–552.Google Scholar
Selinger, P. and Valiron, B. (2009) Quantum λ-calculus. In: Semantic Techniques in Quantum Computation, Cambridge University Press 135–172.Google Scholar
Shor, P. W. (1994) Algorithms for quantum computation: Discrete logarithms and factoring. In: Proceedings of 35th Annual Symposium on Foundations of Computer Science 124–134.Google Scholar
Shor, P. W. (1997) Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing 26 1484–1509.Google Scholar
Simon, D. (1994) On the power of quantum computation. SIAM Journal on Computing 26 116–123.Google Scholar
Simpson, A. (2005) Reduction in a linear lambda-calculus with applications to operational semantics. In: Proceedings of the 16th Annual Conference on Term Rewriting and Applications 219–234.Google Scholar
van Tonder, A. (2004) A λ-calculus for quantum computation. SIAM Journal on Computing 33 (5) 1109–1135.Google Scholar
Vaux, L. (2006) Lambda-calculus in an algebraic setting. Research report, Institut de Mathmatiques de Luminy.Google Scholar
Vaux, L. (2009) The algebraic lambda-calculus. Mathematical Structures in Computer Science 19 (5) 1029–1059.Google Scholar
Volpe, M., Viganò, L. and Zorzi, M. (2014) Quantum state transformations and branching distributed temporal logic. In: Proceedings of the 21st Workshop on Logic, Language, Information and Computation (1–4 September, 2014, Valparaiso, Chile). Lecture Notes in Computer Science 8652 1–19.Google Scholar
Wadler, P. (1994) A syntax for linear logic. In: Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics 513–529.Google Scholar
Wadsworth, C. (1980) Some unusual λ-calculus numeral systems. In: To H.B. Curry: Essays on Combinatory Logic, λ-Calculus and Formalism, Academic Press.Google Scholar
Wootters, W. K. and Zurek, W. H. (1982) A single quantum cannot be cloned. Nature 299 802–803.Google Scholar
Yao, A. (1993) Quantum circuit complexity. In: Proceedings of the 34th Annual Symposium on Foundations of Computer Science 352–360.Google Scholar
Zorzi, M. (2009) Lambda Calculi and Logics for Quantum Computing, Ph.D. thesis, Dipartimento di Informatica, Università degli Studi di Verona.Google Scholar