![[home]](images/PS05.gif){kind=small}
See also:
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.
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.
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)
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:
