-
Compositional Reversible Computation
Authors:
Jacques Carette,
Chris Heunen,
Robin Kaarsgaard,
Amr Sabry
Abstract:
Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible computation. We start from a historical perspective, by reviewing those approaches that developed reversible extensions of lambda-calculi, Turing machines, and com…
▽ More
Reversible computing is motivated by both pragmatic and foundational considerations arising from a variety of disciplines. We take a particular path through the development of reversible computation, emphasizing compositional reversible computation. We start from a historical perspective, by reviewing those approaches that developed reversible extensions of lambda-calculi, Turing machines, and communicating process calculi. These approaches share a common challenge: computations made reversible in this way do not naturally compose locally.
We then turn our attention to computational models that eschew the detour via existing irreversible models. Building on an original analysis by Landauer, the insights of Bennett, Fredkin, and Toffoli introduced a fresh approach to reversible computing in which reversibility is elevated to the status of the main design principle. These initial models are expressed using low-level bit manipulations, however.
Abstracting from the low-level of the Bennett-Fredkin-Toffoli models and pursuing more intrinsic, typed, and algebraic models, naturally leads to rig categories as the canonical model for compositional reversible programming. The categorical model reveals connections to type isomorphisms, symmetries, permutations, groups, and univalent universes. This, in turn, paves the way for extensions to reversible programming based on monads and arrows. These extensions are shown to recover conventional irreversible programming, a variety of reversible computational effects, and more interestingly both pure (measurement-free) and measurement-based quantum programming.
△ Less
Submitted 31 May, 2024;
originally announced May 2024.
-
With a Few Square Roots, Quantum Computing is as Easy as Π
Authors:
Jacques Carette,
Chris Heunen,
Robin Kaarsgaard,
Amr Sabry
Abstract:
Rig groupoids provide a semantic model of \PiLang, 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 $8^{\text{th}}$ ro…
▽ More
Rig groupoids provide a semantic model of \PiLang, 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 $8^{\text{th}}$ 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 \PiLang, called \SPiLang, 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 $\le 2$ qubits, and the computationally universal Gaussian Clifford+T gate set.
△ Less
Submitted 21 October, 2023;
originally announced October 2023.
-
The Quantum Effect: A Recipe for QuantumPi
Authors:
Jacques Carette,
Chris Heunen,
Robin Kaarsgaard,
Amr Sabry
Abstract:
Free categorical constructions characterise quantum computing as the combination of two copies of a reversible classical model, glued by the complementarity equations of classical structures. This recipe effectively constructs a computationally universal quantum programming language from two copies of Pi, the internal language of rig groupoids. The construction consists of Hughes' arrows. Thus ans…
▽ More
Free categorical constructions characterise quantum computing as the combination of two copies of a reversible classical model, glued by the complementarity equations of classical structures. This recipe effectively constructs a computationally universal quantum programming language from two copies of Pi, the internal language of rig groupoids. The construction consists of Hughes' arrows. Thus answer positively the question whether a computational effect exists that turns reversible classical computation into quantum computation: the quantum effect. Measurements can be added by layering a further effect on top. Our construction also enables some reasoning about quantum programs (with or without measurement) through a combination of classical reasoning and reasoning about complementarity.
△ Less
Submitted 8 May, 2023; v1 submitted 3 February, 2023;
originally announced February 2023.
-
A Novel Power-optimized CMOS sEMG Device with Ultra Low-noise integrated with ConvNet (VGG16) for Biomedical Applications
Authors:
Ahmed Ayman - Mohamed Sabry
Abstract:
The needle bio-potential sensors for measuring muscle and brain activity need invasive surgical targeted muscle reinnervation (TMR) and a demanding process to maintain, but surface bio-potential sensors lack clear bio-signal reading (Signal-Interference). In this research, a novel power-optimized complementary metal-oxide-semiconductor (CMOS) Surface Electromyography (sEMG) is developed to improve…
▽ More
The needle bio-potential sensors for measuring muscle and brain activity need invasive surgical targeted muscle reinnervation (TMR) and a demanding process to maintain, but surface bio-potential sensors lack clear bio-signal reading (Signal-Interference). In this research, a novel power-optimized complementary metal-oxide-semiconductor (CMOS) Surface Electromyography (sEMG) is developed to improve the efficiency and quality of captured bio-signal for biomedical application: The early diagnosis of neurological disorders (Dystonia) and a novel compatible mind-controlled prosthetic leg with human daily activities. A novel sEMG composed of CMOS Op-Amp based PIC16F877A 8-bit CMOS Flash-based Microcontroller is utilized to minimize power consumption and data processing time. sEMG Circuit is implemented with developed analog filter along with infinite impulse response (IIR) digital filter via Fast Fourier Transform (FFT), Z-transform, and difference equations. The analysis shows a significant improvement of 169.2% noise-reduction in recorded EMG signal using developed digital filter compared to analog one according to numerical root mean square error (RMSE). Moreover, digital IIR was tested in two stages: algorithmic and real-world. As a result, IIR's algorithmic (MATLAB) and real-world RMSEs were 0.03616 and 0.05224, respectively. A notable advancement of 20.8% in data processing duration in EMG signal analysis. Optimizing VGG, AlexNet, and ResNet ConvNet as trained and tested on 15 public EEG (62-electrode) and 18 subjects' observed EMG data. The results indicate that VGG16-1D is 98.43% higher. During real testing, the accuracy was 95.8 +/- 4.6% for 16 subjects (6 Amputees-10 Dystonia). This study demonstrates the potential for sEMG, paving the way for biomedical applications.
△ Less
Submitted 10 May, 2023; v1 submitted 3 January, 2023;
originally announced January 2023.
-
A Synthesis of Hidden Subgroup Quantum Algorithms and Quantum Chemical Dynamics
Authors:
Srinivasan S. Iyengar,
Anup Kumar,
Debadrita Saha,
Amr Sabry
Abstract:
We describe a general formalism for quantum dynamics and show how this formalism subsumes several quantum algorithms including the Deutsch, Deutsch-Jozsa, Bernstein-Vazirani, Simon, and Shor algorithms as well as the conventional approach to quantum dynamics based on tensor networks. The common framework exposes similarities among quantum algorithms and natural quantum phenomena: we illustrate thi…
▽ More
We describe a general formalism for quantum dynamics and show how this formalism subsumes several quantum algorithms including the Deutsch, Deutsch-Jozsa, Bernstein-Vazirani, Simon, and Shor algorithms as well as the conventional approach to quantum dynamics based on tensor networks. The common framework exposes similarities among quantum algorithms and natural quantum phenomena: we illustrate this connection by showing how the correlated behavior of protons in water wire systems that are common in many biological and materials systems parallels the structure of Shor's algorithm.
△ Less
Submitted 25 December, 2022;
originally announced December 2022.
-
Retrodictive Quantum Computing
Authors:
Jacques Carette,
Gerardo Ortiz,
Amr Sabry
Abstract:
Quantum models of computation are widely believed to be more powerful than classical ones. Efforts center on proving that, for a given problem, quantum algorithms are more resource efficient than any classical one. All this, however, assumes a standard predictive paradigm of reasoning where, given initial conditions, the future holds the answer. How about bringing information from the future to th…
▽ More
Quantum models of computation are widely believed to be more powerful than classical ones. Efforts center on proving that, for a given problem, quantum algorithms are more resource efficient than any classical one. All this, however, assumes a standard predictive paradigm of reasoning where, given initial conditions, the future holds the answer. How about bringing information from the future to the present and exploit it to one's advantage? This is a radical new approach for reasoning, so-called Retrodictive Computation, that benefits from the specific form of the computed functions. We demonstrate how to use tools of symbolic computation to realize retrodictive quantum computing at scale and exploit it to efficiently, and classically, solve instances of the quantum Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms.
△ Less
Submitted 12 May, 2022;
originally announced May 2022.
-
Quantum Computation of Hydrogen Bond Dynamics and Vibrational Spectra
Authors:
Philip Richerme,
Melissa C. Revelle,
Debadrita Saha,
Miguel Angel Lopez-Ruiz,
Anurag Dwivedi,
Sam A. Norrell,
Christopher G. Yale,
Daniel Lobser,
Ashlyn D. Burch,
Susan M. Clark,
Jeremy M. Smith,
Amr Sabry,
Srinivasan S. Iyengar
Abstract:
Calculating the observable properties of chemical systems is often classically intractable and is widely viewed as a promising application of quantum information processing. Yet one of the most common and important chemical systems in nature - the hydrogen bond - has remained a challenge to study using quantum hardware on account of its anharmonic potential energy landscape. Here, we introduce a f…
▽ More
Calculating the observable properties of chemical systems is often classically intractable and is widely viewed as a promising application of quantum information processing. Yet one of the most common and important chemical systems in nature - the hydrogen bond - has remained a challenge to study using quantum hardware on account of its anharmonic potential energy landscape. Here, we introduce a framework for solving hydrogen-bond systems and more generic chemical dynamics problems using quantum logic. We experimentally demonstrate a proof-of-principle instance of our method using the QSCOUT ion-trap quantum computer, in which we experimentally drive the ion-trap system to emulate the quantum wavepacket of the shared-proton within a hydrogen bond. Following the experimental creation of the shared-proton wavepacket, we then extract measurement observables such as its time-dependent spatial projection and its characteristic vibrational frequencies to spectroscopic accuracy (3.3 cm$^{-1}$ wavenumbers, corresponding to > 99.9% fidelity). Our approach introduces a new paradigm for studying the quantum chemical dynamics and vibrational spectra of molecules, and when combined with existing algorithms for electronic structure, opens the possibility to describe the complete behavior of complex molecular systems with unprecedented accuracy.
△ Less
Submitted 20 March, 2023; v1 submitted 18 April, 2022;
originally announced April 2022.
-
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Authors:
Vikraman Choudhury,
Jacek Karwowski,
Amr Sabry
Abstract:
The $\mathitΠ$ family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language, using the language of weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equival…
▽ More
The $\mathitΠ$ family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language, using the language of weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of reversible circuits. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, establishing full abstraction and adequacy. We extend the already established Curry-Howard correspondence for $\mathitΠ$ to a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of $\mathitΠ$ is presented by the free symmetric rig groupoid, given by finite sets and permutations. Our proof uses techniques from the theory of group presentations and rewriting systems to solve the word problem for symmetric groups. Using the formalisation of our results, we show how to perform normalisation-by-evaluation, verification, and synthesis of reversible logic gates, motivated by examples from quantum computing.
△ Less
Submitted 11 October, 2021;
originally announced October 2021.
-
Map** quantum chemical dynamics problems onto spin-lattice simulators
Authors:
Debadrita Saha,
Srinivasan S. Iyengar,
Philip Richerme,
Jeremy M. Smith,
Amr Sabry
Abstract:
The accurate computational determination of chemical, materials, biological, and atmospheric properties has critical impact on a wide range of health and environmental problems, but is deeply limited by the computational scaling of quantum-mechanical methods. The complexity of quantum-chemical studies arises from the steep algebraic scaling of electron correlation methods, and the exponential scal…
▽ More
The accurate computational determination of chemical, materials, biological, and atmospheric properties has critical impact on a wide range of health and environmental problems, but is deeply limited by the computational scaling of quantum-mechanical methods. The complexity of quantum-chemical studies arises from the steep algebraic scaling of electron correlation methods, and the exponential scaling in studying nuclear dynamics and molecular flexibility. To date, efforts to apply quantum hardware to such quantum chemistry problems have focused primarily on electron correlation. Here, we provide a framework which allows for the solution of quantum chemical nuclear dynamics by map** these to quantum spin-lattice simulators. Using the example case of a short-strong hydrogen bonded system, we construct the Hamiltonian for the nuclear degrees of freedom on a single Born-Oppenheimer surface and show how it can be transformed to a generalized Ising model Hamiltonian. We then demonstrate a method to determine the local fields and spin-spin couplings needed to identically match the molecular and spin-lattice Hamiltonians. We describe a protocol to determine the on-site and inter-site coupling parameters of this Ising Hamiltonian from the Born-Oppenheimer potential and nuclear kinetic energy operator. Our approach represents a paradigm shift in the methods used to study quantum nuclear dynamics, opening the possibility to solve both electronic structure and nuclear dynamics problems using quantum computing systems.
△ Less
Submitted 8 June, 2021; v1 submitted 12 March, 2021;
originally announced March 2021.
-
Fractional Types: Expressive and Safe Space Management for Ancilla Bits
Authors:
Chao-Hong Chen,
Vikraman Choudhury,
Jacques Carette,
Amr Sabry
Abstract:
In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely de-allocated if its contents are restored to their initial value from allocation time. Generally speaking, the state of the art provides limited partial solutions…
▽ More
In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely de-allocated if its contents are restored to their initial value from allocation time. Generally speaking, the state of the art provides limited partial solutions that address the first constraint by imposing a stack discipline and by leaving the second constraint to programmers' assertions. We propose a novel approach based on the idea of fractional types. As a simple intuitive example, allocation of a new boolean value initialized to $\texttt{false}$ also creates a value $1/{\texttt{false}}$ that can be thought of as a garbage collection (GC) process specialized to reclaim, and only reclaim, storage containing the value $\texttt{false}$. This GC process is a first-class entity that can be manipulated, decomposed into smaller processes and combined with other GC processes. We formalize this idea in the context of a reversible language founded on type isomorphisms, prove its fundamental correctness properties, and illustrate its expressiveness using a wide variety of examples. The development is backed by a fully-formalized Agda implementation.
△ Less
Submitted 17 February, 2020;
originally announced February 2020.
-
Embracing the Laws of Physics: Three Reversible Models of Computation
Authors:
Jacques Carette,
Roshan P. James,
Amr Sabry
Abstract:
Our main models of computation (the Turing Machine and the RAM) make fundamental assumptions about which primitive operations are realizable. The consensus is that these include logical operations like conjunction, disjunction and negation, as well as reading and writing to memory locations. This perspective conforms to a macro-level view of physics and indeed these operations are realizable using…
▽ More
Our main models of computation (the Turing Machine and the RAM) make fundamental assumptions about which primitive operations are realizable. The consensus is that these include logical operations like conjunction, disjunction and negation, as well as reading and writing to memory locations. This perspective conforms to a macro-level view of physics and indeed these operations are realizable using macro-level devices involving thousands of electrons. This point of view is however incompatible with quantum mechanics, or even elementary thermodynamics, as both imply that information is a conserved quantity of physical processes, and hence of primitive computational operations.
Our aim is to re-develop foundational computational models that embraces the principle of conservation of information. We first define what conservation of information means in a computational setting. We emphasize that computations must be reversible transformations on data. One can think of data as modeled using topological spaces and programs as modeled by reversible deformations. We illustrate this idea using three notions of data. The first assumes unstructured finite data, i.e., discrete topological spaces. The corresponding notion of reversible computation is that of permutations. We then consider a structured notion of data based on the Curry-Howard correspondence; here reversible deformations, as a programming language for witnessing type isomorphisms, comes from proof terms for commutative semirings. We then "move up a level" to treat programs as data. The corresponding notion of reversible programs equivalences comes from the "higher dimensional" analog to commutative semirings: symmetric rig groupoids. The coherence laws for these are exactly the program equivalences we seek.
We conclude with some generalizations inspired by homotopy type theory and survey directions for further research.
△ Less
Submitted 10 December, 2018; v1 submitted 8 November, 2018;
originally announced November 2018.
-
From Symmetric Pattern-Matching to Quantum Control (Extended Version)
Authors:
Amr Sabry,
Benoît Valiron,
Juliana Kaizer Vizzotto
Abstract:
One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of…
▽ More
One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however not believed to be meaningful in its most general form.
In this paper, we argue that, under the right circumstances, a reasonable notion of quantum loops and recursion is possible. To this aim, we first propose a classical, typed, reversible language with lists and fixpoints. We then extend this language to the closed quantum domain (without measurements) by allowing linear combinations of terms and restricting fixpoints to structurally recursive fixpoints whose termination proofs match the proofs of convergence of sequences in infinite-dimensional Hilbert spaces. We additionally give an operational semantics for the quantum language in the spirit of algebraic lambda-calculi and illustrate its expressiveness by modeling several common unitary operations.
△ Less
Submitted 3 April, 2018;
originally announced April 2018.
-
Quantum Interval-Valued Probability: Contextuality and the Born Rule
Authors:
Yu-Tsung Tai,
Andrew J. Hanson,
Gerardo Ortiz,
Amr Sabry
Abstract:
We present a mathematical framework based on quantum interval-valued probability measures to study the effect of experimental imperfections and finite precision measurements on defining aspects of quantum mechanics such as contextuality and the Born rule. While foundational results such as the Kochen-Specker and Gleason theorems are valid in the context of infinite precision, they fail to hold in…
▽ More
We present a mathematical framework based on quantum interval-valued probability measures to study the effect of experimental imperfections and finite precision measurements on defining aspects of quantum mechanics such as contextuality and the Born rule. While foundational results such as the Kochen-Specker and Gleason theorems are valid in the context of infinite precision, they fail to hold in general in a world with limited resources. Here we employ an interval-valued framework to establish bounds on the validity of those theorems in realistic experimental environments. In this way, not only can we quantify the idea of finite-precision measurement within our theory, but we can also suggest a possible resolution of the Meyer-Mermin debate on the impact of finite-precision measurement on the Kochen-Specker theorem.
△ Less
Submitted 5 April, 2018; v1 submitted 24 December, 2017;
originally announced December 2017.
-
From Reversible Programs to Univalent Universes and Back
Authors:
Jacques Carette,
Chao-Hong Chen,
Vikraman Choudhury,
Amr Sabry
Abstract:
We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming language to paths in the univalent universe; and combinator optimizations in the programming language to 2-paths in the univalent universe. The result suggests a simpl…
▽ More
We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combinators witnessing type isomorphisms in the programming language to paths in the univalent universe; and combinator optimizations in the programming language to 2-paths in the univalent universe. The result suggests a simple computational interpretation of paths and of univalence in terms of familiar programming constructs whenever the universe in question is computable.
△ Less
Submitted 9 August, 2017;
originally announced August 2017.
-
Reversible Communicating Processes
Authors:
Geoffrey Brown,
Amr Sabry
Abstract:
Reversible distributed programs have the ability to abort unproductive computation paths and backtrack, while unwinding communication that occurred in the aborted paths. While it is natural to assume that reversibility implies full state recovery (as with traditional roll-back recovery protocols), an interesting alternative is to separate backtracking from local state recovery. For example, such…
▽ More
Reversible distributed programs have the ability to abort unproductive computation paths and backtrack, while unwinding communication that occurred in the aborted paths. While it is natural to assume that reversibility implies full state recovery (as with traditional roll-back recovery protocols), an interesting alternative is to separate backtracking from local state recovery. For example, such a model could be used to create complex transactions out of nested compensable transactions where a programmer-supplied compensation defines the work required to "unwind" a transaction.
Reversible distributed computing has received considerable theoretical attention, but little reduction to practice; the few published implementations of languages supporting reversibility depend upon a high degree of central control. The objective of this paper is to demonstrate that a practical reversible distributed language can be efficiently implemented in a fully distributed manner.
We discuss such a language, supporting CSP-style synchronous communication, embedded in Scala. While this language provided the motivation for the work described in this paper, our focus is upon the distributed implementation. In particular, we demonstrate that a "high-level" semantic model can be implemented using a simple point-to-point protocol.
△ Less
Submitted 10 February, 2016;
originally announced February 2016.
-
Discrete Quantum Theories
Authors:
Andrew J. Hanson,
Gerardo Ortiz,
Amr Sabry,
Yu-Tsung Tai
Abstract:
We explore finite-field frameworks for quantum theory and quantum computation. The simplest theory, defined over unrestricted finite fields, is unnaturally strong. A second framework employs only finite fields with no solution to x^2+1=0, and thus permits an elegant complex representation of the extended field by adjoining i=\sqrt{-1}. Quantum theories over these fields recover much of the structu…
▽ More
We explore finite-field frameworks for quantum theory and quantum computation. The simplest theory, defined over unrestricted finite fields, is unnaturally strong. A second framework employs only finite fields with no solution to x^2+1=0, and thus permits an elegant complex representation of the extended field by adjoining i=\sqrt{-1}. Quantum theories over these fields recover much of the structure of conventional quantum theory except for the condition that vanishing inner products arise only from null states; unnaturally strong computational power may still occur. Finally, we are led to consider one more framework, with further restrictions on the finite fields, that recovers a local transitive order and a locally-consistent notion of inner product with a new notion of cardinal probability. In this framework, conventional quantum mechanics and quantum computation emerge locally (though not globally) as the size of the underlying field increases. Interestingly, the framework allows one to choose separate finite fields for system description and for measurement: the size of the first field quantifies the resources needed to describe the system and the size of the second quantifies the resources used by the observer. This resource-based perspective potentially provides insights into quantitative measures for actual computational power, the complexity of quantum system definition and evolution, and the independent question of the cost of the measurement process.
△ Less
Submitted 14 May, 2013;
originally announced May 2013.
-
Geometry of Discrete Quantum Computing
Authors:
Andrew J. Hanson,
Gerardo Ortiz,
Amr Sabry,
Yu-Tsung Tai
Abstract:
Conventional quantum computing entails a geometry based on the description of an n-qubit state using 2^{n} infinite precision complex numbers denoting a vector in a Hilbert space. Such numbers are in general uncomputable using any real-world resources, and, if we have the idea of physical law as some kind of computational algorithm of the universe, we would be compelled to alter our descriptions o…
▽ More
Conventional quantum computing entails a geometry based on the description of an n-qubit state using 2^{n} infinite precision complex numbers denoting a vector in a Hilbert space. Such numbers are in general uncomputable using any real-world resources, and, if we have the idea of physical law as some kind of computational algorithm of the universe, we would be compelled to alter our descriptions of physics to be consistent with computable numbers. Our purpose here is to examine the geometric implications of using finite fields Fp and finite complexified fields Fp^2 (based on primes p congruent to 3 mod{4}) as the basis for computations in a theory of discrete quantum computing, which would therefore become a computable theory. Because the states of a discrete n-qubit system are in principle enumerable, we are able to determine the proportions of entangled and unentangled states. In particular, we extend the Hopf fibration that defines the irreducible state space of conventional continuous n-qubit theories (which is the complex projective space CP{2^{n}-1}) to an analogous discrete geometry in which the Hopf circle for any n is found to be a discrete set of p+1 points. The tally of unit-length n-qubit states is given, and reduced via the generalized Hopf fibration to DCP{2^{n}-1}, the discrete analog of the complex projective space, which has p^{2^{n}-1} (p-1)\prod_{k=1}^{n-1} (p^{2^{k}}+1) irreducible states. Using a measure of entanglement, the purity, we explore the entanglement features of discrete quantum states and find that the n-qubit states based on the complexified field Fp^2 have p^{n} (p-1)^{n} unentangled states (the product of the tally for a single qubit) with purity 1, and they have p^{n+1}(p-1)(p+1)^{n-1} maximally entangled states with purity zero.
△ Less
Submitted 16 May, 2013; v1 submitted 25 June, 2012;
originally announced June 2012.
-
The Power of Discrete Quantum Theories
Authors:
Andrew J. Hanson,
Gerardo Ortiz,
Amr Sabry,
Jeremiah Willcock
Abstract:
We explore the implications of restricting the framework of quantum theory and quantum computation to finite fields. The simplest proposed theory is defined over arbitrary finite fields and loses the notion of unitaries. This makes such theories unnaturally strong, permitting the search of unstructured databases faster than asymptotically possible in conventional quantum computing. The next most g…
▽ More
We explore the implications of restricting the framework of quantum theory and quantum computation to finite fields. The simplest proposed theory is defined over arbitrary finite fields and loses the notion of unitaries. This makes such theories unnaturally strong, permitting the search of unstructured databases faster than asymptotically possible in conventional quantum computing. The next most general approach chooses finite fields with no solution to x^2+1=0, and thus permits an elegant complex-like representation of the extended field by adjoining i=sqrt(-1). Quantum theories over these fields retain the notion of unitaries and --- for particular problem sizes --- allow the same algorithms as conventional quantum theory. These theories, however, still support unnaturally strong computations for certain problem sizes, but the possibility of such phenomena decreases as the size of the field increases.
△ Less
Submitted 8 April, 2011;
originally announced April 2011.
-
Solving UNIQUE-SAT in a Modal Quantum Theory
Authors:
Jeremiah Willcock,
Amr Sabry
Abstract:
In recent work, Benjamin Schumacher and Michael D. Westmoreland investigate a version of quantum mechanics which they call modal quantum theory. This theory is obtained by instantiating the mathematical framework of Hilbert spaces with a finite field instead of the field of complex numbers. This instantiation collapses much the structure of actual quantum mechanics but retains several of its disti…
▽ More
In recent work, Benjamin Schumacher and Michael D. Westmoreland investigate a version of quantum mechanics which they call modal quantum theory. This theory is obtained by instantiating the mathematical framework of Hilbert spaces with a finite field instead of the field of complex numbers. This instantiation collapses much the structure of actual quantum mechanics but retains several of its distinguishing characteristics including the notions of superposition, interference, and entanglement. Furthermore, modal quantum theory excludes local hidden variable models, has a no-cloning theorem, and can express natural counterparts of quantum information protocols such as superdense coding and teleportation.
We show that the problem of UNIQUE-SAT --- which decides whether a given Boolean formula is unsatisfiable or has exactly one satisfying assignment --- is deterministically solvable in any modal quantum theory in constant time. The solution exploits the lack of orthogonality in modal quantum theories and is not directly applicable to actual quantum theory.
△ Less
Submitted 17 February, 2011;
originally announced February 2011.
-
Quantum Computing over Finite Fields
Authors:
Roshan P. James,
Gerardo Ortiz,
Amr Sabry
Abstract:
In recent work, Benjamin Schumacher and Michael~D. Westmoreland investigate a version of quantum mechanics which they call "modal quantum theory" but which we prefer to call "discrete quantum theory". This theory is obtained by instantiating the mathematical framework of Hilbert spaces with a finite field instead of the field of complex numbers. This instantiation collapses much the structure of a…
▽ More
In recent work, Benjamin Schumacher and Michael~D. Westmoreland investigate a version of quantum mechanics which they call "modal quantum theory" but which we prefer to call "discrete quantum theory". This theory is obtained by instantiating the mathematical framework of Hilbert spaces with a finite field instead of the field of complex numbers. This instantiation collapses much the structure of actual quantum mechanics but retains several of its distinguishing characteristics including the notions of superposition, interference, and entanglement. Furthermore, discrete quantum theory excludes local hidden variable models, has a no-cloning theorem, and can express natural counterparts of quantum information protocols such as superdense coding and teleportation. Our first result is to distill a model of discrete quantum computing from this quantum theory. The model is expressed using a monadic metalanguage built on top of a universal reversible language for finite computations, and hence is directly implementable in a language like Haskell. In addition to superpositions and invertible linear maps, the model includes conventional programming constructs including pairs, sums, higher-order functions, and recursion. Our second result is to relate this programming model to relational programming, e.g., a pure version of Prolog over finite relations. Surprisingly discrete quantum computing is identical to conventional logic programming except for a small twist that is responsible for all the ``quantum-ness.'' The twist occurs when merging sets of answers computed by several alternatives: the answers are combined using an "exclusive" version of logical disjunction. In other words, the two branches of a choice junction exhibit an "interference" effect: an answer is produced from the junction if it occurs in one or the other branch but not both.
△ Less
Submitted 19 January, 2011;
originally announced January 2011.
-
Lazy Evaluation and Delimited Control
Authors:
Ronald Garcia,
Andrew Lumsdaine,
Amr Sabry
Abstract:
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes "under lambdas." We prove that machine…
▽ More
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a series of reasoning steps, we systematically unpack the standard-order reduction relation of the calculus and discover a novel abstract machine definition which, like the calculus, goes "under lambdas." We prove that machine evaluation is equivalent to standard-order evaluation. Unlike traditional abstract machines, delimited control plays a significant role in the machine's behavior. In particular, the machine replaces the manipulation of a heap using store-based effects with disciplined management of the evaluation stack using control-based effects. In short, state is replaced with control. To further articulate this observation, we present a simulation of call-by-need in a call-by-value language using delimited control operations.
△ Less
Submitted 11 July, 2010; v1 submitted 26 March, 2010;
originally announced March 2010.
-
The Arrow Calculus as a Quantum Programming Language
Authors:
Juliana Kaizer Vizzotto,
Andre Rauber Du Bois,
Amr Sabry
Abstract:
We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the presence of computational effects. In addition, the five laws of the arrow calculus provide a convenient framework for equational reasoning about quantum computat…
▽ More
We express quantum computations (with measurements) using the arrow calculus extended with monadic constructions. This framework expresses quantum programming using well-understood and familiar classical patterns for programming in the presence of computational effects. In addition, the five laws of the arrow calculus provide a convenient framework for equational reasoning about quantum computations that include measurements.
△ Less
Submitted 10 April, 2009; v1 submitted 9 March, 2009;
originally announced March 2009.
-
An Algebra of Pure Quantum Programming
Authors:
Thorsten Altenkirch,
Jonathan Grattage,
Juliana K. Vizzotto,
Amr Sabry
Abstract:
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously-developed denotational semantics of QML. The completeness proof also gives rise to a normalisation algorithm following the normalisation by evaluation approach. The current work focuses on the pure fragment of QML o…
▽ More
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously-developed denotational semantics of QML. The completeness proof also gives rise to a normalisation algorithm following the normalisation by evaluation approach. The current work focuses on the pure fragment of QML omitting measurements.
△ Less
Submitted 1 June, 2005;
originally announced June 2005.
-
Structuring quantum effects: superoperators as arrows
Authors:
J. K. Vizzotto,
T. Altenkirch,
A. Sabry
Abstract:
We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and measurement. The effectful part can be modeled using a generalization of monads called arrows. We express the resulting executable model of quantum computing in the programming language Haskell using it…
▽ More
We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and measurement. The effectful part can be modeled using a generalization of monads called arrows. We express the resulting executable model of quantum computing in the programming language Haskell using its special syntax for arrow computations. The embedding in Haskell is however not perfect: a faithful model of quantum computing requires type capabilities which are not directly expressible in Haskell.
△ Less
Submitted 25 January, 2005;
originally announced January 2005.
