Reasoning about Entanglement and Separability in Quantum Higher-Order Functions
We present a logical approach to the separability analysis issue for a functional quantum computation language. This logic is inspired by previous works on logical analysis of aliasing for imperative functional programs. Both analyses share similarities notably because they are highly non-compositional. Nevertheless, the intrisic non determinism of quantum computation has a large impact on the definitions of the semantics and the validity of logical assertions. To the knowledge of the authors, it is the first proposal of an entanglement/separability analysis for a functional quantum programming language with higher-order functions.
KeywordsQuantum State Operational Semantic Quantum Gate Reduction Rule Typing Rule
Unable to display preview. Download preview PDF.
- [Bar96]Barber, A.: Dual intuitionistic logic. Technical Report ECS-LFCS-96-347, Laboratory for Foundations of Computer Science, University of Edimburgh (1996)Google Scholar
- [BHY05]Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. In: Danvy, O., Pierce, B.C. (eds.) Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, pp. 280–293 (2005)Google Scholar
- [PZ08]Prost, F., Zerrari, C.: A logical analysis of entanglement and separability in quantum higher-order functions (2008), http://fr.arxiv.org/abs/0801.0649
- [Vid03]Vidal, G.: Efficient classical simulation of slightly entangled quantum computations. Physical Review Letters 91(14) (2003)Google Scholar