arXiv subjects

Peter Selinger

Publications and source records attributed to Peter Selinger.

At least 37 records · Page 2Linked to original sources

arXiv2021

Generators and Relations for the Group On(Z[1/2])

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.

quant-ph↗

arXiv2021

Generators and Relations for Real Stabilizer Operators

Real stabilizer operators, which are also known as real Clifford operators, are generated, through composition and tensor product, by the Hadamard gate, the Pauli Z gate, and the controlled-Z gate. We introduce a normal form for real stabilizer circuits and show that every real stabilizer operator admits a unique normal form. Moreover, we give a finite set of relations that suffice to rewrite any real stabilizer circuit to its normal form.

quant-ph↗

arXiv2021

Generators and Relations for Un(Z[1/2,i])

Consider the universal gate set for quantum computing consisting of the gates X, CX, CCX, omega^dagger H, and S. All of these gates have matrix entries in the ring Z[1/2,i], the smallest subring of the complex numbers containing 1/2 and i. Amy, Glaudell, and Ross proved the converse, i.e., any unitary matrix with entries in Z[1/2,i] can be realized by a quantum circuit over the above gate set using at most one ancilla. In this paper, we give a finite presentation by generators and relations of U_n(Z[1/2,i]), the group of unitary nxn-matrices with entries in Z[1/2,i].

quant-ph↗

arXiv2020

A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper

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.

cs.PL↗

arXiv2019

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

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).

quant-ph↗

arXiv2019

Proceedings of the 15th International Conference on Quantum Physics and Logic

Quantum Physics and Logic is an annual conference that brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behaviour in general. Work that applies structures and methods inspired by quantum theory to other fields (including computer science) is also welcome.

quant-ph↗

arXiv2018

On the mathematics of the free-choice paradigm

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.

stat.OT↗

arXiv2018

Dependently Typed Folds for Nested Data Types

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.

cs.LO↗

arXiv2018

A Categorical Model for a Quantum Circuit Description Language (Extended 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.

quant-ph↗

arXiv2017

A finite alternation result for reversible boolean circuits

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 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.

cs.ET↗

arXiv2017

Generators and relations for n-qubit Clifford operators

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.

quant-ph↗

arXiv2016

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

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)).

quant-ph↗

arXiv2016

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

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.

cs.ET↗

arXiv2015

Proceedings 12th International Workshop on Quantum Physics and Logic

This volume contains the proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL 2015), which was held July 15-17, 2015 at Oxford University. The goal of this workshop series is to bring together researchers working on mathematical foundations of quantum physics, quantum computing, spatio-temporal causal structures, and related areas such as computational linguistics. Of particular interest are topics that use logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods and other computer science methods for the study of physical behaviour in general.

quant-ph↗

arXiv2014

Completely positive projections and biproducts

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.

math.CT↗

arXiv2014

Quipper: Concrete Resource Estimation in Quantum Algorithms

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.

cs.PL↗

arXiv2014

Efficient Clifford+T approximation of single-qubit operators

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$.

quant-ph↗

arXiv2013

Lecture notes on the lambda calculus

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.

cs.LO↗