A Quantum-Control Lambda-Calculus with Multiple Measurement Bases

• URL: http://arxiv.org/abs/2506.16244v1
• Date: Thu, 19 Jun 2025 11:59:39 GMT
• Title: A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
• Authors: Alejandro Díaz-Caro, Nicolas A. Monzon,
• Abstract summary: We introduce Lambda-SX, a typed quantum-calculus that supports multiple measurement bases.<n>By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements.
• Score: 49.1574468325115
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its syntax, typing rules, subtyping, and operational semantics, and establish its key meta-theoretical properties. This proof-of-concept shows that support for multiple bases can be coherently integrated into the type discipline of quantum programming languages.

Related papers

• 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)
• 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)
• Determining the ability for universal quantum computing: Testing controllability via dimensional expressivity [39.58317527488534]
  Controllability tests can be used in the design of quantum devices to reduce the number of external controls. We devise a hybrid quantum-classical algorithm based on a parametrized quantum circuit.
  arXiv  Detail & Related papers  (2023-08-01T15:33:41Z)
• Quantum signal processing with continuous variables [0.0]
  Quantum singular value transformation (QSVT) enables the application of functions to singular values of near arbitrary linear operators embedded in unitary transforms. We show that one can recover a QSP-type ansatz, and show its ability to approximate near arbitrary transformations. We discuss various experimental uses of this construction, as well as prospects for expanded relevance of QSP-like ans"atze to other Lie groups.
  arXiv  Detail & Related papers  (2023-04-27T17:50:16Z)
• Quantum Bayesian Inference in Quasiprobability Representations [0.0]
  Bayes' rule plays a crucial piece of logical inference in information and physical sciences alike. quantum versions of Bayes' rule have been expressed in the language of Hilbert spaces.
  arXiv  Detail & Related papers  (2023-01-05T08:16:50Z)
• Approximate traces on groups and the quantum complexity class $\operatorname{MIP}^{co,s}$ [0.0]
  We introduce the notion of a qc-modulus, which encodes approximations to quantum commuting correlations. We show that the existence of a computable qc-modulus gives a negative answer to a natural variant of the aforementioned question.
  arXiv  Detail & Related papers  (2022-09-16T15:45:49Z)
• The Many-Worlds Calculus [0.0]
  We propose a colored PROP to model computation in this framework.<n>The model can support regular tests, probabilistic and non-deterministic branching, as well as quantum branching.<n>We prove the language to be universal, and the equational theory to be complete with respect to this semantics.
  arXiv  Detail & Related papers  (2022-06-21T10:10:26Z)
• 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)
• The Logic of Quantum Programs [77.34726150561087]
  We present a logical calculus for reasoning about information flow in quantum programs. In particular we introduce a dynamic logic that is capable of dealing with quantum measurements, unitary evolutions and entanglements in compound quantum systems.
  arXiv  Detail & Related papers  (2021-09-14T16:08:37Z)
• Efficient criteria of quantumness for a large system of qubits [58.720142291102135]
  We discuss the dimensionless combinations of basic parameters of large, partially quantum coherent systems. Based on analytical and numerical calculations, we suggest one such number for a system of qubits undergoing adiabatic evolution.
  arXiv  Detail & Related papers  (2021-08-30T23:50:05Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)
• PBS-Calculus: A Graphical Language for Coherent Control of Quantum Computations [77.34726150561087]
  We introduce the PBS-calculus to represent and reason on quantum computations involving coherent control of quantum operations. We equip the language with an equational theory, which is proved to be sound and complete. We consider applications like the implementation of controlled permutations and the unrolling of loops.
  arXiv  Detail & Related papers  (2020-02-21T16:15:58Z)

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.