![[home]](images/PS05.gif){kind=small}
The references are also available in BibTeX format.
See also:
Abstract: Chen and Risen pointed out a logical flaw affecting the conclusions of a number of past experiments that used the free-choice paradigm to measure choice-induced attitude change. They went on to design and implement a free-choice experiment that used a novel type of control group in order to avoid this logical pitfall. In this paper, we describe a method by which a free-choice experiment can be correctly conducted even without a control group.
Abstract: We present an approach to develop folds for nested data types using dependent types. We call such folds dependently typed folds. They have the following properties. (1) Dependently typed folds are defined by well-founded recursion and they can be defined in a total dependently typed language. (2) Dependently typed folds do not depend on maps. Map functions and many terminating functions can be defined using dependently typed folds. (3) The induction principles for nested data types follow from the definitions of dependently typed folds and the programs defined by dependently typed folds can be formally verified. (4) Dependently typed folds exist for any nested data types and they can be specialized to the traditional higher-order folds. Using various of examples, we show how to program and reason about dependently typed folds. We also show how to obtain dependently typed folds in general and how to specialize them to the corresponding higher-order folds.
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.
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))\).
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 depth d if it can be written as the
sequential composition of d reversible boolean functions, each
of which acts only on the top
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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
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.
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〉.
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.
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.
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.
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.
© 2009 Published by Cambridge University Press.
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 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.
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.
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.
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.
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.
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.
© 2006 Peter Selinger, Benoît Valiron. Published by Cambridge University Press.
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.
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.
Abstract: This article is a brief and subjective survey of quantum programming language research.
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.
© 2004 Published by Cambridge University Press.
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.
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.
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.
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.
Download: [ps, ps2up, pdf, pdf2up, arXiv]
These notes are also available in book form.
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.
Download: [ps, ps2up, pdf, pdf2up] (preprint)
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.
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.
© 2001 Published by Cambridge University Press.
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.
© 1999 Published by
Abstract: The category Rel of sets and relations has two
natural traced monoidal structures: in
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.
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.
Abstract: We show that LH, the category of
topological spaces with local homeomorphisms, has binary
products. This has been previously believed to be false.
Back to Homepage:
![[home]](images/homebutton.gif)