arXiv subjects
Publications and source records attributed to Peter Selinger.
We present a simple construction of hat tilings. The construction can be carried out by superimposing a triangular grid on a specially colored image and reading off the orientation of the tiles. We show that our construction produces valid hat tilings, and conversely, in an appropriate sense that is made precise in the paper, that every valid hat tiling can be obtained in this way.
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.
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).
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.
The quantum programming language Quipper supports circuit operations such as reversing and controlling certain quantum circuits. Additionally, Quipper provides a function called with-computed, which can be used to program circuits of the form g; f; g-dagger. The latter is a common pattern in quantum circuit design. One benefit of using with-computed, as opposed to constructing the circuit g ; f; g-dagger directly from g, f, and g-dagger, is that it facilitates an important optimization. Namely, if the resulting circuit is later controlled, only f needs to be controlled; the circuits g and g-dagger need not even be controllable. In this paper, we formalize a semantics for reversible and controllable circuits, using a dagger symmetric monoidal category R to interpret reversible circuits, and a new notion we call a controllable category N, which encompasses the control and with-computed operations in Quipper. We extend the language Proto-Quipper with reversing, control and the with-computed operation. Since not all circuits are reversible and/or controllable, we use a type system with modalities to track reversibility and controllability. This generalizes the modality of Fu-Kishida-Ross-Selinger 2023. We give an abstract categorical semantics, and show that the type system and operational semantics are sound with respect to this semantics.
We answer the question: what is the longest winning path on a Hex board of size $n\times n$?
We provide three improvements to the product formula implementation of the ground state energy estimation algorithm via Trotter-Suzuki decomposition. These consist of smaller circuit templates for each Hamiltonian term, parallelization of commuting controlled rotations, and more efficient parallel scheduling. These improvements may be regarded separately, and we anticipate that they may be combined with other improvements to the product formula implementation.
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.
We give a presentation by generators and relations of the group of 3-qubit Clifford+CS operators. The proof roughly consists of two parts: (1) applying the Reidemeister-Schreier theorem recursively to an earlier result of ours; and (2) the simplification of thousands of relations into 17 relations. Both (1) and (2) have been formally verified in the proof assistant Agda. The Reidemeister-Schreier theorem gives a constructive method for computing a presentation of a sub-monoid given a presentation of the super-monoid. To achieve (2), we devise an almost-normal form for Clifford+CS operators. Along the way, we also identify several interesting structures within the Clifford+CS group. Specifically, we identify three different finite subgroups for whose elements we can give unique normal forms. We show that the 3-qubit Clifford+CS group, which is of course infinite, is the amalgamated product of these three finite subgroups. This result is analogous to the fact that the 1-qubit Clifford+T group is an amalgamated product of two finite subgroups.
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.
Quipper is a functional programming language for quantum computing. Proto-Quipper is a family of languages aiming to provide a formal foundation for Quipper. In this paper, we extend Proto-Quipper-M with a construct called dynamic lifting, which is present in Quipper. By virtue of being a circuit description language, Proto-Quipper has two separate runtimes: circuit generation time and circuit execution time. Values that are known at circuit generation time are called parameters, and values that are known at circuit execution time are called states. Dynamic lifting is an operation that enables a state, such as the result of a measurement, to be lifted to a parameter, where it can influence the generation of the next portion of the circuit. As a result, dynamic lifting enables Proto-Quipper programs to interleave classical and quantum computation. We describe the syntax of a language we call Proto-Quipper-Dyn. Its type system uses a system of modalities to keep track of the use of dynamic lifting. We also provide an operational semantics, as well as an abstract categorical semantics for dynamic lifting based on enriched category theory. We prove that both the type system and the operational semantics are sound with respect to our categorical semantics. Finally, we give some examples of Proto-Quipper-Dyn programs that make essential use of dynamic lifting.
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.
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.
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.
The class of passable games was recently introduced by Selinger as a class of combinatorial games that are suitable for modelling monotone set coloring games such as Hex. In a monotone set coloring game, the players alternately color the cells of a board with their respective color, and the winner is determined by a monotone function of the final position. It is easy to see that every monotone set coloring game is a passable combinatorial game. Here we prove the converse: every passable game is realizable, up to equivalence, as a monotone set coloring game.
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.
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.
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].