Abstract
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Fiore, M.P.: Syntactic Considerations on Recursive Types. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 242–252. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996.561324
Cho, K.: Semantics for a Quantum Programming Language by Operator Algebras (2014), Master Thesis, University of Tokyo.
Cho, K.: Semantics for a Quantum Programming Language by Operator Algebras. New Generation Comput. 34(1-2), 25–68 (2016). https://doi.org/10.1007/s00354-016-0204-3
Cho, K., Westerbaan, A.: Von Neumann Algebras form a Model for the Quantum Lambda Calculus (2016), http://arxiv.org/abs/1603.02133, manuscript.
Clairambault, P., de Visme, M., Winskel, G.: Game semantics for quantum programming. PACMPL 3(POPL), 32:1–32:29 (2019). https://doi.org/10.1145/3290345
Fiore, M.P.: Axiomatic Domain Theory in Categories of Partial Maps. Ph.D. thesis, University of Edinburgh, UK (1994)
Gay, S.J.: Quantum programming languages: survey and bibliography. Mathematical Structures in Computer Science 16(4), 581–600 (2006). https://doi.org/10.1017/S0960129506005378
Harrow, A.W., Hassidim, A., Lloyd, S.: Quantum Algorithm for Linear Systems of Equations. Phys. Rev. Lett. 103, 150502 (Oct 2009). https://doi.org/10.1103/PhysRevLett.103.150502
Hasuo, I., Hoshino, N.: Semantics of higher-order quantum computation via geometry of interaction. Ann. Pure Appl. Logic 168(2), 404–469 (2017). https://doi.org/10.1016/j.apal.2016.10.010
Kissinger, A., Uijlen, S.: A categorical semantics for causal structure. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1–12. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005095
Kornell, A.: Quantum collections. International Journal of Mathematics 28(12), 1750085 (2017). https://doi.org/10.1142/S0129167X17500859
Lago, U.D., Faggian, C., Valiron, B., Yoshimizu, A.: The geometry of parallelism: classical, probabilistic, and quantum effects. In: Castagna,G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 833–845. ACM (2017), http://dl.acm.org/citation.cfm?id=3009859
Lindenhovius, B., Mislove, M., Zamdzhiev, V.: LNL-FPC: The Linear/Non-linear Fixpoint Calculus https://arxiv.org/abs/1906.09503, submitted.
Lindenhovius, B., Mislove, M., Zamdzhiev, V.: Mixed linear and non-linear recursive types. Proc. ACM Program. Lang. 3(ICFP), 111:1–111:29 (Jul 2019). https://doi.org/10.1145/3341715
Lindenhovius, B., Mislove, M.W., Zamdzhiev, V.: Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. pp. 659–668. ACM (2018). https://doi.org/10.1145/3209108.3209196
Mosca, M., Roetteler, M., Selinger, P.: Quantum Programming Languages (Dagstuhl Seminar 18381). Dagstuhl Reports 8(9), 112–132 (2019). https://doi.org/10.4230/DagRep.8.9.112
Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014. pp. 647–658. ACM (2014). https://doi.org/10.1145/2535838.2535879
Perdrix, S.: Quantum Entanglement Analysis Based on Abstract Interpretation. In: Alpuente, M., Vidal, G. (eds.) Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5079, pp. 270–282. Springer (2008). https://doi.org/10.1007/978-3-540-69166-2_18
Rennela, M.: Operator Algebras in Quantum Computation (2013), Master Thesis, Université Paris 7 Denis Diderot.
Rennela, M., Staton, S.: Classical Control and Quantum Circuits in Enriched Category Theory. Electr. Notes Theor. Comput. Sci. 336, 257–279 (2018). https://doi.org/10.1016/j.entcs.2018.03.027
Rios, F., Selinger, P.: A Categorical Model for a Quantum Circuit Description Language. In: QPL (2017). https://doi.org/10.4204/EPTCS.266.11
Ross, N.J.: Algebraic and Logical Methods in Quantum Computation (2015), Ph.D. thesis, Dalhousie University.
Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 14(4), 527–586 (2004). https://doi.org/10.1017/S0960129504004256
Shor, P.W.: Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer. SIAM Review 41(2), 303–332 (1999). https://doi.org/10.1137/S0036144598347011
Takesaki, M.: Theory of Operator Algebras. Vol. I, II and III. Springer-Verlag, Berlin (2002)
Westerbaan, A.: Quantum Programs as Kleisli Maps. In: Duncan, R., Heunen, C.(eds.) Proceedings 13th International Conference on Quantum Physics and Logic, QPL 2016, Glasgow, Scotland, 6-10 June 2016. EPTCS, vol. 236, pp. 215–228 (2016). https://doi.org/10.4204/EPTCS.236.14
Westerbaan, B.: Dagger and Dilation in the Category of Von Neumann algebras. Ph.D. thesis, Radboud University (2018), http://arxiv.org/abs/1803.01911
Wootters, W.K., Zurek, W.H.: A single quantum cannot be cloned. Nature 299(5886), 802–803 (1982)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Péchoux, R., Perdrix, S., Rennela, M., Zamdzhiev, V. (2020). Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_29
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_29
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)