Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
It is well-known that the category of presheaf functors is complete and cocomplete, and that the Yoneda embedding into the presheaf category preserves products. However, the Yoneda embedding does not preserve coproducts. It is perhaps less well-known that if we restrict the codomain of the Yoneda embedding to the full subcategory of limit-preserving functors, then this embedding preserves colimits, while still enjoying most of the other useful properties of the Yoneda embedding. We call this modified embedding the Lambek embedding. The category of limit-preserving functors is known to be a reflective subcategory of the category of all functors, i.e., there is a left adjoint for the inclusion functor. In the literature, the existence of this left adjoint is often proved non-constructively, e.g., by an application of Freyd's adjoint functor theorem. In this paper, we provide an alternative, more constructive proof of this fact. We first explain the Lambek embedding and why it preserves coproducts. Then we review some concepts from multi-sorted algebras and observe that there is a one-to-one correspondence between product-preserving presheaves and certain multi-sorted term algebras. We provide a construction that freely turns any presheaf functor into a product-preserving one, hence giving an explicit definition of the left adjoint functor of the inclusion. Finally, we sketch how to extend our method to prove that the subcategory of limit-preserving functors is also reflective.
Brett Giles, Peter Selinger
Dec 23, 2013·quant-ph·PDF 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).
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.
Peter Selinger
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.
Eric Demer, Peter Selinger
This paper is about 3-terminal regions in Hex. A 3-terminal region is a region of the Hex board that is completely surrounded by black and white stones, in such a way that the black boundary stones form 3 connected components. We characterize Hex as the universal planar Shannon game of degree 3. This ensures that every Hex position can be decomposed into 3-terminal regions. We then investigate the combinatorial game theory of 3-terminal regions. We show that there are infinitely many distinct Hex-realizable values for such regions. We introduce an infinite family of 3-terminal positions called superswitches and investigate their properties. We also present a database of Hex-realizable 3-terminal values, and illustrate its utility as a problem-solving tool by giving various applications. The applications include the automated verification of connects-both templates and pivoting templates, a new handicap strategy for $11\times 11$ Hex, and a method for constructing witnesses for the non-inferiority of probes in many Hex templates. These methods allow us to disprove a conjecture by Henderson and Hayward.
Peter Selinger
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.
Peter Selinger
Dec 26, 2012·quant-ph·PDF 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\log_2(1/ε)$, where $K$ is approximately equal to $10$. We also prove a worst-case lower bound of $K+4\log_2(1/ε)$, 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/ε)$. By contrast, the Solovay-Kitaev algorithm achieves $T$-count $O(\log^c(1/ε))$, where $c$ is approximately $3.97$.
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger
Quipper and Proto-Quipper are a family of quantum programming languages that, by their nature as circuit description languages, involve two runtimes: one at which the program generates a circuit and one at which the circuit is executed, normally with probabilistic results due to measurements. Accordingly, the language distinguishes two kinds of data: parameters, which are known at circuit generation time, and states, which are known at circuit execution time. Sometimes, it is desirable for the results of measurements to control the generation of the next part of the circuit. Therefore, the language needs to turn states, such as measurement outcomes, into parameters, an operation we call dynamic lifting. The goal of this paper is to model this interaction between the runtimes by providing a general categorical structure enriched in what we call "bisets". We demonstrate that the biset-enriched structure achieves a proper semantics of the two runtimes and their interaction, by showing that it models a variant of Proto-Quipper with dynamic lifting. The present paper deals with the concrete categorical semantics of this language, whereas a companion paper deals with the syntax, type system, operational semantics, and abstract categorical semantics.
Sarah Meng Li, Neil J. Ross, Peter Selinger
We give a finite presentation by generators and relations for the group O_n(Z[1/2]) of n-dimensional orthogonal matrices with entries in Z[1/2]. We then obtain a similar presentation for the group of n-dimensional orthogonal matrices of the form M/sqrt(2)^k, where k is a nonnegative integer and M is an integer matrix. Both groups arise in the study of quantum circuits. In particular, when the dimension is a power of 2, the elements of the latter group are precisely the unitary matrices that can be represented by a quantum circuit over the universal gate set consisting of the Toffoli gate, the Hadamard gate, and the computational ancilla.
Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, Benoît Valiron
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.
Ethan J. Saunders, Peter Selinger
The game of Paintbucket was recently introduced by Amundsen and Erickson. It is played on a rectangular grid of black and white pixels. The players alternately fill in one of their opponent's connected components with their own color, until the entire board is just a single color. The player who makes the last move wins. It is not currently known whether there is a simple winning strategy for Paintbucket. In this paper, we consider a natural generalization of Paintbucket that is played on an arbitrary simple graph, and we show that the problem of determining the winner in a given position of this generalized game is PSPACE-complete.
Peter Selinger
We answer the question: what is the longest winning path on a Hex board of size $n\times n$?
Aaron David Fairbanks, Peter Selinger
Traced monoidal categories are used to model processes that can feed their outputs back to their own inputs, abstracting iteration. The category of finite dimensional Hilbert spaces with the direct sum tensor is not traced. But surprisingly, in 2014, Bartha showed that the monoidal subcategory of isometries is traced. The same holds for coisometries, unitary maps, and contractions. This suggests the possibility of feeding outputs of quantum processes back to their own inputs, analogous to iteration. In this paper, we show that Bartha's result is not specifically tied to Hilbert spaces, but works in any dagger additive category with Moore-Penrose pseudoinverses (a natural dagger-categorical generalization of inverses).
Peng Fu, Peter Selinger
A well-known problem in the theory of dependent types is how to handle so-called nested data types. These data types are difficult to program and to reason about in total dependently typed languages such as Agda and Coq. In particular, it is not easy to derive a canonical induction principle for such types. Working towards a solution to this problem, we introduce dependently typed folds for nested data types. Using the nested data type Bush as a guiding example, we show how to derive its dependently typed fold and induction principle. We also discuss the relationship between dependently typed folds and the more traditional higher-order folds.
Xiaoning Bian, Peter Selinger
We give a presentation by generators and relations of the group of Clifford+T operators on two qubits. The proof relies on an application of the Reidemeister-Schreier theorem to an earlier result of Greylyn, and has been formally verified in the proof assistant Agda.
Eric Demer, Peter Selinger
A notion of combinatorial game over a partially ordered set of atomic outcomes was recently introduced by Selinger. These games are appropriate for describing the value of positions in Hex and other monotone set coloring games. It is already known that there are infinitely many distinct monotone game values when the poset of atoms is not linearly ordered, and that there are only finitely many such values when the poset of atoms is linearly ordered with 4 or fewer elements. In this short paper, we settle the remaining case: when the atom poset has 5 or more elements, there are infinitely many distinct monotone values.
Brett Giles, Peter Selinger
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 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.
Neil J. Ross, Peter Selinger
Mar 12, 2014·quant-ph·PDF 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 3log_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(polylog(1/epsilon)).
Octavio Malherbe, Philip J. Scott, Peter Selinger
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.
Peng Fu, Peter Selinger
We present an approach to develop folds for nested data types using dependent types. We call such folds $\textit{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 $\textit{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.