PaperlayerView exact revision on arXiv

Source-linked AI summary

Staged Hybrid Quantum-Classical Programming

Chuta Sano, Peng Fu, Ryan Kavanagh, Jennifer Paykin, Brigitte Pientka

arXiv:2609.06743v1cs.PLcs.LO

TL;DR

Adaptive quantum programs must choose operations from measurement results within limited qubit coherence, while circuit compilation can outlast qubit lifetimes. HyQ stages circuit generation before runtime instrumentation; its formal results include a circuit-pre-generation corollary and a runtime-preservation theorem.

  • Problem

    Adaptive quantum programs choose operations from measurement results within limited coherence lifetimes, while circuit compilation can take orders of magnitude longer than qubit lifetimes.

    Source: §1 · pp. 1–2

  • Method

    HyQ uses metaprogramming to pre-generate quantum circuits and classical runtime code before a runtime language instruments the quantum co-processor.

    Source: §1 · p. 3, §2 · p. 4

  • Results

    The paper states a Compilation Pre-Generates Circuits corollary and proves runtime preservation.

    Source: §4.1.3 · p. 17, §4.2.3 · p. 19

  • Takeaways & Limitations

    Precomputing circuits trades larger binaries for reduced quantum co-processor idling at runtime.

    Source: §1 · p. 2

    The authors do not mechanize proofs of preservation of mode safety, which they believe follow from prior Proto-Quipper-A mechanization.

    Source: §5.4 · p. 21

Abstract

from arXiv · show

Hybrid quantum-classical computing systems consist of a classical control system that sends quantum circuits and receives measurement results from a quantum co-processor. Such systems allow us to model algorithms that require the classical control system to generate quantum circuits on the fly, potentially based on prior measurement results. This is challenging, as the classical control system must generate quantum circuits that manipulate live quantum states. In this setting, the classical control system is generating further quantum circuits while the quantum co-processor is internally maintaining the state of the live qubits; this is not ideal, since this not only is costly but also introduces additional sources of noise to the live qubits. Thus, we want to minimize the latency between receiving measurement results and sending the next quantum circuit to be executed by pre-computing quantum circuits. We introduce HyQ (pronounced haiku), a multi-modal language based on adjoint logic that pre-generates quantum circuits before executing a hybrid quantum-classical program. We achieve this by separating our semantics into two distinct stages: 1) compile-time generation of quantum circuits and classical runtime code and 2) execution of the classical runtime code that instruments the quantum co-processor. This separation between stages allows us to formally guarantee that all circuit-generation logic occurs before the instrumentation logic, i.e., the actual runtime, and minimizes the idling of the quantum co-processor at runtime. We give a type system, a circuit-normalization semantics for the compile-time stage, which eagerly performs all circuit-generation logic, and a runtime semantics for HyQ that corresponds to the second stage. We prove type preservation and progress for both semantics.

1 Introduction

HyQ separates quantum-circuit generation from runtime instrumentation, formally enforcing that circuits are generated before the quantum co-processor is instrumented. The design addresses the cost of generating circuits while live qubits must be maintained and the resulting tension between larger precomputed binaries and runtime idling.

1 Introduction

  • Adaptive measurement requires quantum-operation choices to depend on measurement results within the computer’s limited coherence lifetime.Examples include quantum error correction and lattice surgery, where repeated measurements detect and correct errors as they occur.Source: §1 · pp. 1–2
  • Circuit compilation can take orders of magnitude longer than qubit lifetimes, while on-the-fly generation makes the co-processor maintain live qubits during classical work.Earlier dynamic-lifting formulations generate circuits from prior measurement results at runtime, adding cost on the co-processor.Source: §1 · p. 2
  • Precomputing circuits trades larger binaries for less quantum co-processor idling, a trade-off the authors argue is often worthwhile given the relative scarcity of quantum resources.The paper motivates a language that ensures circuits are pre-generated at compile time.Source: §1 · p. 2
  • HyQ combines a metaprogramming language, a quantum circuit language, and a minimal classical runtime language; the modular design allows metaprogramming extensions without changing runtime features.The runtime language embeds circuits, requests measurements, and branches on measurement results.Source: §1 · p. 3
  • HyQ separates compile-time circuit generation from runtime instrumentation, with semantics that ensure all circuits are pre-generated before runtime.Its metaprogramming language generates quantum circuits and classical runtime code; the runtime program instruments the co-processor.Source: §1 · p. 3
  • HyQ formalizes the staged approach with type preservation and progress for both semantics, plus a normal-forms theorem for circuit generation.The normal-forms theorem establishes that circuit-generation logic completes during circuit-generation time.Source: §1 · p. 3

2 Gentle Introduction to HyQ through Examples

HyQ uses a metaprogramming language to generate quantum circuits and classical runtime code before execution. Its examples show how these programs can generate, compose, and reuse circuits and hybrid runtime programs.

2 Gentle Introduction to HyQ through Examples

  • HyQ pre-generates the circuits that its classical control system can send, while generating the classical runtime code that executes alongside them.The metaprogramming language generates both components before execution.Source: §2 · p. 4, Figure 2 · p. 4

2.1 Circuit Generation

  • Quantum circuits are linear lambda-calculus terms, so quantum data cannot be duplicated or discarded; gates act as typed functions on qubits.Suspended circuit code can refer to metaprogramming terms, enabling programmatic generation of circuit families.Source: §2.1 · pp. 4–5
  • Metaprogramming can generate circuit families, compose circuits, and initialize qubits from scratch.A recursive list fold generates a circuit applying listed circuits in sequence.Source: §2.1 · p. 5

2.2 Classical Code Generation

  • The classical runtime language embeds circuits, measures live qubits, and branches on results, as in teleportation’s measurement-controlled corrections.The teleportation example uses measurement results to control Z and X operations on the destination qubit.Source: §2.2 · p. 6
  • Separately generated circuits can be referenced from runtime code, allowing libraries of commonly used circuit families to be pre-generated and reused.The runtime code refers to a generated circuit via force.Source: §2.2 · p. 8
  • The metaprogramming language can generate and manipulate families of classical runtime programs, supporting code reuse and domain-specific optimizations.Repeat-until-success programs that simulate gates are one example that can be used in larger algorithms.Source: §2.2 · p. 8
  • The proposed programming pipeline generates quantum code, uses it in generated classical code, then executes the classical code on the control system and quantum code on the co-processor.The classical runtime language is intended to be composed into a larger program that supplies its required input qubit reference.Source: §2.2 · pp. 7–8

3 Adjoint Logic as a Foundation for Quantum Programming

HyQ uses adjoint logic to organize a functional metaprogramming language, quantum circuits, and classical runtime code into modes with controlled dependencies. Its language design extends circuit generation with runtime interaction, then separates circuit normalization from execution of normalized classical code.

3 Adjoint Logic as a Foundation for Quantum Programming

  • Adjoint logic organizes multiple languages as modes, with permitted shifts controlling how terms in one mode can refer to terms in another.The mode ordering restricts which assumptions terms may depend on.Source: §3 · p. 8

3.1 Quantum Circuit Generation

  • The circuit-generation fragment uses unrestricted U, linear L, and quantum Q modes, with shifts supporting staged code generation and execution.Suspended code is treated as syntax until forced; downshifted terms are reduced.Source: §3.1 · pp. 9–10

3.1.1 Quantum Circuit Language.

  • The Q mode is a linear lambda calculus for circuits, with qubits as its base type and first-order functions over simple types.Initialization and discarding are represented by constants, and gates such as Hadamard and CNOT are uninterpreted function constants.Source: §3.1.1 · p. 10

3.1.2 Functional Metaprogramming Language.

  • The U/L metaprogramming language can capture Q-mode circuit terms, then lift closed circuit code into U for duplication or discarding.The passage describes circuit code closed with respect to L and Q assumptions as liftable into U and forceable back for reuse.Source: §3.1.2 · p. 11

3.2 Adding a Classical Runtime Language

  • HyQ adds linear C and unrestricted W runtime modes; C supports circuit execution, measurement-based branching, and loops that may not terminate.Measurement yields a classical bit, and the loop encoding suffices for hybrid algorithms; a more general fixed-point operation can use an affine runtime mode.Source: §3.2 · pp. 11–13

3.3 Instrumenting a Quantum Program

  • Circuit normalization fully reduces generated C code before runtime, which executes normalized C terms and their interactions with the quantum co-processor.Normalized C terms contain no U- or L-mode subterms, so embedded quantum circuits have already been precomputed.Source: §3.3 · p. 13

4 Operational Semantics and Metatheory

HyQ gives separate circuit-normalization and runtime semantics: normalization evaluates circuit-generation logic before runtime, and runtime semantics executes the resulting classical programs with the quantum co-processor. The section establishes preservation, progress, and pre-generation properties for these semantics.

4.1 Circuit-Normalization Semantics

  • Circuit-normalization uses small-step rewriting, reducing metaprogramming logic while ensuring classical and embedded quantum terms eliminate their metaprogramming subterms.Its rules include reductions under functions and neutral-blocked matches, and classical reductions under fixed points and conditionals.Source: §4.1 · pp. 13–14, §4.1.2 · p. 15

4.1.1 Normal Forms.

  • Normal forms in quantum and classical modes may include matches blocked on neutral terms, allowing compilation to normalize their bodies without evaluating uninterpreted gates or measurements.Measurement bodies may contain matches on neutral terms; commuting those matches out could cause multiple quantum co-processor requests.Source: §4.1.1 · p. 14

4.1.3 Properties of the Circuit-Normalization Semantics

  • Circuit-normalization also satisfies a substitution property, which the paper uses to handle substitution cases in the type-preservation proof.The property combines contexts for a typed term and a typed value substituted into it.Source: §4.1.2 · p. 16, §4.1.3 · p. 16
  • Circuit-normalization preserves types and satisfies progress: well-typed terms retain their type after reduction and are values or can step.The normal-forms lemma characterizes the shapes of normal terms by type and mode, supporting the progress result.Source: §4.1.3 · pp. 16–17
  • Compilation pre-generates circuits: a normalized classical program contains no metaprogramming subterms, including in its embedded quantum code.The compilation result is either such a normal form or can take another normalization step.Source: §4.1.3 · p. 17

4.2 Runtime Semantics

  • Runtime semantics executes normalized classical programs using closed terms paired with a quantum state and qubit identifiers.The quantum state is abstract and could be instantiated by a partial density matrix for simulation.Source: §4.2 · p. 17

4.2.2 Small-step Semantics.

  • At runtime, measurement updates the quantum state and returns a classical bit; conditionals then select a branch using that bit.The measured qubit is removed from the list of live identifiers.Source: §4.2.2 · pp. 17–18

4.2.3 Safety properties.

  • Runtime configurations satisfy preservation and progress: a well-typed configuration retains its type after a step and can step or is a value.The configuration typing condition combines a well-typed term with consistency between the quantum state and current qubit identifiers.Source: §4.2.3 · p. 19

5 Mechanization

The mechanization encodes a superset of HyQ in Beluga, using intrinsically typed terms and mode-safety predicates. It mechanizes progress proofs, while type preservation follows from the encoding and mode-safety preservation is not mechanized.

5 Mechanization

  • The paper mechanizes a superset of HyQ, its syntax and semantics, and progress proofs in Beluga.The encoding uses LF and Beluga’s reasoning framework for recursive, total functions over LF objects.Source: §5 · p. 19, §5.4 · p. 22

5.2 Terms

  • Terms are intrinsically typed by mode and type, with higher-order abstract syntax representing binders instead of explicit variables and binding forms.A generic match construct represents the language’s three let-style eliminators.Source: §5.2 · p. 20

5.3 Mode Safety Predicates

  • Mode-safety predicates check that bindings respect linear-use constraints and the mode ordering, and the paper mechanizes the independence principle for these predicates.A whole-term predicate recursively checks that each binding satisfies the local predicate.Source: §5.3 · pp. 20–21

5.4 Type-Preserving Reductions

  • Intrinsic typing gives type preservation for reductions by construction, but the mechanization does not prove that reductions preserve mode safety.The authors expect the latter to follow from the Proto-Quipper-A mechanization.Source: §5.4 · p. 21
  • The progress proofs for circuit-normalization and runtime are mechanized, and neither proof depends on the term satisfying mode safety.For circuit-normalization, progress means a term is normal or can step.Source: §5.4 · p. 22

6 Extending Each Layer

HyQ’s modular layers can be extended separately. The paper sketches metaprogramming extensions for circuit families and syntax analysis, as well as additional classical-runtime and quantum-runtime features.

6 Extending Each Layer

  • HyQ’s modular design allows extensions to one language layer without changing the others.This is especially relevant to metaprogramming, which the authors envision running without the runtime layer’s restrictions.Source: §6 · p. 22

6.1 Extending the Metaprogramming Language

  • Lists and recursion in the metaprogramming language can generate families of quantum circuits, with the recursor fully reduced during circuit-normalization.This keeps metaprogramming constructs out of normalized classical programs.Source: §6.1.1 · p. 22

6.1.1 Recursive Types and Recursion.

  • Metaprogramming could inspect and recursively traverse classical and quantum syntax to analyze or optimize hybrid programs, but type-safe matching requires significant work.The challenge includes matching open terms with binders while respecting linearity and context splits.Source: §6.1.1 · p. 23
  • Dependent types in the metaprogramming language could describe circuit families parameterized by values such as natural numbers.The paper gives generating circuits of a size specified by a natural number as an example.Source: §6.1.3 · p. 23

6.2 Extending 𝐶/𝑄

  • The minimal classical runtime layer could add common data types and operations, while quantum mode could support gates parameterized by classical values.The paper gives floating-point rotation angles for RX, RY, and RZ as examples.Source: §6.2 · pp. 23–24

7 Related Work

HyQ builds on prior quantum-circuit languages but adds a formalized classical runtime and a separation that pre-generates all circuits. Its design differs from approaches that generate circuits at runtime or encode dynamic control as branching circuits.

7 Related Work

  • Proto-Quipper-A [Kavanagh et al. 2026] shares HyQ’s adjoint modes and circuit-normalization approach, but does not model circuit execution or a classical runtime language.HyQ extends that framework with a classical runtime mode, runtime semantics, and their progress proofs.Source: §7 · p. 24
  • Unlike Proto-Quipper-Dyn [Fu et al. 2023], HyQ’s language-level separation pre-generates all quantum circuits rather than allowing runtime circuit generation after measurement.Proto-Quipper-Dyn uses a type system to limit runtime generation by boxing circuits or subcircuits without dynamic-lifting dependencies.Source: §7 · p. 24
  • Proto-Quipper-L [Lee et al. 2021] separates compilation from runtime with branching quantum channels, but each dynamic-lifting instance can double the structure’s size.HyQ instead handles the conditional in its classical runtime layer.Source: §7 · p. 25
  • Proto-Quipper-K [Colledan and Dal Lago 2023] represents dynamic lifting with generalized circuits that conditionally apply gates based on measurement results.The passage describes this representation as reflecting limited on-chip classical control.Source: §7 · p. 25
  • HyQ is not limited to conditional circuit applications and can support richer runtime operations, including function calls or external library calls.The paper contrasts this with generalized circuits that remain limited to conditional circuit applications.Source: §7 · p. 25
  • HyQ’s separation of classical and quantum operations remains relevant for adaptive hardware because it groups operations for classical and quantum compiler optimization.The paper connects quantum grouping to circuit optimization and classical grouping to existing classical optimization infrastructure.Source: §7 · pp. 25–26

8 Conclusion

HyQ separates circuit normalization from runtime execution and formalizes both stages, proving preservation and progress. The authors identify modularity and robustness from adjoint logic and sketch future directions.

8 Conclusion

  • HyQ formalizes circuit-normalization and runtime as distinct dynamics, with preservation and progress proved for both and mechanized in Beluga.The separation is presented as crucial because runtime keeps the quantum co-processor active and should be minimized.Source: §8 · p. 26
  • The authors describe adjoint logic as making HyQ modular and robust, and sketch future directions in Section 6.Source: §8 · p. 26

A.2 Substitution

The substitution rules define how substitution proceeds through variables, applications, and abstractions.

A.2 Substitution

  • Substitution leaves a matching variable unchanged, distributes over applications, and proceeds into a lambda abstraction’s body.Source: §A.2 · p. 29

A.3 Commuting Conversions for Circuit-Normalization Semantics

Circuit-normalization commuting conversions move matches outward across surrounding computations. Matches on unit or pairs can occur among C-terms and Q-terms.

A.3 Commuting Conversions for Circuit-Normalization Semantics

  • A unit or pair match may match C-terms on Q-terms, C-terms on C-terms, or Q-terms on Q-terms.Source: §A.3 · p. 29
  • A unit match around a function moves outside an application, preserving the match before applying the function.Source: §A.3 · p. 29
  • Nested unit and pair matches are reordered so the outer unit match precedes the inner match.Source: §A.3 · p. 29
  • A unit match moves outside a conditional; the text says pair elimination, down elimination, and conditionals have similar cases.Source: §A.3 · p. 29

B Select Cases for Theorems

The appendix states type preservation for circuit normalization and progress for circuit generation. Its selected proof cases use induction, congruence, substitution, and commuting conversions.

B Select Cases for Theorems

Loading 2609.06743v1…