
06286004
a
06286004
Vizzotto, Juliana Kaizer
Calegaro, Bruno Crestani
Piveta, Eduardo Kessler
A double effect $\lambda $calculus for quantum computation.
Du Bois, Andr\'e Rauber (ed.) et al., Programming languages. 17th Brazilian symposium, SBLP 2013, Bras{\'\i}lia, Brazil, October 3  4, 2013. Proceedings. Berlin: Springer (ISBN 9783642409219/pbk). Lecture Notes in Computer Science 8129, 6174 (2013).
2013
Berlin: Springer
EN
doi:10.1007/9783642409226_5
Summary: In this paper we present a double effect version of the simply typed $\lambda $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.