Linear Dependent Type Theory for Quantum Programming Languages

• URL: http://arxiv.org/abs/2004.13472v6
• Date: Tue, 6 Sep 2022 14:00:55 GMT
• Title: Linear Dependent Type Theory for Quantum Programming Languages
• Authors: Peng Fu, Kohei Kishida, Peter Selinger
• Abstract summary: Modern quantum programming languages integrate quantum resources and classical control. They must be linearly typed to reflect the no-cloning property of quantum resources. High-level and practical languages should also support quantum circuits as first-class citizens.
• Score: 1.7166794984161973
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.

Related papers

• Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [63.733312560668274]
  Given a quantum circuit containing d tunable RZ gates and G-d Clifford gates, can a learner perform purely classical inference to efficiently predict its linear properties? We prove that the sample complexity scaling linearly in d is necessary and sufficient to achieve a small prediction error, while the corresponding computational complexity may scale exponentially in d. We devise a kernel-based learning model capable of trading off prediction error and computational complexity, transitioning from exponential to scaling in many practical settings.
  arXiv  Detail & Related papers  (2024-08-22T08:21:28Z)
• Hybrid Quantum-Classical Machine Learning with String Diagrams [49.1574468325115]
  This paper develops a formal framework for describing hybrid algorithms in terms of string diagrams. A notable feature of our string diagrams is the use of functor boxes, which correspond to a quantum-classical interfaces.
  arXiv  Detail & Related papers  (2024-07-04T06:37:16Z)
• Categories of quantum cpos [0.0]
  We find a noncommutative generalization of $omega$-complete partial orders (cpos) called quantum cpos. quantum cpos may form the backbone of a future quantum domain theory.
  arXiv  Detail & Related papers  (2024-06-03T22:13:32Z)
• Quantum and Reality [0.0]
  We describe a natural emergence of Hermiticity which is rooted in principles of equivariant homotopy theory. This construction of Hermitian forms requires of the ambient linear type theory nothing further than a negative unit term of tensor unit type. We show how this allows for encoding (and verifying) the unitarity of quantum gates and of quantum channels in quantum languages embedded into LHoTT.
  arXiv  Detail & Related papers  (2023-11-18T11:00:12Z)
• Circuit Width Estimation via Effect Typing and Linear Dependency (Long Version) [1.3597551064547502]
  We present Proto-Quipper-R, a circuit description language endowed with a linear dependent type-and-effect system. We show that our approach is expressive enough to verify realistic quantum algorithms.
  arXiv  Detail & Related papers  (2023-10-29T18:10:31Z)
• The Quantum Monadology [0.0]
  Modern theory of functional programming languages uses monads for encoding computational side-effects and side-contexts. We analyze the (co)monads on categories of parameterized module spectra induced by Grothendieck's "motivic yoga of operations" We indicate a domain-specific quantum programming language (QS) expressing these monadic quantum effects in transparent do-notation.
  arXiv  Detail & Related papers  (2023-10-24T11:19:24Z)
• A Framework for Demonstrating Practical Quantum Advantage: Racing Quantum against Classical Generative Models [62.997667081978825]
  We build over a proposed framework for evaluating the generalization performance of generative models. We establish the first comparative race towards practical quantum advantage (PQA) between classical and quantum generative models. Our results suggest that QCBMs are more efficient in the data-limited regime than the other state-of-the-art classical generative models.
  arXiv  Detail & Related papers  (2023-03-27T22:48:28Z)
• The Quantum Path Kernel: a Generalized Quantum Neural Tangent Kernel for Deep Quantum Machine Learning [52.77024349608834]
  Building a quantum analog of classical deep neural networks represents a fundamental challenge in quantum computing. Key issue is how to address the inherent non-linearity of classical deep learning. We introduce the Quantum Path Kernel, a formulation of quantum machine learning capable of replicating those aspects of deep machine learning.
  arXiv  Detail & Related papers  (2022-12-22T16:06:24Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  This paper introduces a dynamic logic formalism for reasoning about information flow in composite quantum systems. We present a finitary syntax, a relational semantics and a sound proof system for this logic. As applications, we use our system to give formal correctness for the Teleportation protocol and for a standard Quantum Secret Sharing protocol.
  arXiv  Detail & Related papers  (2021-10-04T12:20:23Z)
• A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper [1.5274311118568713]
  We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits.
  arXiv  Detail & Related papers  (2020-05-17T23:31:23Z)
• From a quantum theory to a classical one [117.44028458220427]
  We present and discuss a formal approach for describing the quantum to classical crossover. The method was originally introduced by L. Yaffe in 1982 for tackling large-$N$ quantum field theories.
  arXiv  Detail & Related papers  (2020-04-01T09:16:38Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.