Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime

Kengo Hirata, Chris Heunen

TL;DR

The Rust type system is extended to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz), which parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime.

Abstract

Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.

Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime

TL;DR

The Rust type system is extended to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz), which parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime.

Abstract

Uncomputation is a feature in quantum programming that allows the programmer to discard a value without losing quantum information, and that allows the compiler to reuse resources. Whereas quantum information has to be treated linearly by the type system, automatic uncomputation enables the programmer to treat it affinely to some extent. Automatic uncomputation requires a substructural type system between linear and affine, a subtlety that has only been captured by existing languages in an ad hoc way. We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts (pronounced quartz). Specifically, we parameterise types by lifetimes, permitting them to be affine during their lifetime, while being restricted to linear use outside their lifetime. We also provide two operational semantics: one based on classical simulation, and one that does not depend on any specific uncomputation strategy.

Paper Structure

This paper contains 74 sections, 17 theorems, 37 equations, 27 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Quantum Computation
  4. Rust: Lifetime, Borrowing, and Ownership
  5. Ownership: Move versus Copy
  6. Reversible Pebble Games
  7. Qurts
  8. Qurts by Example
  9. Grover's algorithm
  10. Implementing Boolean circuits
  11. Lifetime annotations
  12. Lifted functions
  13. Uncomputability via types
  14. Two implementations of CX
  15. Dropping variables
  16. ...and 59 more sections

Key Result

lemma 1

The map $\mathrm{loc}_i[x_i \mapsto [], y\mapsto L]$ in the simulation qif does not depend on $i$.

Figures (27)

  • Figure 1: An example strategy with a minimum number of pebbles
  • Figure 2: Grover's algorithm for 3 qubits in Qurts.
  • Figure 3: Qurts syntax
  • Figure 4: Qurts types and judgement contexts
  • Figure 5: Selected typing rule for statements
  • ...and 22 more figures

Theorems & Definitions (46)

  • definition 1
  • lemma 1
  • lemma 2
  • definition 2
  • definition 3
  • theorem 1
  • definition 4: Circuit Graph
  • definition 5
  • theorem 2
  • theorem 3
  • ...and 36 more