QWIRE: a core language for quantum circuits

ABSTRACT

This paper introduces QWIRE (``choir''), a language for defining quantum circuits and an interface for manipulating them inside of an arbitrary classical host language. QWIRE is minimal---it contains only a few primitives---and sound with respect to the physical properties entailed by quantum mechanics. At the same time, QWIRE is expressive and highly modular due to its relationship with the host language, mirroring the QRAM model of computation that places a quantum computer (controlled by circuits) alongside a classical computer (controlled by the host language).

We present QWIRE along with its type system and operational semantics, which we prove is safe and strongly normalizing whenever the host language is. We give circuits a denotational semantics in terms of density matrices. Throughout, we investigate examples that demonstrate the expressive power of QWIRE, including extensions to the host language that (1) expose a general analysis framework for circuits, and (2) provide dependent types.

References

1. T. Altenkirch and J. Grattage. A functional quantum programming language. In Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on, pages 249–258. IEEE, 2005.
2. T. Altenkirch and A. S. Green. The quantum IO monad. Semantic Techniques in Quantum Computation, pages 173–205, 2010.
3. M. Amy, M. Roetteler, and K. M. Svore. Verified compilation of space-efficient reversible circuits. Technical Report MSR-TR-2016-22, Microsoft Research, March 2016.
4. , pages 33–42, 2015. doi: 10.4204/EPTCS.195.3. P. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In L. Pacholski and J. Tiuryn, editors, Computer Science Logic, volume 933 of Lecture Notes in Computer Science, pages 121–135. Springer Berlin Heidelberg, 1995
5. S. Bettelli, T. Calarco, and L. Serafini. Toward an architecture for quantum programming. The European Physical Journal D, 25(2):181–200, 2003.
6. Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.4. 2015. Electronic resource, available from http://coq.inria.fr. E. D’Hondt and P. Panangaden. Quantum weakest preconditions. Mathematical Structures in Computer Science, 16(03):429–451, 2006.
7. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
8. E. H. Knill. Conventions for quantum pseudocode. Technical Report LAUR-96-2724, Los Alamos National Laboratory, 1996.
9. N. R. Krishnaswami, P. Pradic, and N. Benton. Integrating linear and dependent types. SIGPLAN Notices, 50(1):17–30, Jan. 2015.
10. C. McBride. I Got Plenty o’ Nuttin’, pages 207–233. Springer International Publishing, 2016. M. A. Nielsen and I. L. Chuang. Quantum computation and quantum information. Cambridge university press, 2010.
11. F. Pfenning and D. Griffith. Polarized substructural session types. In A. Pitts, editor, Foundations of Software Science and Computation Structures, volume 9034 of Lecture Notes in Computer Science, pages 3–22. Springer Berlin Heidelberg, 2015. N. J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015.
12. P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, Aug. 2004.
13. P. Selinger and B. Valiron. Quantum lambda calculus. In S. Gay and I. Mackie, editors, Semantic Techniques in Quantum Computation, pages 135–172. Cambridge University Press, 2009.
14. T. Sheard and S. P. Jones. Template meta-programming for haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell ’02, pages 1–16, New York, NY, USA, 2002. ACM.
15. S. Siddiqui, M. J. Islam, and O. Shehab. Five quantum algorithms using Quipper. arXiv preprint arXiv:1406.4481, 2014.
16. S. Staton. Algebraic effects, linearity, and quantum programming languages. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pages 395–406, New York, NY, USA, 2015. ACM.
17. J. K. Vizzotto, A. R. Du Bois, and A. Sabry. The arrow calculus as a quantum programming language. In H. Ono, M. Kanazawa, and R. de Queiroz, editors, Proccedings of Logic, Language, Information and Computation: 16th International Workshop, WoLLIC 2009, pages 379–393. Springer Berlin Heidelberg, June 2009. D. Wecker and K. M. Svore. LIQUi|>: A software design architecture and domain-specific language for quantum computing. arXiv:1402.4467 {quant-ph}, 2014
18. M. Ying. Floyd–hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19, 2011.
19. M. Ying. Quantum recursion and second quantisation. May 2014.
20. arXiv:1405.4443 {quant-ph}. N. Zeilberger. On the unity of duality. Annals of Pure and Applied Logic, 153(1–3):66–96, 2008. Special Issue: Classical Logic and Computation (2006)

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

• Theory of computation

  • Formal languages and automata theory

  • Logic

  • Semantics and reasoning

    • Program reasoning