Skip to main content
Top

2017 | OriginalPaper | Chapter

A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls

Author : Alejandro Díaz-Caro

Published in: Programming Languages and Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, \(\lambda _\rho \), follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, \(\lambda _\rho ^\circ \), takes advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
A generalisation to any arbitrary measurement can be considered in a future, however, for the sake of simplicity in the classical control, we consider only measurements in the computational basis, which is a common practice in quantum lambda calculi [11, 17, 19, 21, 22, 31].
 
Literature
1.
go back to reference Aharonov, D., Ambainis, A., Kempe, J., Vazirani, U.: Quantum walks on graphs. In: Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing, STOC 2001, pp. 50–59. ACM (2001) Aharonov, D., Ambainis, A., Kempe, J., Vazirani, U.: Quantum walks on graphs. In: Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing, STOC 2001, pp. 50–59. ACM (2001)
2.
go back to reference Altenkirch, T., Grattage, J.J.: A functional quantum programming language. In: Proceedings of LICS-2005, pp. 249–258. IEEE Computer Society (2005) Altenkirch, T., Grattage, J.J.: A functional quantum programming language. In: Proceedings of LICS-2005, pp. 249–258. IEEE Computer Society (2005)
3.
go back to reference Ambainis, A., Bach, E., Nayak, A., Vishwanath, A., Watrous, J.: One-dimensional quantum walks. In: Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing, STOC 2001, pp. 37–49. ACM (2001) Ambainis, A., Bach, E., Nayak, A., Vishwanath, A., Watrous, J.: One-dimensional quantum walks. In: Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing, STOC 2001, pp. 37–49. ACM (2001)
4.
go back to reference Arrighi, P., Díaz-Caro, A.: A System F accounting for scalars. Logical Methods Comput. Sci. 8(1:11) (2012) Arrighi, P., Díaz-Caro, A.: A System F accounting for scalars. Logical Methods Comput. Sci. 8(1:11) (2012)
6.
go back to reference Arrighi, P., Dowek, G.: Lineal: A linear-algebraic lambda-calculus. Logical Methods Comput. Sci. 13(1:8) (2017) Arrighi, P., Dowek, G.: Lineal: A linear-algebraic lambda-calculus. Logical Methods Comput. Sci. 13(1:8) (2017)
7.
go back to reference Assaf, A., Díaz-Caro, A., Perdrix, S., Tasson, C., Valiron, B.: Call-by-value, call-by-name and the vectorial behaviour of the algebraic \(\lambda \)-calculus. Logical Methods Comput. Sci. 10(4:8) (2014) Assaf, A., Díaz-Caro, A., Perdrix, S., Tasson, C., Valiron, B.: Call-by-value, call-by-name and the vectorial behaviour of the algebraic \(\lambda \)-calculus. Logical Methods Comput. Sci. 10(4:8) (2014)
8.
go back to reference Bǎdescu, C., Panangaden, P.: Quantum alternation: prospects and problems. In: Heunen, C., Selinger, P., Vicary, J. (eds.) Proceedings of QPL-2015. Electronic Proceedings in Theoretical Computer Science, vol. 195, pp. 33–42 (2015) Bǎdescu, C., Panangaden, P.: Quantum alternation: prospects and problems. In: Heunen, C., Selinger, P., Vicary, J. (eds.) Proceedings of QPL-2015. Electronic Proceedings in Theoretical Computer Science, vol. 195, pp. 33–42 (2015)
10.
go back to reference Díaz-Caro, A.: A lambda calculus for density matrices with classical and probabilistic controls. arXiv:1705.00097 (extended version with a 10-pages appendix with proofs) (2017) Díaz-Caro, A.: A lambda calculus for density matrices with classical and probabilistic controls. arXiv:​1705.​00097 (extended version with a 10-pages appendix with proofs) (2017)
11.
go back to reference Díaz-Caro, A., Dowek, G.: Typing quantum superpositions and measurements. To appear in LNCS 10687 (TPNC 2017) Díaz-Caro, A., Dowek, G.: Typing quantum superpositions and measurements. To appear in LNCS 10687 (TPNC 2017)
12.
go back to reference Díaz-Caro, A., Martínez, G.: Confluence in probabilistic rewriting. LSFA, to appear in ENTCS (2017) Díaz-Caro, A., Martínez, G.: Confluence in probabilistic rewriting. LSFA, to appear in ENTCS (2017)
14.
go back to reference Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. ACM SIGPLAN Notices (POPL 2011) 46(1), 523–534 (2011)CrossRefMATH Feng, Y., Duan, R., Ying, M.: Bisimulation for quantum processes. ACM SIGPLAN Notices (POPL 2011) 46(1), 523–534 (2011)CrossRefMATH
16.
go back to reference Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. ACM SIGPLAN Notices (PLDI 2013) 48(6), 333–342 (2013)CrossRefMATH Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. ACM SIGPLAN Notices (PLDI 2013) 48(6), 333–342 (2013)CrossRefMATH
17.
go back to reference Dal Lago, U., Masini, A., Zorzi, M.: Confluence results for a quantum lambda calculus with measurements. Electron. Notes Theor. Comput. Sci. 270(2), 251–261 (2011)CrossRefMATH Dal Lago, U., Masini, A., Zorzi, M.: Confluence results for a quantum lambda calculus with measurements. Electron. Notes Theor. Comput. Sci. 270(2), 251–261 (2011)CrossRefMATH
18.
go back to reference Nielsen, M., Chuang, I.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)MATH Nielsen, M., Chuang, I.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)MATH
19.
go back to reference Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. ACM SIGPLAN Notices (POPL 2014) 49(1), 647–658 (2014)MATH Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. ACM SIGPLAN Notices (POPL 2014) 49(1), 647–658 (2014)MATH
21.
go back to reference Selinger, P., Valiron, B.: Quantum lambda calculus. In: Gay, S., Mackie, I. (eds.) Semantic Techniques in Quantum Computation, Chap. 9, pp. 135–172. Cambridge University Press (2009) Selinger, P., Valiron, B.: Quantum lambda calculus. In: Gay, S., Mackie, I. (eds.) Semantic Techniques in Quantum Computation, Chap. 9, pp. 135–172. Cambridge University Press (2009)
22.
go back to reference Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathe. Struct. Comput. Sci. 16(3), 527–552 (2006)MathSciNetCrossRefMATH Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathe. Struct. Comput. Sci. 16(3), 527–552 (2006)MathSciNetCrossRefMATH
25.
go back to reference Ying, M.: Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19:1–19:49 (2011)CrossRef Ying, M.: Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19:1–19:49 (2011)CrossRef
27.
go back to reference Ying, M.: Foundations of Quantum Programming. Elsevier (2016) Ying, M.: Foundations of Quantum Programming. Elsevier (2016)
28.
go back to reference Ying, M., Ying, S., Wu, X.: Invariants of quantum programs: characterisations and generation. ACM SIGPLAN Notices (POPL 2017) 52(1), 818–832 (2017)CrossRefMATH Ying, M., Ying, S., Wu, X.: Invariants of quantum programs: characterisations and generation. ACM SIGPLAN Notices (POPL 2017) 52(1), 818–832 (2017)CrossRefMATH
30.
go back to reference Ying, M., Yu, N., Feng, Y.: Alternation in quantum programming: from superposition of data to superposition of programs. arXiv:1402.5172 (2014) Ying, M., Yu, N., Feng, Y.: Alternation in quantum programming: from superposition of data to superposition of programs. arXiv:​1402.​5172 (2014)
31.
Metadata
Title
A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
Author
Alejandro Díaz-Caro
Copyright Year
2017
DOI
https://doi.org/10.1007/978-3-319-71237-6_22

Premium Partner