pith. sign in

arxiv: 2411.10835 · v1 · submitted 2024-11-16 · 💻 cs.PL · quant-ph

Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime

Kengo Hirata , Chris Heunen This is my paper

Pith reviewed 2026-05-23 17:13 UTC · model grok-4.3

classification 💻 cs.PL quant-ph
keywords quantum programmingtype systemsuncomputationaffine typeslifetimessubstructural typesRust
0
0 comments X

The pith

Qurts extends the Rust type system with lifetime-parameterized types to enable uniform automatic uncomputation for quantum data.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a uniform substructural type system for quantum programming that sits between linear and affine regimes. Quantum information must normally be used linearly, yet automatic uncomputation lets programmers treat it affinely by safely discarding values and reusing resources. The approach parameterizes types by lifetimes so that quantum data may be used affinely while the lifetime is active and must be used linearly outside it. This replaces the ad-hoc mechanisms of prior quantum languages with a single framework derived from Rust. Two operational semantics are supplied: one for classical simulation and one independent of any particular uncomputation strategy.

Core claim

We extend the Rust type system to the quantum setting to give a uniform framework for automatic uncomputation called Qurts. 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.

What carries the argument

Lifetime-parameterized types that permit affine use of quantum data only during the active lifetime and enforce linear use outside it.

If this is right

  • Programmers gain the ability to treat quantum values affinely during a lifetime without manual uncomputation.
  • Compilers obtain a systematic basis for resource reuse rather than language-specific ad-hoc rules.
  • Quantum programs become expressible in a typed language that already supports affine and linear modes via lifetimes.
  • Verification of uncomputation correctness can proceed from the type system independently of the chosen uncomputation algorithm.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lifetime mechanism could be lifted to other quantum languages that already embed Rust-like type systems.
  • Resource accounting in larger quantum circuits might become automatic once lifetimes are inferred from control flow.
  • Integration with existing Rust tooling could let quantum developers reuse borrow-checker diagnostics for uncomputation safety.

Load-bearing premise

Lifetime parameterization of types can capture the required distinction between linear and affine use for quantum information in a uniform way.

What would settle it

A concrete quantum program typed in Qurts where a value is discarded inside its lifetime yet the resulting circuit either loses information or violates linearity outside the lifetime.

Figures

Figures reproduced from arXiv: 2411.10835 by Chris Heunen, Kengo Hirata.

Figure 1
Figure 1. Figure 1: An example strategy with a minimum number of pebbles [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Grover’s algorithm for 3 qubits in Qurts. [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Qurts syntax Types: Lifetime 𝔞 ::= 𝛼 | ⊥ | ⊤ Type 𝑇 ::= bool | qbit | ( ) | 𝑇1 × 𝑇2 | & 𝔞 𝑇 | # 𝔞 𝑇 Contexts: Type Context Γ ::= 𝑥0 : a0𝑇0, . . . , 𝑥𝑛−1 : an−1𝑇𝑛−1 Aliveness a ::= active | †𝛼 [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Qurts types and judgement contexts et al. 2020], a formalised core language of Rust. A program is defined as a sequence of function definitions. A function definition consists of a function name, a signature, and a body block. A signature includes a lifetime preorder, a list of arguments, and a return type. Here, a lifetime preorder is a set of lifetime variables and a preorder on them that presents the co… view at source ↗
Figure 5
Figure 5. Figure 5: Selected typing rule for statements Drop: A ⊢ 𝑇 : Drop drop bool A ⊢ bool: Drop drop borrow A ⊢ & 𝔞𝑇 : Drop drop own 𝔞 ∈ A A ⊢ # 𝔞𝑇 : Drop drop unit A ⊢ ( ) : Drop drop tuple 𝑇0 : Drop 𝑇1 : Drop 𝑇0 × 𝑇1 : Drop [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Drop trait return type of a measurement is # ⊤bool: a classical boolean that can always be dropped. General unitary gates have a linear return type # ⊥qbit𝑛 , because the output is not uncomputable. Lifted isometries have return type # 𝔞qbit𝑚 and remain affine if the input is. The most complicated and critical typing rule for Qurts-core is the rule typ qif governing qif statements. This rule only applies w… view at source ↗
Figure 7
Figure 7. Figure 7: Purely Quantum: types without classical data and programs without measurements [PITH_FULL_IMAGE:figures/full_fig_p016_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Typing rule for blocks, function, and whole program [PITH_FULL_IMAGE:figures/full_fig_p016_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Selected simulation semantics rules. Let Loc𝑞 and Loc𝑐 be the sets of locations for quantum and classical memories. An environment is a triple (loc, |𝜑⟩, 𝑠) of a map loc: Var → List(Loc𝑐 + Loc𝑞) from variables to locations, |𝜑⟩ ∈ H𝐿𝑞 F Ë 𝑙 ∈𝐿𝑞 C 2 and 𝑠 ∈ {0, 1} 𝐿𝑐 are the states of quantum and classical memories, and 𝐿𝑞 ⊂ Loc𝑞 and 𝐿𝑐 ⊂ Loc𝑐 are the image of loc. An environment (loc, |𝜑⟩, 𝑠) is compatible … view at source ↗
Figure 10
Figure 10. Figure 10: Toy example: evaluation steps of the simulation semantics. [PITH_FULL_IMAGE:figures/full_fig_p018_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Uncomputation semantics 𝑣 has a pebble 𝑞{⊤}. When we have one fragmented pebble 𝑝{(𝑣, 𝔞)} on a vertex in state |1⟩ and another fragmented pebble 𝑝{(¬𝑣, 𝔞)} on a vertex in state |0⟩, then the whole quantum state is 𝛾0 |00⟩ + 𝛾1 |11⟩ ∈ H𝑞,𝑝 (𝛾𝑖 ∈ C). A pebble can have multiple guards representing qubit states in nested quantum if statements. Just like merge vertices, pebbles also have lifetimes: a pebble 𝑝{… view at source ↗
Figure 12
Figure 12. Figure 12: Silq: assignments and uncomputation as a classical Boolean function, and then construct another circuit graph with the uncomputation. In Reqomp, it is mentioned that pebble game is not suitable for the uncomputation problem, because the graph constructed is not expressive enough to represent non-qfree gates or repeatedly used values. The pebble game for Qurts overcomes these limitations: Our pebble game i… view at source ↗
Figure 13
Figure 13. Figure 13: Subtyping rule Copy. The rules for the Copy trait, the class of types which can be implicitly copied, are defined in [PITH_FULL_IMAGE:figures/full_fig_p030_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Copy trait Drop. The rule for the Drop trait, the class of affine types which can be dropped, is defined in [PITH_FULL_IMAGE:figures/full_fig_p030_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Typing rule for expressions let z' = qif q { qif r1 { U( z ) } else { z } } else { qif r2 { U( z ) } else { z } }; In terms of the lifetime of quantum information, it seems that if we allow to cast # 𝛼& 𝛽 into & 𝛾 with some 𝛾 satisfying 𝛾 ≤ 𝛼, 𝛽, then it would represent the correct lifetime of the information held by 𝑟, making the code above valid. However, the downside is that it further complicates the … view at source ↗
Figure 16
Figure 16. Figure 16: Typing rule for statements Typing Block, Function, Program: typing block 𝑆 : (Γ, A) Π,𝑓 −−→ (𝑥 : 𝑇 , A) (Γ, A) ⊢Π,𝑓 { 𝑆; 𝑥 } : 𝑇 typing fn 𝐹 = fn 𝑓 Σ 𝐵 Σ = ⟨𝛼0, . . . , 𝛼𝑚−1 | 𝛼𝑎0 ≤ 𝛼𝑏0 , . . . , 𝛼𝑎𝑙−1 ≤ 𝛼𝑏𝑙−1 ⟩ Γ → 𝑇 A: the smallest preorder on {𝛼𝑖 } including {𝛼𝑎𝑗 ≤ 𝛼𝑏𝑗 } (Γ, A) ⊢Π,𝑓 𝐵 : 𝑇 Π ⊢ 𝐹 : Function typing program Π = 𝐹0 . . . 𝐹𝑛−1 ∀𝑖 ∈ {0, . . . , 𝑛 − 1}, 𝐹0 . . . 𝐹𝑖−1 ⊢ 𝐹𝑖 : Function Π: Program… view at source ↗
Figure 17
Figure 17. Figure 17: Typing rule for blocks, function, and whole program [PITH_FULL_IMAGE:figures/full_fig_p033_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: Simulation semantics for let y = e The first row of each rule shows the assumption, and the second row shows the environment after the evaluation of the statement let 𝑦 = 𝑒 under the environment (loc, |𝜑⟩, 𝑠 ). To this end, we introduce a dependency graph to keep track of this dependency relation, and we extend the simulation semantics with the dependency graph. Definition C.3. A dependency graph is a tri… view at source ↗
Figure 19
Figure 19. Figure 19: Simulation semantics for statements The first row of each rule shows the assumption, and the second row shows the environment after the evaluation of the statement 𝑆 under the environment (loc, |𝜑⟩, 𝑠 ). • 𝐺 is a directed graph whose vertices are locations, • 𝐷 is a subset of the set of locations, and • 𝐹 is a function which maps 𝑙 ∈ 𝐷 to a function 𝐹 (𝑙) : {0, 1} source𝐺 (𝑙) → {0, 1}. Definition C.4. A t… view at source ↗
Figure 20
Figure 20. Figure 20: Selected rules of simulation semantics with dependency graph [PITH_FULL_IMAGE:figures/full_fig_p037_20.png] view at source ↗
Figure 21
Figure 21. Figure 21: Rules for uncomputer ⇛ which playes a pebble game to the linear vertex. This rule is the only one which is not bidirectional, making the pebble game irreversible. Rules for Executable Threads [PITH_FULL_IMAGE:figures/full_fig_p044_21.png] view at source ↗
Figure 22
Figure 22. Figure 22: Rules for executable threads (Θ𝑡 , A, (|𝜑⟩, 𝑠),𝐺) → (Θ ′ 𝑡 , A, (|𝜑 ′ ⟩, 𝑠′ ),𝐺) status(𝑡) = Check(𝑆 ) 𝑆 = endlft𝛼, 𝑥 as𝑇 Θ𝑡 → Θ𝑡 [status(𝑡) = Ready] status(𝑡) = Check(let 𝑦 = meas(𝑥 ) ) |𝜓 ⟩ = (id ⊗ ⟨0|)|𝜑⟩ where the target is the main label whose location is loc𝑡 (𝑥 ) 𝑙𝑐 : fresh classical location Θ𝑡 , |𝜑⟩, 𝑠 → Θ𝑡 [status(𝑡) = Ready, loc𝑡 [𝑥 ↦→ [ ], 𝑦 ↦→ [𝑙𝑐 ] ] ], |𝜓 ⟩, 𝑠 [𝑙𝑐 ← 0] status(𝑡) = Check(let… view at source ↗
Figure 23
Figure 23. Figure 23: Execution rules for checked statement The first condition checks that the linear vertices 𝑤𝑗 , whose location loc𝑡 (𝑤𝑗) is where we want to apply 𝑈 , is pebbled by 𝑞𝑗 {Control(𝑡)}. The second condition checks that the control qubits 𝑣𝑖 are pebbled by 𝑝𝑖s. For convenience, we assume that 𝑝𝑖s are main labels. The last condition checks that no pebbles on the graph are fragmented by 𝑤𝑗s. Rules for Checked Sta… view at source ↗
Figure 24
Figure 24. Figure 24: Rules for waking up threads Rules for waking up threads [PITH_FULL_IMAGE:figures/full_fig_p046_24.png] view at source ↗
Figure 25
Figure 25. Figure 25: Rules of execution for 𝑆𝑡 = (let𝑦 = 𝑒; 𝑆 ′ ) that do not create new thread Rules for the execution of expressions (with new threads) [PITH_FULL_IMAGE:figures/full_fig_p047_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: Rules of execution for 𝑆𝑡 = (let𝑦 = 𝑒; 𝑆 ′ ) that create new thread The special case is when this qif expression is nested, and the outer qif expression is con￾trolled by the same qubit. In this case, it only makes sense to execute one branch. For example, qif 𝑥 {qif 𝑥 𝐵|1⟩ else 𝐵|0⟩ }, is equivalent to qif 𝑥 𝐵|1⟩ . Therefore, we create only one new thread Θ𝑡 ′ that executes the branch 𝐵|𝑖⟩ , Rules for th… view at source ↗
Figure 27
Figure 27. Figure 27: Rules of execution for statements • If 𝑣 ∈ 𝑉init, then 𝐹𝑣 is the constant function from the singleton set 0: {∗} → {0, 1}. • If 𝑣 ∈ 𝑉gate, and the sources of incoming edges are 𝑣0, . . . , 𝑣𝑛 where 𝑣0 is the target, then 𝐹𝑣 is defined by 𝐹𝑣0 ⊕ [PITH_FULL_IMAGE:figures/full_fig_p049_27.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces Qurts, an extension of the Rust type system to quantum programming. Types are parameterized by lifetimes so that quantum data may be used affinely within a lifetime and must be used linearly outside it; this is claimed to yield a uniform substructural type system supporting automatic uncomputation. Two operational semantics are supplied: one simulation-based and one independent of any particular uncomputation strategy.

Significance. If the operational semantics are shown to be sound with respect to the type rules, the work supplies a uniform, non-ad-hoc mechanism for the linear-to-affine transition required by automatic uncomputation. The explicit provision of two distinct semantics (simulation-based and strategy-independent) is a concrete strength that supports reproducibility and strategy-agnostic reasoning.

minor comments (3)
  1. [Abstract] The abstract states that the lifetime parameterization 'permits' affine use inside a lifetime and 'restricts' linear use outside it, but does not indicate whether the type rules enforce the restriction or merely allow it; a concrete example of a well-typed term that would be rejected without the lifetime discipline would clarify the claim.
  2. The two operational semantics are introduced without a statement of their relationship (e.g., whether the strategy-independent semantics is a quotient or abstraction of the simulation semantics). Adding a short paragraph relating the two would strengthen the presentation.
  3. No mention is made of how the lifetime discipline interacts with measurement or with classical control flow; a brief discussion of these interactions would help readers assess applicability to realistic quantum programs.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending minor revision. The report accurately captures the core contribution of Qurts as a uniform framework for automatic uncomputation via lifetime-parameterized affine types, along with the provision of both simulation-based and strategy-independent operational semantics. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central contribution is the introduction of a new parameterization of types by lifetimes in an extension of the Rust type system to quantum settings, allowing affine use during a lifetime and linear use outside it. This is presented directly as a uniform framework for automatic uncomputation without any reduction to fitted parameters, self-definitional equations, or load-bearing self-citations. The abstract and description frame the work as a novel extension addressing ad hoc prior approaches, with operational semantics provided as independent support. No steps in the derivation chain reduce by construction to the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the domain assumption that quantum information must be treated linearly and on the paper-specific choice to use lifetimes to mediate between linear and affine regimes; no free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption Quantum information has to be treated linearly by the type system
    Explicitly stated in the abstract as the starting requirement that automatic uncomputation must respect.
  • ad hoc to paper A substructural type system between linear and affine can be captured uniformly by lifetime parameterization
    The key modeling choice that the paper introduces to solve the ad-hoc problem mentioned in the abstract.

pith-pipeline@v0.9.0 · 5673 in / 1377 out tokens · 43177 ms · 2026-05-23T17:13:43.187904+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages

  1. [1]

    In 47th ACM/IEEE Annual International Symposium on Computer Architecture, ISCA 2020, Virtual Event / Valencia, Spain, May 30 - June 3, 2020

    SQUARE: Strategic Quantum Ancilla Reuse for Modular Quantum Programs via Cost-Effective Uncomputation. In 47th ACM/IEEE Annual International Symposium on Computer Architecture, ISCA 2020, Virtual Event / Valencia, Spain, May 30 - June 3, 2020 . IEEE, 570–583. https://doi.org/10.1109/ISCA45697.2020.00054 Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Seli...

    work page doi:10.1109/isca45697.2020.00054 2020

  2. [2]

    fresh location

    ScaffCC: Scalable compilation and analysis of quantum programs. Parallel Comput. 45 (2015), 2–17. https: //doi.org/10.1016/j.parco.2014.12.001 Niels Kornerup, Jonathan Sadun, and David Soloveichik. 2024. Tight Bounds on the Spooky Pebble Game: Recycling Qubits with Measurements. arXiv:2110.08973 [quant-ph] Arun Kumar Pati and Samuel L. Braunstein. 2000. I...

    work page doi:10.1016/j.parco.2014.12.001 2015