PaperlayerView exact revision on arXiv

Source-linked AI summary

Quantisation of Abstract Data Types

Mingsheng Ying, Zhicheng Zhang, Kean Chen

arXiv:2609.03778v1quant-phcs.PLcs.SE

TL;DR

Quantum programming research has focused more on algorithms than on data, while data abstraction raises questions about how to specify quantum data types. The paper develops a universal-algebraic framework for quantising classical types, lifting their specifications, and relating quantum examples to classical structure. It concludes that the construction covers bit- and phase-oracle methods and applies to arrays and error-correcting codes, while limiting its scope to two quantisation forms and purely quantum ADTs.

  • Problem

    Quantum programming has focused more on algorithms than data, leaving the data aspect less investigated and raising the question of how classical data types can be specified in the quantum setting.

    Source: §1 · p. 1, §4 · p. 10

  • Method

    The paper defines abstract quantum data types and a universal-algebraic quantisation of classical data types, with bit- and phase-oracle quantisations as special cases.

    Source: §9 · p. 27

  • Results

    The paper shows that equational specifications lift soundly to quantisations and establishes conditions for preserving embeddings, isomorphisms, and products.

    Source: §9 · pp. 27–28

  • Takeaways & Limitations

    Quantum arrays and quantum error-correcting codes illustrate how quantum data and operations can be organised and specified through data-type quantisation.

    Source: §9 · p. 28

    The paper considers only bit- and phase-oracle quantisations and purely quantum ADTs, leaving other forms and classical-quantum hybrid ADTs for future research.

    Source: §9 · p. 28

Abstract

from arXiv · show

In this paper, we introduce a notion of abstract quantum data type within the framework of universal algebra. This notion provides an algebraic foundation for describing data abstraction in quantum programming. We formally define a quantisation of classical data types and show that their equational specifications can be soundly lifted to the quantum setting. Two standard quantisation methods for classical functions, namely the bit oracle and the phase oracle, arise as special cases of this general construction. We illustrate the framework with applications to quantum arrays and quantum error-correcting codes, showing how they can be understood through the lens of data-type quantisation. We further establish conditions under which quantisation preserves structural relationships and constructions of classical data types, including embeddings, isomorphisms, and products.

1 INTRODUCTION

Quantum programming has focused more on algorithms than on data, leaving data abstraction less investigated. This paper develops a universal-algebraic approach to abstract quantum data types and to quantising classical data types.

1.2 Data abstraction: from classical to quantum programming

  • Data abstraction is less investigated in quantum programming than algorithmic research, motivating the question of how to define abstract quantum data types and lift classical types.The paper frames high-level abstraction as relevant to respecting quantum constraints and avoiding dependence on specific hardware or gate sets.Source: §1 · p. 1, §1.2 · p. 2, §1.3 · p. 2

1.1 Data types and data structures in quantum programming

  • Prior work includes quantum data types in programming languages and Tower’s data structures in superposition, including quantised lists, stacks, queues, strings, and sets [40].Source: §1.1 · pp. 1–2

1.4 Contributions of this paper

  • The paper defines abstract quantum data types in universal algebra and introduces classical-data-type quantisation, proving that equational specifications lift soundly to the quantum setting.Generalised bit-oracle and phase-oracle quantisations are special cases.Source: §1.4 · p. 3
  • Under suitable conditions, quantisation preserves embeddings, isomorphisms, and products; embedding preservation carries some classical inheritance relationships to quantum counterparts.Quantum arrays and quantum error correction illustrate the framework.Source: §1.4 · p. 3

1.3 Abstract data types

  • An abstract data type specifies data, operations, and their rules independently of concrete representation, separating the user-facing interface from implementation.Source: §1.3 · p. 2, §2 · p. 3

2.1 Basics of Universal Algebra

  • Universal algebra formalises ADTs through signatures that specify interfaces, algebras that interpret domains and operations, and equations that state operation rules.Source: §2.1 · pp. 3–4

2.2 Specification of ADTs

  • An ADT specification comprises a signature and a set of equations, and its algebras are those satisfying every equation; the paper mainly considers equational specifications.Source: §2.2 · pp. 4–5

3 QUANTUM DATA TYPES

Section 3 generalizes algebraic specification techniques for classical ADTs to quantum computing, defining quantum data types in universal algebra and illustrating the framework with examples.

3.1 Basic Definitions

  • Quantum signatures specify quantum sorts, state symbols, and gate symbols; quantum algebras interpret sort domains as Hilbert spaces and symbols as pure states and unitary operators.The paper focuses on pure states and unitary gates, while noting that the definitions can be generalized to mixed states and quantum channels.Source: §3.1 · p. 6
  • Quantum terms represent circuits applied to initialized variables, whose input states may be entangled.Circuit formulas compose gates, and a quantum term can also represent a circuit with no initialized variables.Source: §3.1 · p. 7
  • Quantum equations require equality for every possible input state, allow entangled inputs, and compare reduced states on designated principal variables.Validity is defined by comparing the reduced density operators on those variables.Source: §3.1 · p. 8

3.2 Specification of Quantum Data Types

  • A quantum specification pairs a quantum signature with equations, and its algebras are those satisfying every equation.The QBIT example specifies NOT, Hadamard, and CNOT behavior, and the constructed algebra satisfies all QBIT equations.Source: §3.2 · pp. 8–9

3.3 A Simple Application Example: Programming Quantum Query Algorithms

  • Quantum query algorithms are introduced as circuits that query a black-box unitary oracle, using separate work and output qubits.The passage identifies the work and output registers as disjoint strings of qubits.Source: Quantum query algorithms · p. 9

Quantum query algorithms.

The section treats quantum oracles as abstract data types and explains how classical data types and their specifications are quantised into bit-oracle and phase-oracle forms. It also describes how phase kickback relates these forms when they share quantum domains, including changes to classical-data encoding through preO and postO.

Oracles as ADTs

  • A quantum query programmer can specify an oracle through an ADT without knowing its implementation details.The oracle is constrained by the specification it must satisfy.Source: Oracles as ADTs · pp. 9–10

4 QUANTISATION OF DATA TYPES

  • Quantisation maps classical sorts and constants to quantum counterparts and each operation to a gate with preprocessing and postprocessing.The preprocessing and postprocessing represent classical data in the quantum setting, while the operation gate lifts the classical operation; its action agrees on classical inputs.Source: §4 · pp. 10–11
  • If SUM_s maps |a⟩|b⟩ to |a⟩|a⊞_s b⟩, the lifted equations make the quantised algebra a model of the quantised specification.The theorem assumes a classical specification, a signature quantisation, and SUM_s gates for each sort.Source: §4 · pp. 12–13

4.1 Bit Oracle Quantisation

  • With identity bit labeling and XOR addition, BO-quantisation yields the common bit oracle, whose target qubit stores f(x) so the oracle is unitary.The input qubits record x and the last qubit stores the computational outcome f(x).Source: §4.1 · pp. 13–14

4.2 Phase Oracle Quantisation

  • PO-quantisation applies an output-dependent phase and yields the common controlled phase oracle when bit labeling is the identity, ω = −1, and QFT2 = H.Here H is the Hadamard operator.Source: §4.2 · p. 14

4.3 Phase Kickback Trick

  • Phase kickback connects bit and phase oracles: initializing the target register in |−⟩ makes the phase (−1)^f(x) appear before the quantum state.The passage presents this connection through the Deutsch-Jozsa algorithm.Source: §4.3 · pp. 14–15
  • When BO- and PO-quantisations of the same algebra share the same quantum domain for each sort, phase kickback relates the two quantisations.Source: §4.3 · p. 15
  • The relation amounts to changing how classical data are encoded through preO and postO.Source: §4.3 · p. 15

5 ILLUSTRATIVE APPLICATION I: QUANTUM ARRAYS

The section presents quantum arrays as a quantisation of the classical array ADT, whose read and write operations are specified by axioms. The quantum operations support coherent access and updates, but a natural quantum analogue of classical extensionality does not hold.

5.1 Classical Arrays

  • The classical array ADT treats arrays as functions from index tuples to values and provides selector read and store write operations.Read returns the value at an index; write returns an array updated at that index.Source: §5.1 · pp. 15–16

5.2 Quantum Arrays

  • A qread operation coherently loads values from multiple addresses when the address is in superposition.For the stated identity-bijection example, qread implements a QRAM read.Source: §5.2 · p. 17
  • A qwrite operation coherently writes data to multiple addresses in one operation.For the stated identity-bijection example, qwrite implements a QRAM swap.Source: §5.2 · pp. 17–18
  • Quantum arrays satisfy a specification relating qwrite followed by qread to SUM followed by qwrite.The proposition gives an equation analogous to the first part of the classical read-over-write axiom.Source: §5.2 · p. 18
  • A natural quantum analogue of classical extensionality fails because subsystem states do not uniquely determine the state of a composite system.The failure is noted even for the simplest case with index and value domains Z2.Source: §5.2 · p. 18

6 ILLUSTRATIVE APPLICATION II: QUANTUM ERROR CORRECTION

The section illustrates data-type quantisation by moving from a classical 3-bit repetition code to its quantum counterpart. The quantum construction encodes logical states, extracts syndromes, and specifies correction after a single Pauli X error.

6.1 Classical Repetition Code

  • The classical 3-bit repetition code encodes a logical bit by repeating it three times and uses majority correction to recover after a flip of any physical bit.Its correction operation leaves code words unchanged.Source: §6.1 · pp. 18–19

Quantum encoding.

The quantum encoding gate maps logical states into physical arrays, with superposed inputs producing entangled physical qubits.

Quantum encoding.

  • The quantised encoding gate has logical-qubit input and quantum-array output sorts.The gate and its preprocessing and postprocessing symbols share these sorts.Source: Quantum encoding · p. 19
  • For a computational-basis input |x⟩, qenc produces |x,x,x⟩ and resets the logical bit to |0⟩.This is the stated behavior of the quantised 3-bit repetition-code encoding gate.Source: Quantum encoding · p. 20
  • When the logical qubit begins in superposition, the encoded physical qubits become entangled.This distinguishes the quantum encoding behavior from the stated computational-basis mapping.Source: Quantum encoding · p. 20

Quantum flip.

The section describes quantised flip and correction operations for repetition codes, then extends the construction to the Shor code. The Shor-code specification covers recovery from single-qubit Pauli X, Z, and Y errors, and therefore an arbitrary single-qubit error.

Quantum flip.

  • For the 3-qubit repetition code, qflip leaves the index unchanged and applies a Pauli X gate to the indexed physical qubit.It implements the classical flip operation in the computational basis.Source: Quantum flip · p. 20

Quantum correction.

  • The 3-qubit quantum repetition-code correction gate produces a syndrome and corrects computational-basis errors; its specification covers a single Pauli X error.For a code word, the syndrome is ⊥; otherwise, it identifies the unique physical bit differing from the majority value.Source: Quantum correction · p. 20

6.3 Shor Code

  • The 3-qubit quantum repetition code is limited to correcting a Pauli X error; the Shor code is introduced as an extension that corrects arbitrary single-qubit errors.The paper identifies the Shor code as the first quantum error-correcting code to correct an arbitrary single-qubit error.Source: §6.3 · p. 20
  • Shor-code qenc maps a computational-basis logical state into a Shor code word, while a superposed input becomes the corresponding superposition of code words.The construction is presented as a quantisation of a 9-bit repetition code.Source: §6.3 · pp. 20, 22
  • The Shor-code qflipX and qflipZ gates leave the index unchanged and apply the corresponding Pauli gate to the indexed physical qubit.The gates introduce the corresponding Pauli errors.Source: §6.3 · p. 22
  • The Shor-code syndrome records within-group error locations and group-level majority deviations, yielding a bijection between arrays and logical-bit–syndrome pairs.The syndrome distinguishes the information needed for correction of Pauli X, Z, and Y errors.Source: §6.3 · p. 22
  • The Shor-code specification states that correction recovers the code word after Pauli X, Z, and Y errors, covering an arbitrary single-qubit error.The Y case is represented by sequential application of qflipX and qflipZ.Source: §6.3 · p. 23

7 EMBEDDINGS OF QUANTUM DATA TYPES

The section asks when classical structural relationships lift through quantisation, focusing on embeddings and isomorphisms. It gives conditions for the induced maps between quantum algebras to preserve those relationships.

7 EMBEDDINGS OF QUANTUM DATA TYPES

  • An embedding between quantum algebras consists of isometric maps on each sort that preserve state symbols and commute with gate operations.The classical definition similarly requires operation preservation, with injective maps defining an embedding.Source: §7 · p. 24

7.1 Embeddings of Quantisations

  • The induced map sends each basis state for a classical value to the basis state for its image; it is isometric for injective maps and unitary when the classical map is an isomorphism.The quantum embedding condition also requires the induced map to preserve state symbols and commute with gates.Source: §7 · p. 24, §7.1 · p. 25
  • Under the proposition’s conditions, an embedding between classical algebras induces an embedding between their bit-oracle quantisations.The induced map is isometric when the classical maps are injective.Source: §7.1 · p. 25
  • For phase-oracle quantisations, the section gives an isomorphism result rather than an embedding result because Fourier-transform compatibility forces the classical maps to be surjective.Under the proposition’s conditions, the induced map is an isomorphism between the quantised algebras.Source: §7.1 · pp. 25–26

8 PRODUCTS OF QUANTUM DATA TYPES

The section defines products of classical and quantum data types, combining their domains with Cartesian and tensor products, respectively. It then gives conditions under which quantisation preserves these products.

8 PRODUCTS OF QUANTUM DATA TYPES

  • The section frames products as a way to compose independently specified abstractions while preserving their interfaces and invariants.It relates classical Cartesian products to quantum tensor products and investigates when quantisation is compatible with the construction.Source: §8 · p. 26
  • The quantum product combines the domains of two quantum algebras with tensor products and defines state symbols and gates on the combined spaces.The corresponding classical product uses Cartesian products and applies each operation componentwise.Source: §8 · pp. 26–27

8.1 Products of Quantisations

  • Under the stated conditions, the product of two bit-oracle quantisations is isomorphic to the quantisation of the classical product.The proposition identifies the induced map J as an isomorphism from C to A ⊗ B.Source: §8.1 · p. 27
  • Under the stated conditions, the product of two phase-oracle quantisations is likewise isomorphic to the quantisation of the classical product.The proposition identifies J as an isomorphism from C to A ⊗ B.Source: §8.1 · p. 27

9 CONCLUSION

The paper develops a universal-algebraic framework for abstract quantum data types and proves that classical equations can be lifted soundly. It illustrates the framework and establishes conditions for preserving structural relationships, while limiting its scope to two quantisation forms and purely quantum ADTs.

9 CONCLUSION

  • The paper defines abstract quantum data types and classical data-type quantisation, and proves that equational specifications lift soundly to the quantum setting.Generalised bit-oracle and phase-oracle quantisations are instances of the construction and are related through phase kickback.Source: §9 · p. 27
  • The framework is illustrated with quantum arrays, the three-qubit repetition code, and the nine-qubit Shor code.These examples show how quantum data and operations can be organised and specified within the framework.Source: §9 · pp. 27–28
  • The paper establishes conditions under which quantisation preserves embeddings, isomorphisms, and products of classical data types.The paper describes data abstraction as a way to reason about complex quantum behaviour while enforcing quantum constraints.Source: §9 · p. 28
  • The study considers only bit-oracle and phase-oracle quantisations and purely quantum abstract data types.Classical-quantum hybrid abstract data types are identified as a future research topic.Source: §9 · p. 28

A DEFERRED PROOFS

The appendix supplies proofs for the paper’s main-text theorems and propositions. Its arguments verify sound equation lifting, the worked data-type examples, and preservation results for embeddings and products.

A DEFERRED PROOFS

  • The appendix provides proofs for the main-text theorems and propositions, beginning with a lemma used to prove Theorem 4.5.Theorem 4.5 is proved by showing that the quantised algebra satisfies the lifted equations.Source: A DEFERRED PROOFS · pp. 30–31
  • The array proof checks the two sides of the update equation on an array changed at index j, then concludes validity for any quantum state.The proof defines the updated array by retaining other entries and setting its jth entry to u.Source: A DEFERRED PROOFS · p. 31
  • The proofs establish Equations (23), (24), and (29) as valid; they show matching evaluations for (23) and (29), and examine an arbitrary q_l, q_i state for (24).Source: A DEFERRED PROOFS · pp. 32, 34
  • For the Shor-code construction, the appendix shows that the defined states can be extended to an orthonormal basis and verifies the correction equations.The correction operator maps the states indexed by the syndrome back to the encoded states.Source: A DEFERRED PROOFS · pp. 32–34
  • The embedding proofs verify that the induced maps preserve state symbols and gates, yielding embeddings and, for isomorphisms, quantum-algebra isomorphisms.The proofs use isometric induced maps and the classical homomorphism property.Source: A DEFERRED PROOFS · pp. 34–35
  • The product proofs verify that the induced map J preserves the quantum-algebra structure and is an isomorphism for both oracle quantisations.The arguments establish the gate condition for bit-oracle and phase-oracle products.Source: A DEFERRED PROOFS · pp. 35–37
Loading 2609.03778v1…