With a Few Square Roots, Quantum Computing is as Easy as Pi
Rig groupoids provide a semantic model of Π, a universal classical reversible programming language over finite types. We prove that extending rig groupoids with just two maps and three equations about them results in a model of quantum computing that is computationally universal and equationally sound and complete for a variety of gate sets. The first map corresponds to an 8th root of the identity morphism on the unit 1. The second map corresponds to a square root of the symmetry on 1+1. As square roots are generally not unique and can sometimes even be trivial, the maps are constrained to satisfy a nondegeneracy axiom, which we relate to the Euler decomposition of the Hadamard gate. The semantic construction is turned into an extension of Π, called √Π, that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to ≤2 qubits, and the computationally universal Gaussian Clifford+T gate set.
Thu 18 JanDisplayed time zone: London change
13:40 - 15:00 | |||
13:40 20mTalk | With a Few Square Roots, Quantum Computing is as Easy as Pi POPL Jacques Carette McMaster University, Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Southern Denmark, Amr Sabry Indiana University Pre-print | ||
14:00 20mTalk | Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers POPL Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy | ||
14:20 20mTalk | SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog CompilationRemote POPL Yuxiang Peng University of Maryland, Jacob Young University of Maryland, Pengyu Liu Tsinghua University, Xiaodi Wu University of Maryland | ||
14:40 20mTalk | Enriched Presheaf Model of Quantum FPC POPL |