-
Join Inverse Rig Categories for Reversible Functional Programming, and Beyond
Authors:
Robin Kaarsgaard,
Mathys Rennela
Abstract:
Reversible computing is a computational paradigm in which computations are deterministic in both the forward and backward direction, so that programs have well-defined forward and backward semantics. We investigate the formal semantics of the reversible functional programming language Rfun. For this purpose, we introduce join inverse rig categories, the natural marriage of join inverse categories…
▽ More
Reversible computing is a computational paradigm in which computations are deterministic in both the forward and backward direction, so that programs have well-defined forward and backward semantics. We investigate the formal semantics of the reversible functional programming language Rfun. For this purpose, we introduce join inverse rig categories, the natural marriage of join inverse categories and rig categories, which we show can be used to model the language Rfun, under reasonable assumptions. These categories turn out to be a particularly natural fit for reversible computing as a whole, as they encompass models for other reversible programming languages, notably Theseus and reversible flowcharts. This suggests that join inverse rig categories really are the categorical models of reversible computing.
△ Less
Submitted 28 December, 2021; v1 submitted 20 May, 2021;
originally announced May 2021.
-
Hybrid divide-and-conquer approach for tree search algorithms
Authors:
Mathys Rennela,
Sebastiaan Brand,
Alfons Laarman,
Vedran Dunjko
Abstract:
One of the challenges of quantum computers in the near- and mid- term is the limited number of qubits we can use for computations. Finding methods that achieve useful quantum improvements under size limitations is thus a key question in the field. In this vein, it was recently shown that a hybrid classical-quantum method can help provide polynomial speed-ups to classical divide-and-conquer algorit…
▽ More
One of the challenges of quantum computers in the near- and mid- term is the limited number of qubits we can use for computations. Finding methods that achieve useful quantum improvements under size limitations is thus a key question in the field. In this vein, it was recently shown that a hybrid classical-quantum method can help provide polynomial speed-ups to classical divide-and-conquer algorithms, even when only given access to a quantum computer much smaller than the problem itself. In this work, we study the hybrid divide-and-conquer method in the context of tree search algorithms, and extend it by including quantum backtracking, which allows better results than previous Grover-based methods. Further, we provide general criteria for polynomial speed-ups in the tree search context, and provide a number of examples where polynomial speed ups, using arbitrarily smaller quantum computers, can be obtained. We provide conditions for speedups for the well known algorithm of DPLL, and we prove threshold-free speed-ups for the PPSZ algorithm (the core of the fastest exact Boolean satisfiability solver) for well-behaved classes of formulas. We also provide a simple example where speed-ups can be obtained in an algorithm-independent fashion, under certain well-studied complexity-theoretical assumptions. Finally, we briefly discuss the fundamental limitations of hybrid methods in providing speed-ups for larger problems.
△ Less
Submitted 20 March, 2023; v1 submitted 14 July, 2020;
originally announced July 2020.
-
Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
Authors:
Romain Péchoux,
Simon Perdrix,
Mathys Rennela,
Vladimir Zamdzhiev
Abstract:
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in…
▽ More
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics.
△ Less
Submitted 21 October, 2019;
originally announced October 2019.
-
Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
Authors:
Mathys Rennela,
Sam Staton
Abstract:
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for t…
▽ More
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.
△ Less
Submitted 9 March, 2020; v1 submitted 14 November, 2017;
originally announced November 2017.
-
Infinite-Dimensionality in Quantum Foundations: W*-algebras as Presheaves over Matrix Algebras
Authors:
Mathys Rennela,
Sam Staton,
Robert Furber
Abstract:
In this paper, W*-algebras are presented as canonical colimits of diagrams of matrix algebras and completely positive maps. In other words, matrix algebras are dense in W*-algebras.
In this paper, W*-algebras are presented as canonical colimits of diagrams of matrix algebras and completely positive maps. In other words, matrix algebras are dense in W*-algebras.
△ Less
Submitted 3 January, 2017;
originally announced January 2017.
-
Convexity and Order in Probabilistic Call-by-Name FPC
Authors:
Mathys Rennela
Abstract:
Kegelspitzen are mathematical structures coined by Keimel and Plotkin, in order to encompass the structure of a convex set and the structure of a dcpo. In this paper, we ask ourselves what are Kegelspitzen the model of. We adopt a categorical viewpoint and show that Kegelspitzen model stochastic matrices onto a category of domains. Consequently, Kegelspitzen form a denotational model of pPCF, an a…
▽ More
Kegelspitzen are mathematical structures coined by Keimel and Plotkin, in order to encompass the structure of a convex set and the structure of a dcpo. In this paper, we ask ourselves what are Kegelspitzen the model of. We adopt a categorical viewpoint and show that Kegelspitzen model stochastic matrices onto a category of domains. Consequently, Kegelspitzen form a denotational model of pPCF, an abstract functional programming language for probabilistic computing. We conclude the present work with a discussion of the interpretation of (probabilistic) recursive types, which are types for entities which might contain other entities of the same type, such as lists and trees.
△ Less
Submitted 11 November, 2020; v1 submitted 14 July, 2016;
originally announced July 2016.
-
Operator Algebras in Quantum Computation
Authors:
Mathys Rennela
Abstract:
In this master thesis, I discuss how the theory of operator algebras, also called operator theory, can be applied in quantum computer science.
In this master thesis, I discuss how the theory of operator algebras, also called operator theory, can be applied in quantum computer science.
△ Less
Submitted 22 October, 2015;
originally announced October 2015.
-
Privacy in Quantum Communication Complexity
Authors:
Iordanis Kerenidis,
Mathieu Laurière,
François Le Gall,
Mathys Rennela
Abstract:
In two-party quantum communication complexity, Alice and Bob receive some classical inputs and wish to compute some function that depends on both these inputs, while minimizing the communication. This model has found numerous applications in many areas of computer science. One question that has received a lot of attention recently is whether it is possible to perform such protocols in a private wa…
▽ More
In two-party quantum communication complexity, Alice and Bob receive some classical inputs and wish to compute some function that depends on both these inputs, while minimizing the communication. This model has found numerous applications in many areas of computer science. One question that has received a lot of attention recently is whether it is possible to perform such protocols in a private way. We show that defining privacy for quantum protocols is not so straightforward and it depends on whether we assume that the registers where Alice and Bob receive their classical inputs are in fact classical registers (and hence unentangled with the rest of the protocol) or quantum registers (and hence can be entangled with the rest of the protocol or the environment). We provide new quantum protocols for the Inner Product function and for Private Information Retrieval, and show that the privacy assuming classical input registers can be exponentially smaller than the privacy assuming quantum input registers. We also argue that the right notion of privacy of a communication protocol is the one assuming classical input registers, since otherwise the players can deviate considerably from the protocol.
△ Less
Submitted 30 September, 2014;
originally announced September 2014.
