×

Semantics of quantum programming languages: Classical control, quantum control. (English) Zbl 07576520

Summary: This chapter is devoted to a discussion on the semantics of quantum programming languages. We will discuss two main paradigms: the usual, standard co-processor model, and more exotic models based on quantum superposition of executions. We will discuss how these two systems can –or cannot– be unified, and how this relates to languages.

MSC:

68-XX Computer science
Full Text: DOI

References:

[1] Nielsen, M. A.; Chuang, I. L., Quantum Computation and Quantum Information (2002), Cambridge University Press
[2] Wootters, W. K.; Zurek, W. H., A single quantum cannot be cloned, Nature, 299, 802-803 (1982) · Zbl 1369.81022
[3] Selinger, P., Towards a quantum programming language, Math. Struct. Comput. Sci., 14, 4, 527-586 (2004) · Zbl 1085.68014
[4] Choi, M.-D., Completely positive linear maps on complex matrices, Linear Algebra Appl., 10, 3, 285-290 (1975) · Zbl 0327.15018
[5] Knill, E. H., Conventions for quantum pseudocode (1996), Los Alamos National Laboratory: Los Alamos National Laboratory Los Alamos, New Mexico, US, Tech. Rep. LAUR-96-2724
[6] Barendregt, H. P., The Lambda-Calculus, its Syntax and Semantics, Studies in Logic and the Foundation of Mathematics, vol. 103 (1984), North Holland · Zbl 0551.03007
[7] Barendregt, H.; Dekkers, W.; Statman, R., Lambda Calculus with Types, Perspective in Logic (2013), Cambridge University Press and ASL · Zbl 1347.03001
[8] van Tonder, A., A lambda calculus for quantum computation, SIAM J. Comput., 33, 5, 1109-1135 (2004) · Zbl 1057.81016
[9] Valiron, B., A functional programming language for quantum computation with classical control (2004), University of Ottawa, Master thesis
[10] Pagani, M.; Selinger, P.; Valiron, B., Applying quantitative semantics to higher-order quantum computing, in: Jagannathan and Sewell [93], pp. 647-658 · Zbl 1284.68271
[11] Selinger, P.; Valiron, B., A lambda calculus for quantum computation with classical control, Math. Struct. Comput. Sci., 16, 527-552 (2006) · Zbl 1122.68033
[12] Valiron, B., On quantum and probabilistic linear lambda-calculi (extended abstract), (Coecke, B.; Mackie, I.; Panangaden, P.; Selinger, P., Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models, QPL/DCM 2008. Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models, QPL/DCM 2008, Electronic Notes in Theoretical Computer Science, vol. 270 (2011)), 121-128 · Zbl 1347.68146
[13] Girard, J.-Y., Linear logic, Theor. Comput. Sci., 50, 1, 1-101 (1987) · Zbl 0625.03037
[14] Jones, C., Probabilistic non-determinism (1990), University of Edinburgh, Ph.D. thesis
[15] Gierz, G.; Hofmann, K. H.; Keimel, K.; Lawson, J. D.; Mislove, M.; Scott, D. S., Continuous Lattices and Domains, Encyclopedia of Mathematics and its Applications, vol. 93 (2003), Cambridge University Press · Zbl 1088.06001
[16] Graham, S. K., Closure properties of a probabilistic domain construction, (Main, M. G.; Melton, A.; Mislove, M. W.; Schmidt, D. A., Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics, MFPS’87. Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics, MFPS’87, Lecture Notes in Computer Science, vol. 298 (1988), Springer), 213-233 · Zbl 0644.68027
[17] Jung, A.; Tix, R., The troublesome probabilistic powerdomain, (Edalat, A.; Jung, A.; Keimel, K.; Kwiatkowska, M., Comprox III, Third Workshop on Computation and Approximation. Comprox III, Third Workshop on Computation and Approximation, Electronic Notes in Theoretical Computer Science, vol. 13 (1998)), 70-91
[18] Girard, J., The system F of variable types, fifteen years later, Theor. Comput. Sci., 45, 2, 159-192 (1986) · Zbl 0623.03013
[19] Girard, J., Coherent Banach spaces: a continuous denotational semantics, Theor. Comput. Sci., 227, 1-2, 275-297 (1999) · Zbl 0952.03025
[20] Ehrhard, T., On köthe sequence spaces and linear logic, Math. Struct. Comput. Sci., 12, 5, 579-623 (2002) · Zbl 1025.03066
[21] Girard, J.-Y., Between Logic and Quantic – a Tract, London Mathematical Society Lecture Notes Series, vol. 316, 346-381 (2004), Cambridge University Press, Ch. 10 · Zbl 1073.03036
[22] Danos, V.; Ehrhard, T., Probabilistic coherence spaces as a model of higher-order probabilistic computation, Inf. Comput., 209, 6, 966-991 (2011) · Zbl 1267.68085
[23] Ehrhard, T.; Pagani, M.; Tasson, C., The computational meaning of probabilistic coherence spaces, (Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 (2011), IEEE Computer Society), 87-96
[24] Girard, J.-Y., Normal functors, power series and lambda-calculus, Ann. Pure Appl. Log., 37, 2, 129-177 (1988) · Zbl 0646.03056
[25] R.F. Blute, P. Panangaden, R.A. Seely, Fock space: a model of linear exponential types, manuscript, revised version of [94], 1993.
[26] Blute, R. F., Hopf algebras and linear logic, Math. Struct. Comput. Sci., 6, 2, 189-212 (1996) · Zbl 0859.18008
[27] Ehrhard, T., Finiteness spaces, Math. Struct. Comput. Sci., 15, 4, 615-646 (2005) · Zbl 1084.03048
[28] Laird, J.; Manzonetto, G.; McCusker, G.; Pagani, M., Weighted relational models of typed lambda-calculi, (Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013 (2013), IEEE Computer Society), 301-310 · Zbl 1366.03171
[29] Mittelstaedt, P., Quantum Logic, Synthese Library, vol. 126 (1978), D. Reidel Publishing Company: D. Reidel Publishing Company Dordrecht, Holland · Zbl 0445.03038
[30] Baratella, S., Quantum coherent spaces and linear logic, RAIRO Theor. Inform. Appl., 44, 4, 419-441 (2010) · Zbl 1211.68241
[31] Selinger, P., Towards a semantics for higher-order quantum computation, (Selinger, P., Proceedings of the Second International Workshop on Quantum Programming Languages, QPL’04. Proceedings of the Second International Workshop on Quantum Programming Languages, QPL’04, TUCS General Publication, TUCS, vol. 33 (2004)), 127-143
[32] Selinger, P., Dagger compact closed categories and completely positive maps (extended abstract), (Selinger, P., Proceedings of the 3rd International Workshop on Quantum Programming Languages, QPL’05. Proceedings of the 3rd International Workshop on Quantum Programming Languages, QPL’05, Electronic Notes in Theoretical Computer Science, vol. 170 (2007)), 139-163 · Zbl 1277.18008
[33] Selinger, P.; Valiron, B., On a fully abstract model for a quantum linear functional language, (Selinger, P., Proceedings of the Fourth International Workshop on Quantum Programming Languages, QPL’06. Proceedings of the Fourth International Workshop on Quantum Programming Languages, QPL’06, Electronic Notes in Theoretical Computer Science, vol. 210 (2008)), 123-137 · Zbl 1279.68046
[34] Zhao, D.; Fan, T., Dcpo-completion of posets, Theor. Comput. Sci., 411, 22-24, 2167-2173 (2010) · Zbl 1192.06007
[35] Melliès, P.; Tabareau, N.; Tasson, C., An explicit formula for the free exponential modality of linear logic, (Albers, S.; Marchetti-Spaccamela, A.; Matias, Y.; Nikoletseas, S. E.; Thomas, W., Proceedings of the 36th International Colloquium on Automata, Languages and Programming, ICALP 2009, Part II. Proceedings of the 36th International Colloquium on Automata, Languages and Programming, ICALP 2009, Part II, Lecture Notes in Computer Science, vol. 5556 (2009), Springer), 247-260 · Zbl 1248.03080
[36] Ehrhard, T.; Tasson, C.; Pagani, M., Probabilistic coherence spaces are fully abstract for probabilistic PCF, in: Jagannathan and Sewell [93], pp. 309-320 · Zbl 1284.68268
[37] Clairambault, P.; de Visme, M., Full abstraction for the quantum lambda-calculus, Proc. ACM Programm. Lang., 4, POPL, 63:1-63:28 (2020)
[38] Westerbaan, A., Quantum programs as kleisli maps, (Duncan, R.; Heunen, C., Proceedings of the 13th International Conference on Quantum Physics and Logic, QPL 2016. Proceedings of the 13th International Conference on Quantum Physics and Logic, QPL 2016, Electronic Proceedings in Theoretical Computer Science, vol. 236 (2016)), 215-228 · Zbl 1486.81071
[39] Westerbaan, A. A., The category of von Neumann algebras (2019), Radboud Universiteit Nijmegen, Ph.D. thesis
[40] Malherbe, O.; Scott, P.; Selinger, P., Presheaf models of quantum computation: an outline, (Coecke, B.; Ong, L.; Panangaden, P., Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday. Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 7860 (2013), Springer), 178-194 · Zbl 1264.81119
[41] Péchoux, R.; Perdrix, S.; Rennela, M.; Zamdzhiev, V., Quantum programming with inductive datatypes: causality and affine type theory, (Goubault-Larrecq, J.; König, B., Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2020. Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2020, Lecture Notes in Computer Science, vol. 12077 (2020), Springer), 562-581 · Zbl 1442.68034
[42] Benton, N., A mixed linear and non-linear logic: proofs, terms and models (extended abstract), (Pacholski, L.; Tiuryn, J., Computer Science Logic, Eighth International Workshop, CSL’94, Selected Papers. Computer Science Logic, Eighth International Workshop, CSL’94, Selected Papers, Lecture Notes in Computer Science, vol. 933 (1994), European Association for Computer Science Logic, Springer Verlag), 121-135 · Zbl 1044.03543
[43] Lindenhovius, B.; Mislove, M. W.; Zamdzhiev, V., Enriching a linear/non-linear lambda calculus: a programming language for string diagrams, (Dawar, A.; Grädel, E., Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’2018 (2018), ACM), 659-668 · Zbl 1454.03023
[44] Fu, P.; Kishida, K.; Selinger, P., Linear dependent type theory for quantum programming languages: extended abstract, (Hermanns, H.; Zhang, L.; Kobayashi, N.; Miller, D., Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 (2020), ACM), 440-453 · Zbl 1502.68076
[45] Paykin, J., Linear/non-linear types for embedded domain-specific languages (2018), University of Pennsylvania, Ph.D. thesis
[46] Lee, D.; Perrelle, V.; Valiron, B.; Xu, Z., Concrete categorical model of a quantum circuit description language with measurement, (Bojanczyk, M.; Chekuri, C., Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021. Proceedings of the 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2021, LIPIcs, vol. 213 (2021)), 51:1-51:20 · Zbl 07799629
[47] Gandy, R., Church’s thesis and principles for mechanisms, (Barwise, J.; Keisler, H. J.; Kunen, K., The Kleene Symposium. The Kleene Symposium, Studies in Logic and the Foundations of Mathematics, vol. 101 (1980), North-Holland Publishing Company), 123-148 · Zbl 0465.03022
[48] Copeland, B. J., The Church-Turing thesis, (Zalta, E. N., The Stanford Encyclopedia of Philosophy (2017))
[49] Kleene, S. C. (1967), Mathematical Logic, Dover Publication Inc. · Zbl 0149.24309
[50] Turing, A. M., On computable numbers, with an application to the Entscheidungsproblem, Proc. Lond. Math. Soc. (2), 42, 230-265 (1936), can be found integrally, and commented, in [95] · JFM 62.1059.03
[51] Kleene, S. C., A theory of positive integers in formal logic, part I, Am. J. Math., 57, 1, 153-173 (1935) · Zbl 0011.00202
[52] Kleene, S. C., A theory of positive integers in formal logic, part II, Am. J. Math., 57, 2, 219-244 (1935) · Zbl 0011.24103
[53] Church, A., An unsolvable problem of elementary number theory, Am. J. Math., 58, 2, 345-363 (1936) · JFM 62.0046.01
[54] Turing, A., Systems of logic based on ordinals (1938), Princeton University, Ph.D. thesis · Zbl 0021.09704
[55] Dershowitz, N.; Gurevich, Y., A natural axiomatization of computability and proof of Church’s thesis, Bull. Symb. Log., 14, 3, 299-350 (2008) · Zbl 1167.03027
[56] Deutsch, D., Quantum theory, the Church-Turing principle and the universal quantum computer, Proc. R. Soc. Lond. A, 400, 1818, 97-117 (1985) · Zbl 0900.81019
[57] Nielsen, M. A., Computable functions, quantum measurements, and quantum dynamics, Phys. Rev. Lett., 79, 2915-2918 (1997)
[58] Arrighi, P.; Dowek, G., The physical Church-Turing thesis and the principles of quantum theory, Int. J. Found. Comput. Sci., 23, 5, 1131-1146 (2012) · Zbl 1279.68096
[59] Dowek, G., Around the physical Church-Turing thesis: cellular automata, formal languages, and the principles of quantum theory, (Dediu, A.; Martín-Vide, C., Proceedings of the 6th International Conference on Language and Automata Theory and Applications, LATA 2012. Proceedings of the 6th International Conference on Language and Automata Theory and Applications, LATA 2012, Lecture Notes in Computer Science, vol. 7183 (2012), Springer), 21-37 · Zbl 1351.68099
[60] Arrighi, P., An overview of quantum cellular automata, Nat. Comput., 18, 4, 885-899 (2019) · Zbl 1530.81039
[61] Chiribella, G.; D’Ariano, G. M.; Perinotti, P.; Valiron, B., Quantum computations without definite causal structure, Phys. Rev. A, 88, Article 022318 pp. (2013)
[62] Wilson, M.; Chiribella, G., A Diagrammatic Approach to Information Transmission in Generalised Switches (2020)
[63] Arrighi, P.; Martiel, S., Quantum causal graph dynamics, Phys. Rev. D, 96, Article 024026 pp. (2017)
[64] Portmann, C.; Matt, C.; Maurer, U.; Renner, R.; Tackmann, B., Causal boxes: quantum information-processing systems closed under composition, IEEE Trans. Inf. Theory, 63, 5, 3277-3305 (2017) · Zbl 1368.81055
[65] Vanrietvelde, A.; Kristjánsson, H.; Barrett, J., Routed quantum circuits, Quantum, 5, 503 (2021)
[66] Chiribella, G.; D’Ariano, G. M.; Perinotti, P., Transforming quantum operations: quantum supermaps, Europhys. Lett., 83, 3, Article 30004 pp. (2008)
[67] Wechs, J.; Dourdent, H.; Abbott, A. A.; Branciard, C., Quantum circuits with classical versus quantum control of causal order, PRX Quant., 2, Article 030335 pp. (2021)
[68] Chiribella, G.; D’Ariano, G. M.; Perinotti, P., Quantum circuit architecture, Phys. Rev. Lett., 101, Article 060401 pp. (2008)
[69] Chiribella, G.; D’Ariano, G. M.; Perinotti, P., Theoretical framework for quantum networks, Phys. Rev. A, 80, Article 022339 pp. (2009) · Zbl 1255.81045
[70] Friis, N.; Dunjko, V.; Dür, W.; Briegel, H. J., Implementing quantum control for unknown subroutines, Phys. Rev. A, 89, Article 030303 pp. (2014)
[71] Procopio, L. M.; Moqanaki, A.; Araújo, M.; Costa, F.; Alonso Calafell, I.; Dowd, E. G.; Hamel, D. R.; Rozema, L. A.; Brukner, Č.; Walther, P., Experimental superposition of orders of quantum gates, Nat. Commun., 6, 1, Article 7913 pp. (2015)
[72] Taddei, M. M.; Cariñe, J.; Martínez, D.; García, T.; Guerrero, N.; Abbott, A. A.; Araújo, M.; Branciard, C.; Gómez, E. S.; Walborn, S. P.; Aolita, L.; Lima, G., Computational advantage from the quantum superposition of multiple temporal orders of photonic gates, PRX Quant., 2, Article 010320 pp. (2021)
[73] Araújo, M.; Costa, F.; Brukner, Č., Computational advantage from quantum-controlled ordering of gates, Phys. Rev. Lett., 113, Article 250402 pp. (2014)
[74] Moggi, E., Computational lambda-calculus and monads, (Proceedings of the Fourth Symposium on Logic in Computer Science, LICS’89 (1989), IEEE, IEEE Computer Society Press), 14-23; http://www.lfcs.inf.ed.ac.uk/reports/88/ECS-LFCS-88-66/ · Zbl 0716.03007
[75] de’Liguoro, U.; Piperno, A., Non deterministic extensions of untyped lambda-calculus, Inf. Comput., 122, 2, 149-177 (1995) · Zbl 1096.03502
[76] Lago, U. D.; Zorzi, M., Probabilistic operational semantics for the lambda calculus, RAIRO Theor. Inform. Appl., 46, 3, 413-450 (2012) · Zbl 1279.68183
[77] Leventis, T., Probabilistic λ-theories (2016), Aix-Marseille Université, Thèse de doctorat
[78] Vaux, L., The algebraic lambda-calculus, Math. Struct. Comput. Sci., 19, 5, 1029-1059 (2009) · Zbl 1186.03025
[79] Kluge, W. E., A reversible SE(M)CD machine, (Koopman, P. W.M.; Clack, C., Selected Papers of the 11th International Workshop on the Implementation of Functional Languages, IFL’99. Selected Papers of the 11th International Workshop on the Implementation of Functional Languages, IFL’99, Lecture Notes in Computer Science, vol. 1868 (1999), Springer), 95-113
[80] Altenkirch, T.; Grattage, J., A functional quantum programming language, (Panangaden, P., Proceedings of the 20th Symposium on Logic in Computer Science, LICS’05 (2005), IEEE, IEEE Computer Society Press), 249-258
[81] T. Altenkirch, J. Grattage, QML: Quantum data and control, draft, extended version of the LICS publication, [80], 2005.
[82] Arrighi, P.; Dowek, G., Linear-algebraic lambda-calculus: higher-order, encodings, and confluence, (Voronkov, A., Proceedings of the 19th International Conference on Rewriting Techniques and Applications, RTA’08. Proceedings of the 19th International Conference on Rewriting Techniques and Applications, RTA’08, Lecture Notes in Computer Science, vol. 5117 (2008), Springer), 17-31 · Zbl 1146.68027
[83] Arrighi, P.; Dowek, G., Lineal: a linear-algebraic lambda-calculus, Log. Methods Comput. Sci., 13, 1 (2017) · Zbl 1448.68206
[84] Arrighi, P.; Dowek, G., A computational definition of the notion of vectorial space, (Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications (WRLA’04). Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications (WRLA’04), Electronic Notes in Theoretical Computer Science, vol. 117 (2005)), 249-261 · Zbl 1272.68166
[85] Hatcliff, J.; Danvy, O., Thunks and the lambda-calculus (1996), BRICS, University of Aahrus, Tech. Rep. RS-96-19 · Zbl 0881.68025
[86] Breazu-Tannen, V.; Meyer, A. R., Computable values can be classical, (Proceedings of the 14th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’87 (1987), ACM), 238-245
[87] Breazu-Tannen, V., Combining algebra and higher-order types, (Proceedings of the Third Annual Symposium on Logic in Computer Science, LICS ’88 (1988), IEEE Computer Society), 82-90
[88] Diaz Caro, A., Du typage vectoriel (2011), Université de Grenoble, Ph.D. thesis
[89] Díaz-Caro, A.; Guillermo, M.; Miquel, A.; Valiron, B., Realizability in the unitary sphere, (Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’19 (2019), IEEE), 1-13
[90] Sabry, A.; Valiron, B.; Vizzotto, J. K., From symmetric pattern-matching to quantum control, (Baier, C.; Lago, U. D., Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2018. Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2018, Lecture Notes in Computer Science, vol. 10803 (2018), Springer), 348-364 · Zbl 1504.68075
[91] Badescu, C.; Panangaden, P., Quantum alternation: prospects and problems, (Heunen, C.; Selinger, P.; Vicary, J., Proceedings of the 12th International Workshop on Quantum Physics and Logic, QPL 2015. Proceedings of the 12th International Workshop on Quantum Physics and Logic, QPL 2015, Electronic Proceedings in Theoretical Computer Science, vol. 195 (2015)), 33-42 · Zbl 1477.81026
[92] Branciard, C.; Clément, A.; Mhalla, M.; Perdrix, S., Coherent control and distinguishability of quantum channels via PBS-diagrams, (Bonchi, F.; Puglisi, S. J., Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021. Proceedings of the 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, LIPIcs, vol. 202 (2021), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 22:1-22:20 · Zbl 07724195
[93] (Jagannathan, S.; Sewell, P., Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’14 (2014), ACM) · Zbl 1282.68034
[94] Blute, R. F.; Panangaden, P.; Seely, R. A., Holomorphic models of exponential types in linear logic, (Brookes, S.; Main, M.; Melton, A.; Mislove, M.; Schmidt, D., Mathematical Foundations of Programming Semantics: Ninth International Conference, MFPS IX. Mathematical Foundations of Programming Semantics: Ninth International Conference, MFPS IX, Lecture Notes in Computer Science, vol. 802 (1993), Springer Verlag), 474-512, a revised version can be found in [25] · Zbl 1509.18020
[95] (Girard, J.-Y., La Machine de Turing. La Machine de Turing, Points Sciences, vol. 131 (1995)), contains [50] and [96] in integrality, with comments
[96] Turing, A. M., Computing machinery and intelligence, J. Mind Assoc., 59, 236, 433-460 (1950), can be found integrally, and commented, in [95]
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.