Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Rewriting Theory for Quantum Lambda-Calculus

Claudia Faggian, Gaetan Lopez, Benoît Valiron

TL;DR

This work develops a comprehensive rewriting theory for an untyped quantum lambda-calculus with measurements, integrating probabilistic and infinitary behavior through a surface-focused evaluation strategy. It proves confluence and finitary standardization for a general reduction that respects quantum memory constraints, and establishes asymptotic normalization via a strict surface-lifting approach that guarantees convergence to a unique limit. By coupling a rich operational semantics with multidistribution-based probabilistic rewriting, it provides a solid foundation for reasoning about program transformations, optimizations, and equivalence in quantum functional programming. The results extend the classical standardization paradigm to the quantum setting, enabling robust analysis of termination probabilities and long-run behavior in quantum computations. This framework is expected to support compiler optimizations and formal verification in quantum programming languages that blend classical control with quantum memory manipulation.

Abstract

Quantum lambda calculus has been studied mainly as an idealized programming language -- the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results.

A Rewriting Theory for Quantum Lambda-Calculus

TL;DR

This work develops a comprehensive rewriting theory for an untyped quantum lambda-calculus with measurements, integrating probabilistic and infinitary behavior through a surface-focused evaluation strategy. It proves confluence and finitary standardization for a general reduction that respects quantum memory constraints, and establishes asymptotic normalization via a strict surface-lifting approach that guarantees convergence to a unique limit. By coupling a rich operational semantics with multidistribution-based probabilistic rewriting, it provides a solid foundation for reasoning about program transformations, optimizations, and equivalence in quantum functional programming. The results extend the classical standardization paradigm to the quantum setting, enabling robust analysis of termination probabilities and long-run behavior in quantum computations. This framework is expected to support compiler optimizations and formal verification in quantum programming languages that blend classical control with quantum memory manipulation.

Abstract

Quantum lambda calculus has been studied mainly as an idealized programming language -- the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus is standardization and normalization results.

Paper Structure

This paper contains 44 sections, 10 theorems, 13 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Quantum $\lambda$-Calculus and Linear Logics.
  3. Probabilistic and Infinitary Behavior.
  4. Operational Semantics of Quantum Programs.
  5. A Rewriting Theory for the Quantum $\lambda$-Calculus.
  6. Contributions.
  7. Setting the Scene: the Rewriting Ingredients
  8. Untyped Quantum $\lambda$-Calculus.
  9. Call-by-Value... or rather, Call-by-Push-Value.
  10. A Taste of Standardization and Normalization: Pure $\lambda$-Calculi.
  11. Untyped Quantum $\lambda$-Calculus
  12. Raw Terms.
  13. Terms Validity.
  14. Quantum Operations.
  15. Programs.
  16. ...and 29 more sections

Key Result

Proposition 8

If $M$ is a valid term, and ${\pmb{[}}\mathtt{Q} ; M{ \pmb{]}} \rightarrow \{\!\!\{\, p_i {\pmb{[}} \mathtt{Q}_i ; M_i{ \pmb{]}} \,\}\!\!\}$, then $M_i$ is a valid term.

Figures (4)

  • Figure 1: Root rules $(\mapsto)$
  • Figure 3: Lifting of $\rightarrow$
  • Figure 4: Strict lifting of $\mathrel{\mathop{\rightarrow}\limits_{ \hbox{\ex@ ${\mathsf s}$}}}$
  • Figure 5: Limit of (possibly infinite) reduction sequences

Theorems & Definitions (26)

  • Example 1: duplication, or not
  • Remark 2
  • Definition 3: Valid Terms, and Linearity
  • Remark 4
  • Definition 5: Program
  • Example 6
  • Remark 7: Reindexing
  • Proposition 8
  • Example 9: Flipping the quantum coin
  • Example 10: Entangled pair
  • ...and 16 more