Abstract
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.
Partially funded by the STIC-AmSud Project FoQCoSS and PICT-PRH 2015-1208.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Where \(|x\rangle \) is the Dirac notation for vectors, with \(|0\rangle =\bigl ( {\begin{matrix}1\\ 0\end{matrix}}\bigr )\in \mathbb C^2\) and \(|1\rangle =\bigl ( {\begin{matrix}0\\ 1\end{matrix}}\bigr )\in \mathbb C^2\), so \(\{|0\rangle ,|1\rangle \}\) is an orthonormal basis of \(\mathbb C^2\), called here the “computational basis”.
- 2.
We speak about weights and not amplitudes, since the vector may not have norm 1. The projection rule normalizes the vector while reducing.
References
Abramsky, S.: Computational interpretations of linear logic. Theor. Comput. Sci. 111(1), 3–57 (1993)
Altenkirch, T., Grattage, J.: A functional quantum programming language. In: Proceedings of LICS 2005, pp. 249–258. IEEE (2005)
Arrighi, P., Díaz-Caro, A.: A system F accounting for scalars. Logical Methods in Computer Science 8(1:11) (2012)
Arrighi, P., Díaz-Caro, A., Valiron, B.: The vectorial lambda-calculus. Inf. Comput. 254(1), 105–139 (2017)
Arrighi, P., Dowek, G.: Lineal: a linear-algebraic lambda-calculus. Logical Methods in Computer Science 13(1:8) (2017)
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 in Computer Science 10(4:8) (2014)
Barber, A.: Dual intuitionistic linear logic. Technical report ECS-LFCS-96-347, The Laboratory for Foundations of Computer Science, University of Edinburgh (1996)
Díaz-Caro, A., Petit, B.: Linearity in the non-deterministic call-by-value setting. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 216–231. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32621-9_16
Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)
Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: ACM SIGPLAN Notices (PLDI 2013), vol. 48, no. 6, pp. 333–342 (2013)
Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. In: ACM SIGPLAN Notices (POPL 2014), vol. 49, no. 1, pp. 647–658 (2014)
Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233–264 (1981)
Selinger, P., Valiron, B.: Quantum lambda calculus. In: Gay, S., Mackie, I. (eds.) Semantic Techniques in Quantum Computation, pp. 135–172. Cambridge University Press, Cambridge (2009). Chapter 9
Zorzi, M.: On quantum lambda calculi: a foundational perspective. Math. Struct. Comput. Sci. 26(7), 1107–1195 (2016)
Acknowledgements
We would like to thank Eduardo Bonelli, Luca Paolini, Simona Ronchi della Rocca and Luca Roversi for interesting comments and suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Díaz-Caro, A., Dowek, G. (2017). Typing Quantum Superpositions and Measurement. In: Martín-Vide, C., Neruda, R., Vega-Rodríguez, M. (eds) Theory and Practice of Natural Computing. TPNC 2017. Lecture Notes in Computer Science(), vol 10687. Springer, Cham. https://doi.org/10.1007/978-3-319-71069-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-71069-3_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-71068-6
Online ISBN: 978-3-319-71069-3
eBook Packages: Computer ScienceComputer Science (R0)