![[home]](images/PS05.gif){kind=small}
See also:
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 ε >
0. Under a mild hypothesis on the distribution of primes, the
algorithm's expected runtime is polynomial in log(1/ε). If the
operator to be approximated is a z-rotation, the resulting gate
sequence has T-count K + 4 log2(1/ε),
where K is approximately equal to 11. We also prove a
worst-case lower bound of K' + 4 log2(1/ε),
where K' = −9, so that our algorithm is within an
additive constant of optimal for z-rotations. For an arbitrary
member of SU(2), we achieve approximations with T-count
3K+12 log2(1/ε). By contrast, the
Solovay-Kitaev algorithm achieves T-count
O(log
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 ℤ[1/√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〉.
An extended abstract of this work appeared in Proceedings of the 5th International Workshop on Quantum Physics and Logic (QPL 2008), Reykjavik. ENTCS 270(1):113-119, 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 is isomorphic to
A
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.
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 bit = 
I. 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
CPM(C) 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: [dvi, ps, ps2up, pdf] (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
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. [dvi, 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: [dvi, ps, ps2up, pdf, pdf2up]
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. 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, type inference, denotational semantics, complete partial orders, and the language PCF.
Download: [dvi, ps, ps2up, pdf] (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 
-calculus-calculus-calculus
© 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 (Rel,+,Tr), the tensor is given by disjoint union, and in (Rel,x,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,x,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.
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: [dvi, 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:
