• Home   /
• Archive by category "1"

Quantum Programming Languages Survey And Bibliography

Quantum programming is the process of assembling sequences of instructions, called quantum programs, that are capable of running on a quantum computer. Quantum programming languages help express quantum algorithms using high-level constructs.[1]

Quantum instruction sets

Quantum instruction sets are used to turn higher level algorithms into physical instructions that can be executed on quantum processors. Sometimes these instructions are specific to a given hardware platform, e.g. ion traps or superconducting qubits.

Quil

Main article: Quil (instruction set architecture)

Quil is an instruction set architecture for quantum computing that first introduced a shared quantum/classical memory model. It was introduced by Robert Smith, Michael Curtis, and William Zeng in A Practical Quantum Instruction Set Architecture.[2] Many quantum algorithms (including quantum teleportation, quantum error correction, simulation,[3][4] and optimization algorithms[5]) require a shared memory architecture.

OpenQASM

Main article: OpenQASM

OpenQASM[6] is the intermediate representation introduced by IBM for use with their Quantum Experience.

Quantum programming languages

There are two main groups of quantum programming languages: imperative quantum programming languages and functional quantum programming languages.

Imperative languages

The most prominent representatives of the imperative languages are QCL,[7] LanQ[8] and Q|SI>.[9]

QCL

Main article: Quantum computation language

Quantum Computation Language (QCL) is one of the first implemented quantum programming languages.[10] The most important feature of QCL is the support for user-defined operators and functions. Its syntax resembles the syntax of the C programming language and its classical data types are similar to primitive data types in C. One can combine classical code and quantum code in the same program.

Quantum pseudocode

Quantum pseudocode proposed by E. Knill is the first formalized language for description of quantum algorithms. It was introduced and, moreover, was tightly connected with a model of quantum machine called Quantum Random Access Machine (QRAM).

Q|SI>

Q|SI>[9] is a platform embedded in .Net language supporting quantum programming in a quantum extension of while-language.[11] This platform includes a compiler of the quantum while-language[12] and a chain of tools for the simulation of quantum computation, optimisation of quantum circuits, termination analysis of quantum programs,[13] and verification of quantum programs.[14][15]

Q language

Q Language is the second implemented imperative quantum programming language.[16] Q Language was implemented as an extension of C++ programming language. It provides classes for basic quantum operations like QHadamard, QFourier, QNot, and QSwap, which are derived from the base class Qop. New operators can be defined using C++ class mechanism.

Quantum memory is represented by class Qreg.

Qreg x1; // 1-qubit quantum register with initial value 0 Qreg x2(2,0); // 2-qubit quantum register with initial value 0

The computation process is executed using a provided simulator. Noisy environments can be simulated using parameters of the simulator.

qGCL

Quantum Guarded Command Language (qGCL) was defined by P. Zuliani in his PhD thesis. It is based on Guarded Command Language created by Edsger Dijkstra.

It can be described as a language of quantum programs specification.

QMASM

Quantum Macro Assembler (QMASM) is a low-level language specific to quantum annealers such as the D-Wave.[17]

Functional languages

Efforts are underway to develop functional programming languages for quantum computing. Functional programming languages are well-suited for reasoning about programs. Examples include Selinger's QPL,[18] and the Haskell-like language QML by Altenkirch and Grattage.[19][20] Higher-order quantum programming languages, based on lambda calculus, have been proposed by van Tonder,[21] Selinger and Valiron[22] and by Arrighi and Dowek.[23]

QFC and QPL

QFC and QPL are two closely related quantum programming languages defined by Peter Selinger. They differ only in their syntax: QFC uses a flow chart syntax, whereas QPL uses a textual syntax. These languages have classical control flow but can operate on quantum or classical data. Selinger gives a denotational semantics for these languages in a category of superoperators.

QML

QML is a Haskell-like quantum programming language by Altenkirch and Grattage.[19] Unlike Selinger's QPL, this language takes duplication, rather than discarding, of quantum information as a primitive operation. Duplication in this context is understood to be the operation that maps to , and is not to be confused with the impossible operation of cloning; the authors claim it is akin to how sharing is modeled in classical languages. QML also introduces both classical and quantum control operators, whereas most other languages rely on classical control.

An operational semantics for QML is given in terms of quantum circuits, while a denotational semantics is presented in terms of superoperators, and these are shown to agree. Both the operational and denotational semantics have been implemented (classically) in Haskell.[24]

LIQUi|>

LIQUi|> (pronounced 'liquid') is a quantum simulation extension on the F# programming language.[25] It is currently being developed by the Quantum Architectures and Computation Group (QuArC)[26] part of the StationQ efforts at Microsoft Research. LIQUi|> seeks to allow theorists to experiment with quantum algorithm design before physical quantum computers are available for use.[27]

It includes a programming language, optimization and scheduling algorithms, and quantum simulators. LIQUi|> can be used to translate a quantum algorithm written in the form of a high-level program into the low-level machine instructions for a quantum device.[28]

Quantum lambda calculi

Quantum lambda calculi are extensions of the classical lambda calculus introduced by Alonzo Church and Stephen Cole Kleene in the 1930s. The purpose of quantum lambda calculi is to extend quantum programming languages with a theory of higher-order functions.

The first attempt to define a quantum lambda calculus was made by Philip Maymin in 1996.[29] His lambda-q calculus is powerful enough to express any quantum computation. However, this language can efficiently solve NP-complete problems, and therefore appears to be strictly stronger than the standard quantum computational models (such as the quantum Turing machine or the quantum circuit model). Therefore, Maymin's lambda-q calculus is probably not implementable on a physical device.

In 2003, André van Tonder defined an extension of the lambda calculus suitable for proving correctness of quantum programs. He also provided an implementation in the Scheme programming language.[30]

In 2004, Selinger and Valiron defined a strongly typed lambda calculus for quantum computation with a type system based on linear logic.

Quipper

Quipper was published in 2013.[31] It is implemented as an embedded language, using Haskell as the host language.[32] For this reason, quantum programs written in Quipper are written in Haskell using provided libraries. For example, the following code implements preparation of a superposition

import Quipper spos :: Bool -> Circ Qubit spos b = do q <- qinit b r <- hadamard q return r

Q#

Q# is a quantum programming language from Microsoft.

References

1. ^Jarosław Adam Miszczak. High-level Structures in Quantum Computing. ASIN 1608458512.
2. ^Smith, Robert S.; Curtis, Michael J.; Zeng, William J. (2016-08-10). "A Practical Quantum Instruction Set Architecture". arXiv:1608.03355 [quant-ph].
3. ^McClean, Jarrod R.; Romero, Jonathan; Babbush, Ryan; Aspuru-Guzik, Alán (2016-02-04). "The theory of variational hybrid quantum-classical algorithms". New Journal of Physics. 18 (2): 023023. arXiv:1509.04279. Bibcode:2016NJPh...18b3023M. doi:10.1088/1367-2630/18/2/023023. ISSN 1367-2630.
4. ^Rubin, Nicholas C. (2016-10-21). "A Hybrid Classical/Quantum Approach for Large-Scale Studies of Quantum Systems with Density Matrix Embedding Theory". arXiv:1610.06910 [quant-ph].
5. ^Farhi, Edward; Goldstone, Jeffrey; Gutmann, Sam (2014-11-14). "A Quantum Approximate Optimization Algorithm". arXiv:1411.4028 [quant-ph].
6. ^qiskit-openqasm: OpenQASM specification, International Business Machines, 2017-07-04, retrieved 2017-07-06
7. ^Bernhard Omer. "The QCL Programming Language".
8. ^Hynek Mlnařík. "LanQ – a quantum imperative programming language".
9. ^ abLiu, Shusen; Zhou, li; Guan, Ji; He, Yang; Duan, Runyao; Ying, Mingsheng (2017-05-09). "Q|SI>: A Quantum Programming Language". SCIENTIA Sinica Information. 47 (10): 1300. doi:10.1360/N112017-00095.
10. ^"QCL - A Programming Language for Quantum Computers". tuwien.ac.at. Retrieved 2017-07-20.
11. ^Ying, Mingsheng (January 2012). "Floyd–hoare Logic for Quantum Programs". ACM Trans. Program. Lang. Syst. 33 (6): 19:1–19:49. doi:10.1145/2049706.2049708. ISSN 0164-0925.
12. ^Ying, Mingsheng; Feng, Yuan (2010). "A Flowchart Language for Quantum Programming". IEEE Transactions on Software Engineering. 37 (4): 466–485. doi:10.1109/TSE.2010.94. ISSN 0098-5589.
13. ^Ying, Mingsheng; Yu, Nengkun; Feng, Yuan; Duan, Runyao (2013). "Verification of quantum programs". Science of Computer Programming. 78 (9): 1679–1700. doi:10.1016/j.scico.2013.03.016.
14. ^Ying, Mingsheng; Ying, Shenggang; Wu, Xiaodi (2017). "Invariants of Quantum Programs: Characterisations and Generation". Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. POPL 2017. New York, NY, USA: ACM. 52: 818–832. doi:10.1145/3093333.3009840. ISBN 9781450346603.
15. ^Liu, Tao; Li, Yangjia; Wang, Shuling; Ying, Mingsheng; Zhan, Naijun (2016-01-15). "A Theorem Prover for Quantum Hoare Logic and Its Applications". arXiv:1601.03835 [cs.LO].
16. ^"Software for the Q language". archive.org. 2001-11-23. Retrieved 2017-07-20.
17. ^Scott Pakin, "A Quantum Macro Assembler", Proceedings of the 20th Annual IEEE High Performance Extreme Computing Conference 2016
18. ^Peter Selinger, "Towards a quantum programming language", Mathematical Structures in Computer Science 14(4):527-586, 2004.
19. ^ abJonathan Grattage: QML Research (website)
20. ^T. Altenkirch, V. Belavkin, J. Grattage, A. Green, A. Sabry, J. K. Vizzotto, QML: A Functional Quantum Programming Language (website)
21. ^Andre van Tonder, "A Lambda Calculus for Quantum Computation", SIAM J. Comput., 33(5), 1109–1135. (27 pages), 2004. Also available from arXiv:quant-ph/0307150
22. ^Peter Selinger and Benoît Valiron, "A lambda calculus for quantum computation with classical control", Mathematical Structures in Computer Science 16(3):527-552, 2006.
23. ^Pablo Arrighi, Gilles Dowek, "Linear-algebraic lambda-calculus: higher-order, encodings and confluence", 2006
24. ^Jonathan Grattage, QML: A Functional Quantum Programming Language (compiler), 2005–2008
25. ^"The Language Integrated Quantum Operations Simulator". github.io. Retrieved 2017-07-20.
26. ^Quantum Architectures and Computation Group (QuArC), https://www.microsoft.com/en-us/research/group/quantum-architectures-and-computation-group-quarc/, 2011
27. ^"StationQ". microsoft.com. Retrieved 2017-07-20.
28. ^"Language-Integrated Quantum Operations: LIQUi|>". 2016.
29. ^Philip Maymin, "Extending the Lambda Calculus to Express Randomized and Quantumized Algorithms", 1996
30. ^André van Tonder. "A lambda calculus for quantum computation (website)".
31. ^Alexander S. Green; Peter LeFanu Lumsdaine; Neil J. Ross; Peter Selinger; Benoît Valiron. "The Quipper Language (website)".
32. ^Alexander S. Green; Peter LeFanu Lumsdaine; Neil J. Ross; Peter Selinger; Benoît Valiron (2013). "An Introduction to Quantum Programming in Quipper". Lecture Notes in Computer Science. Lecture Notes in Computer Science. 7948: 110–124. arXiv:1304.5485. doi:10.1007/978-3-642-38986-3_10. ISBN 978-3-642-38985-6.

Mingsheng, Ying. Foundations of quantum programming. Cambridge, MA. ISBN 9780128025468. OCLC 945735387.

Papers

This is a list of Peter Selinger's papers, along with abstracts and hyperlinks.

The references are also available in BibTeX format.

• A categorical model for a quantum circuit description language (with F. Rios)
• Optimal ancilla-free Clifford+T approximation of z-rotations (with N. J. Ross)
• A finite alternation result for reversible boolean circuits
• Reversible k-valued logic circuits are finitely generated for odd k
• Programming the quantum future (with B. Valiron, N. J. Ross, D. S. Alexander, and J. M. Smith)
• Quipper: Concrete Resource Estimation in Quantum Algorithms (with J. M. Smith, N. J. Ross, and B. Valiron)
• Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators (with B. Giles)
• Applying quantitative semantics to higher-order quantum computing (with M. Pagani and B. Valiron)
• Generators and relations for n-qubit Clifford operators
• Completely positive projections and biproducts (with C. Heunen and A. Kissinger)
• An Introduction to Quantum Programming in Quipper (with A. S. Green, P. L. Lumsdaine, N. J. Ross, and B. Valiron)
• Quipper: A Scalable Quantum Programming Language (with A. S. Green, P. L. Lumsdaine, N. J. Ross, and B. Valiron)
• Presheaf models of quantum computation: an outline (with O. Malherbe and P.J. Scott)
• Efficient Clifford+T approximation of single-qubit operators
• Exact synthesis of multiqubit Clifford+T circuits (with B. Giles)
• Quantum circuits of T-depth one
• Finite dimensional Hilbert spaces are complete for dagger compact closed categories
• Partially traced categories (with O. Malherbe and P.J. Scott)
• Autonomous categories in which A is isomorphic to A
• Quantum lambda calculus (with B. Valiron)
• A survey of graphical languages for monoidal categories
• A linear-non-linear model for a computational call-by-value lambda calculus (with B. Valiron)
• Idempotents in dagger categories
• On a fully abstract model for a quantum linear functional language (with B. Valiron)
• Tree checking for sparse complexes (with M. Caboara and S. Faridi)
• Simplicial cycles and the computation of simplicial trees (with M. Caboara and S. Faridi)
• A lambda calculus for quantum computation with classical control (with B. Valiron)
• Dagger compact closed categories and completely positive maps
• Towards a semantics for higher-order quantum computation
• A brief survey of quantum programming languages
• Towards a quantum programming language
• Some remarks on control categories
• From continuation passing style to Krivine's abstract machine
• Order-incompleteness and finite lambda reduction models
• The lambda calculus is algebraic
• Lecture notes on the lambda calculus
• Models for an adversary-centric protocol logic
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• Categorical structure of asynchrony
• A note on Bainbridge's power set construction
• My Ph.D. thesis
• First-order axioms for asynchrony
• LH has nonempty products
• My papers on the arXiv.
• The Quipper Programming Language.
• Proceedings of QPL 2015 (editor, with C. Heunen and J. Vicary).
• Proceedings of QPL 2011 (editor, with B. Jacobs and B. Spitters).
• Special issue on QPL 2010, (editor, with B. Coecke and P. Panangaden).
• Proceedings of QPL 2010 (editor, with B. Coecke and P. Panangaden).
• Proceedings of MFPS 2010 (editor, with M. Mislove).
• Proceedings of QPL 2009 (editor, with B. Coecke and P. Panangaden).
• Proceedings of DCM/QPL 2008 (editor, with B. Coecke, I. Mackie, and P. Panangaden).
• Proceedings of QPL 2006 (editor).
• Proceedings of QPL 2005 (editor).
• Special issue on QPL 2004 (editor).
• Proceedings of QPL 2004 (editor).
• Proceedings of CTCS 2002 (editor, with R. Blute).
• My compiler for the core join calculus.
• My finite lambda model applet.
• My compiler for the lambda-mu-nu calculus.

A categorical model for a quantum circuit description language

With Francisco Rios. To appear in Proceedings of the 14th International Conference on Quantum Physics and Logic (QPL 2017), Nijmegen. 12 pages, 2017.

Abstract: Quipper is a practical programming language for describing families of quantum circuits. In this paper, we formalize a small, but useful fragment of Quipper called Proto-Quipper-M. Unlike its parent Quipper, this language is type-safe and has a formal denotational and operational semantics. Proto-Quipper-M is also more general than Quipper, in that it can describe families of morphisms in any symmetric monoidal category, of which quantum circuits are but one example. We design Proto-Quipper-M from the ground up, by first giving a general categorical model of parameters and state. The distinction between parameters and state is also known from hardware description languages. A parameter is a value that is known at circuit generation time, whereas a state is a value that is known at circuit execution time. After finding some interesting categorical structures in the model, we then define the programming language to fit the model. We cement the connection between the language and the model by proving type safety, soundness, and adequacy properties.

Optimal ancilla-free Clifford+T approximation of z-rotations

With Neil J. Ross. In Quantum Information and Computation 16(11–12):901–953, 2016.

Abstract: We consider the problem of approximating arbitrary single-qubit z-rotations by ancilla-free Clifford+T circuits, up to given epsilon. We present a fast new probabilistic algorithm for solving this problem optimally, i.e., for finding the shortest possible circuit whatsoever for the given problem instance. The algorithm requires a factoring oracle (such as a quantum computer). Even in the absence of a factoring oracle, the algorithm is still near-optimal under a mild number-theoretic hypothesis. In this case, the algorithm finds a solution of T-count $$m + O(\log(\log(1/\epsilon)))$$, where m is the T-count of the second-to-optimal solution. In the typical case, this yields circuit approximations of T-count $$3\log_2(1/\epsilon) + O(\log(\log(1/\epsilon)))$$. Our algorithm is efficient in practice, and provably efficient under the above-mentioned number-theoretic hypothesis, in the sense that its expected runtime is $$O({\rm polylog}(1/\epsilon))$$.

A finite alternation result for reversible boolean circuits

16 pages. Science of Computer Programming 151:2–17, 2018.

An extended abstract of this work appeared in Proceedings of the 8th Conference on Reversible Computation (RC 2016), Bologna, Italy.Lecture Notes in Computer Science 9720:271–285, Springer, 2016.

Abstract: We say that a reversible boolean function on n bits has alternation depthd if it can be written as the sequential composition of d reversible boolean functions, each of which acts only on the top n−1 bits or on the bottom n−1 bits. Moreover, if the functions on n−1 bits are even, we speak of even alternation depth. We show that every even reversible boolean function of n ≥ 4 bits has alternation depth at most 9 and even alternation depth at most 13.

Reversible k-valued logic circuits are finitely generated for odd k

Manuscript, April 2016, 3 pages.

Abstract: In his 2003 paper "Towards an algebraic theory of Boolean circuits", Lafont notes that the class of reversible circuits over a set of k truth values is finitely generated when k is odd. He cites a private communication for the proof. The purpose of this short note is to make the content of that communication available.

Programming the quantum future

With Benoît Valiron, Neil J. Ross, D. Scott Alexander, and Jonathan M. Smith. Communications of the ACM Vol. 58 No. 8, pages 52–61, 2015.

Abstract: Quantum programming languages (QPLs) are an essential part of Quantum Computer Science. The automated translation of expressive programming languages has been of immense benefit to classical computing, permitting algorithmic complexity to be managed through abstraction and modularity; the same benefits can accrue to the emerging capabilities of quantum computing. We present both a model of quantum computation using classical control and a set of requirements for a practical QPL. Quipper is a QPL satisfying these requirements, and has been used to implement a variety of non-trivial quantum algorithms; we illustrate some of its main features with examples.

Quipper: Concrete Resource Estimation in Quantum Algorithms

With Jonathan M. Smith, Neil J. Ross, and Benoît Valiron. Extended abstract. In 12th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2014), Grenoble, France, 2014.

Abstract: Despite the rich literature on quantum algorithms, there is a surprisingly small amount of coverage of their concrete logical design and implementation. Most resource estimation is done at the level of complexity analysis, but actual concrete numbers (of quantum gates, qubits, etc.) can differ by orders of magnitude. The line of work we present here is a formal framework to write, and reason about, quantum algorithms. Specifically, we designed a language, Quipper, with scalability in mind, and we are able to report actual resource counts for seven non-trivial algorithms found in the quantum computer science literature.

Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators

With Brett Giles. December 2013, 13 pages.

Abstract: Matsumoto and Amano (2008) showed that every single-qubit Clifford+T operator can be uniquely written of a particular form, which we call the Matsumoto-Amano normal form. In this mostly expository paper, we give a detailed and streamlined presentation of Matsumoto and Amano's results, simplifying some proofs along the way. We also point out some corollaries to Matsumoto and Amano's work, including an intrinsic characterization of the Clifford+T subgroup of SO(3), which also yields an efficient T-optimal exact single-qubit synthesis algorithm. Interestingly, this also gives an alternative proof of Kliuchnikov, Maslov, and Mosca's exact synthesis result for the Clifford+T subgroup of U(2).

Applying quantitative semantics to higher-order quantum computing

With Michele Pagani and Benoît Valiron. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), San Diego, ACM SIGPLAN Notices 49(1):647–658, January 2014.

Abstract: Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this problem fell short in one way or another, either limiting the language to an unusably small finitary fragment, or giving up important features of quantum physics such as entanglement. In this paper, we propose a denotational semantics for a quantum lambda calculus with recursion and an infinite data type, using constructions from quantitative semantics of linear logic.

Generators and relations for n-qubit Clifford operators

Logical Methods in Computer Science 11(2:10):1–17, 2015.

The full proof of Proposition 7.1 is available as a supplement (105 pages): [ps, pdf] and in machine-readable form: [txt]

Abstract: We define a normal form for Clifford circuits, and we prove that every Clifford operator has a unique normal form. Moreover, we present a rewrite system by which any Clifford circuit can be reduced to normal form. This yields a presentation of Clifford operators in terms of generators and relations.

Completely positive projections and biproducts

With Chris Heunen and Aleks Kissinger. In Proceedings of the 10th International Workshop on Quantum Physics and Logic (QPL 2013), Barcelona. Electronic Proceedings in Theoretical Computer Science 171:71–83, 2014.

Abstract: The recently introduced CP*-construction unites quantum channels and classical systems, subsuming the earlier CPM-construction in categorical quantum mechanics. We compare this construction to two earlier attempts at solving this problem: freely adding biproducts to CPM, and freely splitting idempotents in CPM. The CP*-construction embeds the former, and embeds into the latter, but neither embedding is an equivalence in general.

An Introduction to Quantum Programming in Quipper

With Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, and Benoît Valiron. In Proceedings of the 5th International Conference on Reversible Computation (RC 2013), Victoria, BC, Canada. Lecture Notes in Computer Science 7948:110–124, Springer, 2013.

Abstract: Quipper is a recently developed programming language for expressing quantum computations. This paper gives a brief tutorial introduction to the language, through a demonstration of how to make use of some of its key features. We illustrate many of Quipper's language features by developing a few well known examples of Quantum computation, including quantum teleportation, the quantum Fourier transform, and a quantum circuit for addition.

Quipper: A Scalable Quantum Programming Language

With Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, and Benoît Valiron. In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI 2013), Seattle, ACM SIGPLAN Notices 48(6):333–342, June 2013.

Abstract: The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and can generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.

Presheaf models of quantum computation: an outline

With Octavio Malherbe and Philip J. Scott. In Bob Coecke, Luke Ong, Prakash Panangaden, editors, Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky. Lecture Notes in Computer Science 7860:178–194, Springer, 2013.

Abstract: This paper outlines the construction of categorical models of higher-order quantum computation. We construct a concrete denotational semantics of Selinger and Valiron's quantum lambda calculus, which was previously an open problem. We do this by considering presheaves over appropriate base categories arising from first-order quantum computation. The main technical ingredients are Day's convolution theory and Kelly and Freyd's notion of continuity of functors. We first give an abstract description of the properties required of the base categories for the model construction to work. We then exhibit a specific example of base categories satisfying these properties.

Efficient Clifford+T approximation of single-qubit operators

Quantum Information and Computation 15(1–2):159–180, 2015.

Abstract: We give an efficient randomized algorithm for approximating an arbitrary element of SU(2) by a product of Clifford+T operators, up to any given error threshold $$\epsilon>0$$. Under a mild hypothesis on the distribution of primes, the algorithm's expected runtime is polynomial in $$\log(1/\epsilon)$$. If the operator to be approximated is a z-rotation, the resulting gate sequence has T-count $$K+4\log_2(1/\epsilon)$$, where K is approximately equal to 10. We also prove a worst-case lower bound of $$K+4\log_2(1/\epsilon)$$, where K = −9, so that our algorithm is within an additive constant of optimal for certain z-rotations. For an arbitrary member of SU(2), we achieve approximations with T-count $$K+12\log_2(1/\epsilon)$$. By contrast, the Solovay-Kitaev algorithm achieves T-count $$O(\log^c(1/\epsilon))$$, where c is approximately 3.97.

Exact synthesis of multiqubit Clifford+T circuits

With Brett Giles. Physical Review A 87, 032332 (7 pages), 2013.

Abstract: We prove that a unitary matrix has an exact representation over the Clifford+T gate set with local ancillas if and only if its entries are in the ring $$\mathbb{Z}[1/\sqrt{2},i]$$. Moreover, we show that one ancilla always suffices. These facts were conjectured by Kliuchnikov, Maslov, and Mosca. We obtain an algorithm for synthesizing a exact Clifford+T circuit from any such n-qubit operator. We also characterize the Clifford+T operators that can be represented without ancillas.

Quantum circuits of T-depth one

Physical Review A 87, 042302 (4 pages), 2013.

Abstract: We give a Clifford+T representation of the Toffoli gate of T-depth 1, using four ancillas. More generally, we describe a class of circuits whose T-depth can be reduced to 1 by using sufficiently many ancillas. We show that the cost of adding an additional control to any controlled gate is at most 8 additional T-gates, and T-depth 2. We also show that the circuit THT does not possess a T-depth 1 representation with an arbitrary number of ancillas initialized to |0〉.

Finite dimensional Hilbert spaces are complete for dagger compact closed categories

Logical Methods in Computer Science 8(3:6):1–12, 2012.

A list of corrections is available: Errata.

An extended abstract of this work appeared in Proceedings of the 5th International Workshop on Quantum Physics and Logic (QPL 2008), Reykjavik.Electronic Notes in Theoretical Computer Science 270(1):113–119, Elsevier, 2011.

Abstract: We show that an equation follows from the axioms of dagger compact closed categories if and only if it holds in finite dimensional Hilbert spaces.

Partially traced categories

With Octavio Malherbe and Philip J. Scott. Journal of Pure and Applied Algebra 216(12):2563–2585, 2012.

Abstract: This paper deals with questions relating to Haghverdi and Scott's notion of partially traced categories. The main result is a representation theorem for such categories: we prove that every partially traced category can be faithfully embedded in a totally traced category. Also conversely, every symmetric monoidal subcategory of a totally traced category is partially traced, so this characterizes the partially traced categories completely. The main technique we use is based on Freyd's paracategories, along with a partial version of Joyal, Street, and Verity's Int-construction.

Autonomous categories in which $$A\cong A^*$$

Extended Abstract. In Proceedings of the 7th International Workshop on Quantum Physics and Logic (QPL 2010), Oxford, pp. 151–160, 2010.

Abstract: Recently, there has been some interest in autonomous categories (such as compact closed categories) in which the objects are self-dual, in the sense that $$A\cong A^*$$, or even $$A=A^*$$, for all objects A. In this talk, we investigate which coherence conditions should be required of such a category. We also investigate what graphical language could be used to reason about such a category.

Quantum lambda calculus

Book chapter, with Benoît Valiron. In Simon Gay and Ian Mackie, editors, Semantic Techniques in Quantum Computation, Cambridge University Press, pp. 135–172, 2009.

Abstract: We discuss the design of a typed lambda calculus for quantum computation. After a brief discussion of the role of higher-order functions in quantum information theory, we define the quantum lambda calculus and its operational semantics. Safety invariants, such as the no-cloning property, are enforced by a static type system that is based on intuitionistic linear logic. We also describe a type inference algorithm, and a categorical semantics.

A survey of graphical languages for monoidal categories

Book chapter. In Bob Coecke, editor, New Structures for Physics, Lecture Notes in Physics 813:289–355, Springer, 2011.

Abstract: This article is intended as a reference guide to various notions of monoidal categories and their associated string diagrams. It is hoped that this will be useful not just to mathematicians, but also to physicists, computer scientists, and others who use diagrammatic reasoning. We have opted for a somewhat informal treatment of topological notions, and have omitted most proofs. Nevertheless, the exposition is sufficiently detailed to make it clear what is presently known, and to serve as a starting place for more in-depth study. Where possible, we provide pointers to more rigorous treatments in the literature. Where we include results that have only been proved in special cases, we indicate this in the form of caveats.

Bibliography: Because many of the references are difficult to track down, I have created a version of the bibliography with hyperlinks: [bibliography]

A linear-non-linear model for a computational call-by-value lambda calculus

Extended Abstract, with Benoît Valiron. In Proceedings of the Eleventh International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2008), Budapest,Lecture Notes in Computer Science 4962:81–96, Springer, 2008.

A list of corrections is available: Errata.

Abstract: We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator "!" as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements. The "!" operator gives rise to a comonad, as in the linear logic models of Seely, Bierman, and Benton. The side-effects give rise to a monad, as in Moggi's computational lambda calculus. It is this combination of a monad and a comonad that makes the present paper interesting. We show that our categorical semantics is sound and complete.

Idempotents in dagger categories

Extended Abstract. In Proceedings of the 4th International Workshop on Quantum Programming Languages (QPL 2006), Oxford.Electronic Notes in Theoretical Computer Science 210:107–122, Elsevier, 2008.

Abstract: Dagger compact closed categories were studied by Abramsky and Coecke (under the name "strongly compact closed categories") as an abstract presentation of the category of Hilbert spaces and linear maps, and as a framework in which to carry out the interpretation of quantum protocols. I subsequently showed that dagger compact closed categories can also describe mixed quantum computation, where the morphisms are completely positive maps. I introduced the CPM construction as a way to pass from the pure to the mixed setting. One technical detail of the CPM(C) construction is that it does not preserve biproducts. Therefore, to obtain an interpretation of classical types such as $${\rm bit} = I\oplus I$$, one must work in the free biproduct completion $${\bf CPM}({\bf C})^{\oplus}$$. In this paper, we show that there is another view of classical types, namely as splittings of self-adjoint idempotents on quantum types. We show that all the objects of $${\bf CPM}({\bf C})^{\oplus}$$ arise as such splittings.

On a fully abstract model for a quantum linear functional language

Extended Abstract, with Benoît Valiron. In Proceedings of the 4th International Workshop on Quantum Programming Languages (QPL 2006), Oxford.Electronic Notes in Theoretical Computer Science 210:123–137, Elsevier, 2008.

Abstract: This paper studies the linear fragment of the programing language for quantum computation with classical control described in [Selinger and Valiron, 2005]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps.

Tree checking for sparse complexes

With Massimo Caboara and Sara Faridi. In Proceedings of the Second International Congress on Mathematical Software (ICMS 2006), Castro-Urdiales, Spain.Lecture Notes in Computer Science 4151:110–121, Springer, 2006.

Abstract: We detail here the sparse variant of the algorithm sketched in [CFS] for checking if a simplicial complex is a tree. A full worst case complexity analysis is given and several optimizations are discussed. The practical complexity is discussed for some examples.

Simplicial cycles and the computation of simplicial trees

With Massimo Caboara and Sara Faridi. Journal of Symbolic Computation 42:74–88, 2007.

An extended abstract of this work appeared in MEGA 2005, [ps, ps2up, pdf]

Abstract: We generalize the concept of a cycle from graphs to simplicial complexes. We show that a simplicial cycle is either a sequence of facets connected in the shape of a circle, or is a cone over such a structure. We show that a simplicial tree is a connected cycle-free simplicial complex, and use this characterization to produce an algorithm that checks in polynomial time whether a simplicial complex is a tree. We also present an efficient algorithm for checking whether a simplicial complex is grafted, and therefore Cohen-Macaulay.

A lambda calculus for quantum computation with classical control

With Benoît Valiron. Mathematical Structures in Computer Science 16(3):527–552, 2006.

An extended abstract of this work appeared in TLCA 2005 © Springer 2005. [dvi, ps, ps2up, pdf] (preprint)

Abstract: In this paper, we develop a functional programming language for quantum computers, by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the "quantum data, classical control" paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and we give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

Dagger compact closed categories and completely positive maps

Extended Abstract. In Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005), Chicago.Electronic Notes in Theoretical Computer Science 170:139–163, Elsevier, 2007.

Abstract: Dagger compact closed categories were recently introduced by Abramsky and Coecke, under the name "strongly compact closed categories", as an axiomatic framework for quantum mechanics. We present a graphical language for dagger compact closed categories, and sketch a proof of its completeness for equational reasoning. We give a general construction, the CPM construction, which associates to each dagger compact closed category its "category of completely positive maps", and we show that the resulting category is again dagger compact closed. We apply these ideas to Abramsky and Coecke's interpretation of quantum protocols, and to D'Hondt and Panangaden's predicate transformer semantics.

Towards a semantics for higher-order quantum computation

In Proceedings of the 2nd International Workshop on Quantum Programming Languages, Turku, Finland.TUCS General Publication No 33, pp. 127–143, June 2004.

An expanded version (with proofs) is also available: [ps, ps2up, pdf, pdf2up] (21 pages, corrected July 2011)

Abstract: The search for a semantics for higher-order quantum computation leads naturally to the study of categories of normed cones. In the first part of this paper, we develop the theory of continuous normed cones, and prove some of their basic properties, including a Hahn-Banach style theorem. We then describe two different concrete *-autonomous categories of normed cones. The first of these categories is built from completely positive maps as in the author's semantics of first-order quantum computation. The second category is a reformulation of Girard's quantum coherent spaces. We also point out why ultimately, neither of these categories is a satisfactory model of higher-order quantum computation.

Towards a quantum programming language

Mathematical Structures in Computer Science 14(4):527–586, 2004.

Abstract: We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and it has an interesting denotational semantics in terms of complete partial orders of superoperators.

Some remarks on control categories

Manuscript, June 2003, 17 pages.

Abstract: This paper is a collection of remarks on control categories, including answers to some frequently asked questions. The paper is not self-contained and must be read in conjunction with Control Categories and Duality. We clarify the definition of response categories, and show that most of the conditions can be dropped. In particular, the requirement of having finite sums can be dropped, leading to an interesting new CPS translation of the lambda-mu-calculus. We discuss the choice of left-to-right vs. right-to-left evaluation in the call-by-value lambda calculus, an issue which is sometimes misunderstood because it is a purely syntactical issue which is not reflected semantically. We clarify the relationships between various alternative formulations of disjunction types and conjunction types, which coincide in call-by-value but differ in call-by-name. We prove that copyable and discardable maps are not always central, and we characterize those control categories of the form $$R^{\bf Set}$$ for which copyable and discardable implies central. We prove that any control category with initial object is a preorder.

From continuation passing style to Krivine's abstract machine

Manuscript, May 2003, 23 pages.

Abstract: We describe, for three different extensions of typed lambda calculus, how the rules for a version of Krivine's abstract machine can be derived from those of continuation passing style (CPS) semantics. The three extensions are: Parigot's $$\lambda\mu$$-calculus, Pym and Ritter's $$\lambda\mu\nu$$-calculus, and an extension of the call-by-name lambda calculus with built-in types and primitive functions. We also show how Krivine's abstract machine can be implemented on realistic hardware by compiling it into an idealized assembly language.

Order-incompleteness and finite lambda reduction models

Theoretical Computer Science 309(1):43–63, 2003.

An extended abstract of this work appeared in LICS'96, © 1996 IEEE. [ps, pdf]

Abstract: Many familiar models of the untyped lambda calculus are constructed by order theoretic methods. This paper provides some basic new facts about ordered models of the lambda calculus. We show that in any partially ordered model that is complete for the theory of $$\beta$$- or $$\beta\eta$$-conversion, the partial order is trivial on term denotations. Equivalently, the open and closed term algebras of the untyped lambda calculus cannot be non-trivially partially ordered. Our second result is a syntactical characterization, in terms of so-called generalized Mal'cev operators, of those lambda theories which cannot be induced by any non-trivially partially ordered model. We also consider a notion of finite models for the untyped lambda calculus, or more precisely, finite models of reduction. We demonstrate how such models can be used as practical tools for giving finitary proofs of term inequalities.

The lambda calculus is algebraic

Journal of Functional Programming 12(6):549–566, 2002.

Abstract: This paper serves as a self-contained, tutorial introduction to combinatory models of the untyped lambda calculus. We focus particularly on the interpretation of free variables. We argue that free variables should not be interpreted as elements in a model, as is usually done, but as indeterminates. We claim that the resulting interpretation is more natural and leads to a closer correspondence between models and theories. In particular, it solves the problem of the notorious $$\xi$$-rule, which asserts that equations should be preserved under binders, and which fails to be sound for the usual interpretation.

Lecture notes on the lambda calculus

Expository course notes. 2001–2013. 120 pages.

Abstract: This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007 and 2013. Topics covered in these notes include the untyped lambda calculus, the Church-Rosser theorem, combinatory algebras, the simply-typed lambda calculus, the Curry-Howard isomorphism, weak and strong normalization, polymorphism, type inference, denotational semantics, complete partial orders, and the language PCF.

Models for an adversary-centric protocol logic

In Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification, Electronic Notes in Theoretical Computer Science 55(1):69–84, Elsevier, 2001.

Abstract: In this paper, we propose an adversary-centric, logical framework for formalizing cryptographic protocols. The formalism is inspired by the work of Compton and Dexter and of Cervesato et al., but we do not focus on proof search, but instead on logical validity. A novel contribution of this paper is a technique for giving very short proofs of protocol correctness through models of first-order logic.

Control categories and duality: on the categorical semantics of the lambda-mu calculus

Mathematical Structures in Computer Science 11(2):207–260, 2001.

Abstract: We give a categorical semantics to the call-by-name and call-by-value versions of Parigot's $$\lambda\mu$$-calculus with disjunction types. We introduce the class of control categories, which combine a cartesian-closed structure with a premonoidal structure in the sense of Power and Robinson. We prove, via a categorical structure theorem, that the categorical semantics is equivalent to a CPS semantics in the style of Hofmann and Streicher. We show that the call-by-name $$\lambda\mu$$-calculus forms an internal language for control categories, and that the call-by-value $$\lambda\mu$$-calculus forms an internal language for the dual co-control categories. As a corollary, we obtain a syntactic duality result: there exist syntactic translations between call-by-name and call-by-value which are mutually inverse and which preserve the operational semantics. This answers a question of Streicher and Reus.

Categorical structure of asynchrony

In Proceedings of MFPS 15.Electronic Notes in Theoretical Computer Science 20:158–181, Elsevier, 1999.

Abstract: We investigate a categorical framework for the semantics of asynchronous communication in networks of parallel processes. Abstracting from a category of asynchronous labeled transition systems, we formulate the notion of a categorical model of asynchrony as a uniformly traced monoidal category with diagonals, such that every morphism is total and the focus is equivalent to a category of complete partial orders. We present a simple, non-deterministic, cpo-based model that satisfies these requirements, and we discuss how to refine this model by an observational congruence. We also present a general construction of passing from deterministic to non-deterministic models, and more generally, from non-linear to linear structure on a category.

A note on Bainbridge's power set construction

Manuscript. May 1998. 10 pages.

Abstract: The category Rel of sets and relations has two natural traced monoidal structures: in (Rel,+,Tr), the tensor is given by disjoint union, and in (Rel,×,Tr') by products of sets. Already in 1976, predating the definition of traced monoidal categories by 20 years, Bainbridge has shown how to model flowcharts and networks in these two respective settings. Bainbridge has also pointed out that one can move from one setting to the other via the power set operation. However, Bainbridge's power operation is not functorial, and in this paper we show that there is no traced monoidal embedding of (Rel,+,Tr) into (Rel,×,Tr') whose object part is given by the power set operation. On the other hand, we show that there is such an embedding whose object part is given by the power-multiset operation.

Functionality, polymorphism, and concurrency:a mathematical investigation of programming paradigms

Ph.D. Thesis, University of Pennsylvania. June 1997. 129 pages. Appeared as IRCS Technical Report 97-17.

A list of corrections is available: Errata.

Abstract: The search for mathematical models of computational phenomena often leads to problems that are of independent mathematical interest. Selected problems of this kind are investigated in this thesis. First, we study models of the untyped lambda calculus. Although many familiar models are constructed by order-theoretic methods, it is also known that there are some models of the lambda calculus that cannot be non-trivially ordered. We show that the standard open and closed term algebras are unorderable. We characterize the absolutely unorderable T-algebras in any algebraic variety T. Here an algebra is called absolutely unorderable if it cannot be embedded in an orderable algebra. We then introduce a notion of finite models for the lambda calculus, contrasting the known fact that models of the lambda calculus, in the traditional sense, are always non-recursive. Our finite models are based on Plotkin's syntactical models of reduction. We give a method for constructing such models, and some examples that show how finite models can yield useful information about terms. Next, we study models of typed lambda calculi. Models of the polymorphic lambda calculus can be divided into environment-style models, such as Bruce and Meyer's non-strict set-theoretic models, and categorical models, such as Seely's interpretation in PL-categories. Reynolds has shown that there are no set-theoretic strict models. Following a different approach, we investigate a notion of non-strict categorical models. These provide a uniform framework in which one can describe various classes of non-strict models, including set-theoretic models with or without empty types, and Kripke-style models. We show that completeness theorems correspond to categorical representation theorems, and we reprove a completeness result by Meyer et al. on set-theoretic models of the simply-typed lambda calculus with possibly empty types. Finally, we study properties of asynchronous communication in networks of communicating processes. We formalize several notions of asynchrony independently of any particular concurrent process paradigm. A process is asynchronous if its input and/or output is filtered through a communication medium, such as a buffer or a queue, possibly with feedback. We prove that the behavior of asynchronous processes can be equivalently characterized by first-order axioms.

First-order axioms for asynchrony

In Proceedings of CONCUR '97, Lecture Notes in Computer Science 1243:376–390, Springer, 1997.

An expanded version is also available: [ps, pdf] (21 pages)

Abstract: We study properties of asynchronous communication independently of any concrete concurrent process paradigm. We give a general-purpose, mathematically rigorous definition of several notions of asynchrony in a natural setting where an agent is asynchronous if its input and/or output is filtered through a buffer or a queue, possibly with feedback. In a series of theorems, we give necessary and sufficient conditions for each of these notions in the form of simple first-order or second-order axioms. We illustrate the formalism by applying it to asynchronous CCS and the core join calculus.