In this paper we present a double effect version of the simply typed λ-calculus where we can represent both pure and impure quantum computations. The double effect calculus comprises a quantum arrow layer defined over a quantum monadic layer. In previous works we have developed the quantum arrow calculus, a calculus where we can consider just impure (or mixed) quantum computations. Technically, here we extend the quantum arrow calculus with a construct (and equations) that allows the communication of the monadic layer with the arrow layer of the calculus. That is, the quantum arrow is defined over a monadic instance enabling to consider pure and impure quantum computations in the same framework. As a practical contribution, the calculus allows to express quantum algorithms including reversible operations over pure states and measurements in the middle of the computation using a traditional style of functional programming and reasoning. We also define equations for algebraic reasoning of computations involving measurements. © 2013 Springer-Verlag.
CITATION STYLE
Vizzotto, J. K., Calegaro, B. C., & Piveta, E. K. (2013). A double effect λ-calculus for quantum computation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8129 LNCS, pp. 61–74). Springer Verlag. https://doi.org/10.1007/978-3-642-40922-6_5
Mendeley helps you to discover research relevant for your work.