Quantisation of Abstract Data Types

Quantisation of Abstract Data Types

arXiv:2609.03778v1 [quant-ph] 3 Sep 2026

MINGSHENG YING, University of Technology Sydney, Australia ZHICHENG ZHANG, Griffith University, Australia KEAN CHEN, University of Pennsylvania, USA 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. CCS Concepts: • Software and its engineering → Abstract data types; • Theory of computation → Quantum computation theory. Additional Key Words and Phrases: Quantum programming, abstract data types, universal algebra, quantisation, inheritance.

1

INTRODUCTION Algorithms + Data Structures = Programs — Niklaus Wirth [38]

Quantum programming research has been conducted for more than 30 years, beginning with Knill’s proposal of a set of conventions for writing quantum pseudocode [23], and it has become increasingly active in recent years [18, 39]. The majority of this research has focused on the algorithmic aspect of quantum programs. However, programming methodology must also study the structures, representations, and operations of data involved in large and complex programs [38]. To date, the data aspect of quantum programming has been less investigated. 1.1

Data types and data structures in quantum programming

Several basic quantum data types that abstract qubits and quantum registers are widely used in practical quantum programming languages, e.g. Qiskit [19], Q# [35], Cirq [6], Quipper [14], Guppy [24], Silq [3], Qrisp [32] and isQ [16]. Some more advanced quantum data types have been defined in theoretical research on quantum programming; for example, inductive quantum data types were introduced by Péchoux, Perdrix, Rennela and Zamdzhiev [31]. On the other hand, from the viewpoint of developer-friendly programming, a quantum programming language, Rhyme, with richer data types—including quantum extensions of floats, characters, arrays, and strings—was proposed by Varga, Aragonés-Soria and Oriol [36]. Various quantum data structures have been introduced for the design of quantum algorithms (see e.g. [1, 20, 21, 28, 37]). Yuan and Carbin’s Tower [40] provides the first programming language support for data structures in quantum superposition, including using random-access memory and Authors’ addresses: Mingsheng Ying, Centre for Quantum Software and Information, University of Technology Sydney, Sydney, Australia, Mingsheng.Ying@uts.edu.au; Zhicheng Zhang, School of Information and Communication Technology, Griffith University, Brisbane, Australia, iszczhang@gmail.com; Kean Chen, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, USA, keanchen.gan@gmail.com.

2

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

recursive definitions of operations. A library of quantisations of data structures lists, stacks, queues, strings, and sets is programmed in Tower. 1.2

Data abstraction: from classical to quantum programming

Data abstraction is a foundational concept in classical programming that allows a programmer to focus on what an object does rather than how it does it. It is the process of hiding complex implementation details while exposing only the essential features of an object or data type. Thus, it allows developers to work with abstract data types (e.g. integers, arrays, or linked lists) without worrying about memory layout or hardware details [25, 26]. We believe that data abstraction will play an even more critical role in quantum programming [8, 30] for at least the following two reasons: (1) Concepts such as superposition, entanglement, and measurement impose physical constraints that quantum data must respect but programmers may overlook or ignore. Therefore, data abstraction is essential for writing correct and scalable quantum software. (2) Hardware independence is essential in quantum programming because quantum hardware is evolving rapidly. High-level abstractions allow quantum algorithms to be expressed without being tied to a specific quantum device or gate set. Compilers then map these abstract representations onto real hardware, optimising for noise, connectivity, and error rates. Building upon previous work on quantum data structures [40] and quantum data types [36], we then naturally ask the following: Question 1. How can we realise data abstraction in quantum programming? 1.3

Abstract data types

The introduction of abstract data types (ADTs) is a key way of realising data abstraction [17]. An ADT specifies a data type by focusing on what it does rather than how it is implemented, and thus the internal representation is hidden from the user. ADTs are defined from a user’s viewpoint. In contrast, data structures are defined from an implementer’s viewpoint as concrete representations of data. ADTs encourage programmers to think at a higher level of abstraction. The main advantages of ADTs include: • By separating the interface from the implementation, programmers can change how an ADT is implemented without affecting the rest of the program. For example, a stack ADT is defined by operations such as push, pop, and peek, regardless of whether it is implemented using an array or a linked list. This makes code easier to maintain, understand, and reuse. • ADTs support modularity so that users interact only through well-defined operations. This can significantly improve software reliability because errors caused by directly manipulating data are reduced. Turning to the realm of quantum programming, Question 1 should be concretised to the following: Question 2. How can we define abstract quantum data types? Is there a principled way to lift classical data types to the quantum setting—what one might call the quantisation of data types? 1.4

Contributions of this paper

The aim of this paper is to introduce a method for the quantisation of data types that supports data abstraction in quantum programming. The main difference between our work and previous studies [36, 40] is that our approach operates at the level of abstract data types, whereas [36, 40] focus on

Quantisation of Abstract Data Types

3

less abstract levels, such as data structures and concrete data types. The technical contributions of this paper are threefold: (1) We formally define the notion of an abstract quantum data type within a universal-algebraic framework. (2) We introduce a quantisation of classical ADTs and prove that their equational specifications can be soundly lifted to the quantum setting. This notion includes generalisations of two basic quantisation methods for classical functions as important special cases. (3) We identify conditions ensuring that quantisation is compatible with structural relationships and constructions of classical data types, including embeddings, isomorphisms, and products. We complement these results with illustrative applications to quantum arrays and quantum error correction. We hope that the introduction of abstract quantum data types will help programmers design clean, flexible, and robust software systems for quantum computers. In particular, inheritance is a fundamental feature of object-oriented programming [5, 12], playing a crucial role in managing software complexity through mechanisms such as code reuse and hierarchical classification. The embedding result in Contribution (3) shows that certain algebraic inheritance relationships between classical data types can, under suitable conditions, be preserved under quantisation and transferred to their quantum counterparts. 1.5

Organisation of the paper

For the convenience of the reader, the basic concepts of ADTs are reviewed in Section 2. The notion of a quantum data type is introduced in Section 3, where several simple examples are also given to illustrate how quantum ADTs can be used in quantum programming. Section 4 develops a quantisation of classical ADTs and shows how equational specifications can be lifted to the quantum setting. It also presents two standard quantisation methods as special cases and explains their relationship through phase kickback. The framework is then illustrated through quantum arrays in Section 5 and quantum error correction in Section 6. Sections 7 and 8 investigate the structural properties of quantisation through embeddings and products, respectively. The paper concludes with a summary of the results and a brief discussion about topics for further research. The proofs of the main theorems and propositions are deferred to Appendix A. 2

ADTS IN CLASSICAL COMPUTING

In this section, we briefly review the basics of ADTs, following the textbook [9]. For more details, the reader can consult related chapters of [9]. A data type is a collection of data domains, designated basic data items, and operations on these domains. However, a programmer may not be interested in the concrete representation of a data type but only in its properties at an abstract level. Thus, the notion of ADT is introduced to specify the kinds of data that can be stored, the operations that can be performed on that data, and the rules those operations satisfy, independently of their concrete representation. 2.1 Basics of Universal Algebra ADTs can be properly formalised in the mathematical language of universal algebra. A signature specifies the interface of an ADT. Formally, we have: Definition 2.1 (Signatures). A signature is a pair Sig = (𝑆, OP), where: (1) 𝑆 is a set of sorts; (2) OP is a set of operation symbols. Each symbol 𝑂 ∈ OP is assigned input sorts in(𝑂) ∈ 𝑆 ∗ (the set of strings of elements in 𝑆, including the empty string 𝜖) and an output sort out (𝑂) ∈ 𝑆.

4

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

We often write 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠 for in(𝑂) = 𝑠 1, . . . , 𝑠𝑛 and out (𝑂) = 𝑠. In particular, a constant symbol is an operation symbol 𝑐 :→ 𝑠 where the input sort in(𝑐) = 𝜖 is empty. Mathematically, a data type can then be modelled as an algebra as defined as follows: Definition 2.2 (Algebras). An algebra 𝐴 of a signature Sig = (𝑆, OP), or a Sig-algebra for short, consists of: (1) for each 𝑠 ∈ 𝑆, 𝐴𝑠 is a nonempty set, called the domain of sort 𝑠; (2) for each 𝑂 ∈ OP with 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠, 𝑂 𝐴 is a mapping 𝐴𝑠1 × · · · × 𝐴𝑠𝑛 → 𝐴𝑠 , called an operation. In particular, for each constant symbol 𝑐 :→ 𝑠, 𝑐 𝐴 is an element of 𝐴𝑠 . Throughout this paper, we only consider finite domains. The rules that the operations of an ADT must follow are usually specified as a family of equations. To define them, for each 𝑠 ∈ 𝑆, we assume a set 𝑋𝑠 of variables of sort 𝑠. The variable sets 𝑋𝑠 are required to be pairwise disjoint and also disjoint from the operation symbols OP. Then we can introduce the following definition. Definition 2.3 (Terms). The terms are recursively defined as follows: (1) every constant symbol 𝑐 :→ 𝑠 and every variable 𝑥 ∈ 𝑋𝑠 are terms of sort 𝑠; (2) if 𝑡 1, . . . , 𝑡𝑛 are terms of sorts 𝑠 1, . . . , 𝑠𝑛 , respectively, and 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠 ∈ OP, then 𝑂 (𝑡 1, . . . , 𝑡𝑛 ) is a term of sort 𝑠. A term without variables is called a ground term. The semantic interpretation of terms in a given algebra is presented through the notion of evaluation defined in the following: Definition 2.4 (Evaluation). Let 𝐴 be an Sig-algebra and 𝜎 an assignment in 𝐴 that maps each variable 𝑥 ∈ 𝑋𝑠 to an element 𝜎 (𝑥) ∈ 𝐴𝑠 for every sort 𝑠. Then the evaluation eval𝜎 (𝑡) of a term 𝑡 in assignment 𝜎 is recursively defined as follows: (1) if 𝑡 is a variable 𝑥, then eval𝜎 (𝑡) = 𝜎 (𝑥), and if 𝑡 is a constant 𝑐, then eval𝜎 (𝑡) = 𝑐 𝐴 ; (2) if 𝑡 = 𝑂 (𝑡 1, . . . , 𝑡𝑛 ), then eval𝜎 (𝑡) = 𝑂 𝐴 (eval𝜎 (𝑡 1 ), . . . , eval𝜎 (𝑡𝑛 )). As noted above, a large class of the rules for the operations in an ADT can be described by equations between terms. The notion of equations can be formally defined in the following: Definition 2.5 (Equations and Validity). (1) Let 𝑡 1 and 𝑡 2 be two terms of the same sort 𝑠. If all variables occurring in 𝑡 1 and 𝑡 2 are among 𝑥 1, . . . , 𝑥𝑛 , then 𝑒 = (∀𝑥 1 : 𝑠 1, . . . , 𝑥𝑛 : 𝑠𝑛 ) (𝑡 1 = 𝑡 2 ) (1) is called an equation, where 𝑥𝑖 is a variable of sort 𝑠𝑖 for every 𝑖 = 1, . . . , 𝑛. (2) The equation 𝑒 is valid in an algebra 𝐴, or 𝐴 satisfies 𝑒, written 𝐴 |= 𝑒, if for any assignment 𝜎 in 𝐴, we have eval𝜎 (𝑡 1 ) = eval𝜎 (𝑡 2 ). It is easy to see that the validity of equation 𝑒 only depends on the values 𝜎 (𝑥𝑖 ) (𝑖 = 1, . . . , 𝑛) of assignments 𝜎. In the specifications of ADTs in practical applications, universal quantifiers (∀𝑥 1 : 𝑠 1, . . . , 𝑥𝑛 : 𝑠𝑛 ) in Equation (1) are often omitted (see Example 2.7). If both 𝑡 1 and 𝑡 2 are ground terms, then 𝑒 is called a ground equation. The validity of a ground equation 𝑒 in an algebra does not depend on any assignment 𝜎 in 𝐴. 2.2

Specification of ADTs

Now we can use the algebraic framework defined in the previous subsection to specify ADTs. Definition 2.6 (Specifications). (1) A specification is a triple Spec = (𝑆, OP, 𝐸), where Sig = (𝑆, OP) is a signature, and 𝐸 is a set of equations over the signature Sig.

Quantisation of Abstract Data Types

5

(2) An algebra of the specification Spec, or Spec-algebra for short, is an algebra 𝐴 of signature Sig such that 𝐴 |= 𝑒 for every 𝑒 ∈ 𝐸. Besides the equational specifications defined above, there are more sophisticated classes of ADT specifications, such as Horn specifications. In this paper, we mainly consider equational specifications. For a better understanding of the notions introduced above, let us see the following simple example: Example 2.7 (Abstract data type of strings). A string is a sequence of basic data items from a given domain, called the alphabet. Let 𝑐 1, . . . , 𝑐𝑛 be constant symbols denoting the basic data items. The most useful operations of strings in practical applications are: • make: it converts each basic data item into a string of length 1; • concat: it concatenates two strings; • ladd, radd: they add a basic data item to the left and right ends of a string, respectively. A specification of strings is given as follows: STRING = sorts : alphabet, string operations : 𝑐 1, . . . , 𝑐𝑛 :→ alphabet empty :→ string make : alphabet → string concat : string, string → string ladd : alphabet, string → string radd : string, alphabet → string equations : 𝑎 : alphabet, 𝑠, 𝑠 1, 𝑠 2, 𝑠 3 : string concat (𝑠, empty) = 𝑠 concat (empty, 𝑠) = 𝑠 concat (concat (𝑠 1, 𝑠 2 ), 𝑠 3 ) = concat (𝑠 1, concat (𝑠 2, 𝑠 3 )) ladd (𝑎, 𝑠) = concat (make(𝑎), 𝑠) radd (𝑠, 𝑎) = concat (𝑠, make(𝑎)) We can define a STRING-algebra 𝐴 as follows: • Let 𝐴alphabet = {𝑎 1, . . . , 𝑎𝑛 } be a domain for the alphabet. Let 𝐴string = (𝐴alphabet ) ∗ be the set of strings of elements in 𝐴alphabet , including the empty string 𝜖. • For constant symbols, define 𝑐𝑖𝐴 = 𝑎𝑖 for 𝑖 = 1, . . . , 𝑛 and empty𝐴 = 𝜖. • For nonconstant operation symbols, define (1) make𝐴 : 𝐴alphabet → 𝐴string , make𝐴 (𝑎) = 𝑎 for all 𝑎 ∈ 𝐴alphabet ; (2) concat 𝐴 : 𝐴string × 𝐴string → 𝐴string , concat 𝐴 (𝑢, 𝑣) = 𝑢𝑣 for all 𝑢, 𝑣 ∈ 𝐴string ; (3) ladd 𝐴 : 𝐴alphabet × 𝐴string → 𝐴string , ladd 𝐴 (𝑎, 𝑢) = 𝑎𝑢 for all 𝑎 ∈ 𝐴alphabet and 𝑢 ∈ 𝐴string ; (4) radd 𝐴 : 𝐴string × 𝐴alphabet → 𝐴string , radd 𝐴 (𝑢, 𝑎) = 𝑢𝑎 for all 𝑎 ∈ 𝐴alphabet and 𝑢 ∈ 𝐴string . It is easy to check that the above operations satisfy the equations in STRING, and hence 𝐴 is a STRING-algebra.

6

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

3

QUANTUM DATA TYPES

From now on, we generalise the algebraic specification techniques for classical ADTs into quantum computing. In this section, we formally define quantum data types in the universal-algebraic framework, analogously to their classical counterparts in Section 2, and illustrate it with some simple examples. 3.1

Basic Definitions

Let us first introduce the notion of a quantum signature as the quantum counterpart of Definition 2.1: Definition 3.1 (Quantum Signatures). A quantum signature is a triple QSig = (𝑆𝑞 , K, U), where: (1) 𝑆𝑞 is a set of quantum sorts; (2) K is a set of quantum state symbols. Each symbol |𝜓 ⟩ ∈ K is assigned sort sort (|𝜓 ⟩) ∈ 𝑆𝑞+ (the set of nonempty strings of elements in 𝑆𝑞 ); (3) U is a set of quantum gate symbols. Each symbol 𝑈 ∈ U is assigned sort sort (𝑈 ) ∈ 𝑆𝑞+ ; Roughly speaking, K and U correspond to the constant symbols and operation symbols in Definition 2.1, respectively. But there are some subtle differences between them and their classical counterparts. For a classical constant symbol 𝑐 :→ 𝑠, its input sort is empty and its output sort is a single sort 𝑠 ∈ 𝑆. However, for a quantum state symbol |𝜓 ⟩, it is possible that sort (|𝜓 ⟩) = 𝑠 1, . . . , 𝑠𝑛 ∈ 𝑆𝑞+ with 𝑛 > 1. The reason is that |𝜓 ⟩ may denote an entangled state between 𝑛 subsystems, which cannot be decomposed into a string of the states of individual subsystems. We often write |𝜓 ⟩ : 𝑠 1, . . . , 𝑠𝑛 for sort (|𝜓 ⟩) = 𝑠 1, . . . , 𝑠𝑛 . Moreover, for a classical operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠, the input sorts 𝑠 1, . . . , 𝑠𝑛 and the output sort 𝑠 need not coincide. In contrast, the input and output sorts of a quantum gate symbol 𝑈 must be the same because it denotes a unitary operator. We write 𝑈 : 𝑠 1, . . . , 𝑠𝑛 for sort (𝑈 ) = 𝑠 1, . . . , 𝑠𝑛 . Indeed, sort (𝑈 ) is both the input sort and output sort of 𝑈 . As the quantum counterparts of algebras described in Definition 2.2, quantum algebras are then defined by taking the domains of sorts to be Hilbert spaces and interpreting quantum state symbols and quantum gate symbols as pure quantum states and unitary operators, respectively. Definition 3.2 (Quantum Algebras). A quantum algebra A of signature QSig = (𝑆𝑞 , K, U) consists of: (1) for each 𝑠 ∈ 𝑆𝑞 , H𝑠A is a Hilbert space, called the quantum domain of sort 𝑠 (the superscript A of H𝑠A is often omitted for simplicity); (2) for each quantum state symbol |𝜓 ⟩ ∈ K with sort (|𝜓 ⟩) = 𝑠 1, . . . , 𝑠𝑛 , |𝜓 ⟩ A is a unit vector (i.e. a pure quantum state) in H𝑠1 ⊗ · · · ⊗ H𝑠𝑛 ; and (3) for each quantum gate symbol 𝑈 ∈ U with sort (𝑈 ) = 𝑠 1, . . . , 𝑠𝑛 , 𝑈 A is a unitary operator (i.e. a quantum gate) on H𝑠1 ⊗ · · · ⊗ H𝑠𝑛 . In this paper, we only consider quantum algebras where state symbols are interpreted as pure states and gate symbols as unitary operators. Of course, Definition 3.2 can be generalized such that state symbols are interpreted as mixed states (i.e. density operators) and gate symbols as noisy quantum gates (i.e. quantum channels) when needed in applications. Given a quantum signature QSig, we assume a set 𝑄 of quantum variables. Each 𝑞 ∈ 𝑄 is assigned a sort sort (𝑞) ∈ 𝑆𝑞 . For a string 𝑞 = 𝑞 1, . . . , 𝑞𝑛 of quantum variables, we define sort (𝑞) = 𝑠 = 𝑠 1, . . . , 𝑠𝑛 , where 𝑠𝑖 = sort (𝑞𝑖 ). When the context is clear, we also use 𝑞 to denote the set {𝑞 1, . . . , 𝑞𝑛 }. Then the notion of term is generalised to the quantum case as follows: Definition 3.3 (Quantum Circuit Formulas and Terms).

Quantisation of Abstract Data Types

7

(1) Quantum circuit formulas 𝐶 and their quantum variables qv(𝐶) are inductively defined as follows: (a) if 𝑈 : 𝑠 1, . . . , 𝑠𝑛 is a quantum gate symbol and 𝑞 = 𝑞 1, . . . , 𝑞𝑛 is a string of distinct quantum variables with sort (𝑞𝑖 ) = 𝑠𝑖 for 𝑖 = 1, . . . , 𝑛, then 𝐶 = 𝑈 [𝑞] is a quantum circuit formula, and qv(𝐶) = 𝑞; (b) if 𝐶 1 and 𝐶 2 are quantum circuit formulas, then 𝐶 = 𝐶 1 ; 𝐶 2 is a quantum circuit formula, and qv(𝐶) = qv(𝐶 1 ) ∪ qv(𝐶 2 ). (2) Suppose 𝐶 is a quantum circuit formula. For 𝑖 = 1, . . . , 𝑛, let |𝜓𝑖 ⟩ : 𝑠𝑖 be a quantum state symbol and 𝑞𝑖 be a string of distinct quantum variables with sort (𝑞𝑖 ) = 𝑠𝑖 and 𝑞𝑖 ∩ 𝑞 𝑗 = ∅ for 𝑖 ≠ 𝑗. Then 𝜏 = 𝐶 |𝜓 1 ⟩𝑞1 . . . |𝜓𝑛 ⟩𝑞𝑛 is a quantum term, and qv(𝜏) = 𝑞 1 ∪ . . . ∪ 𝑞𝑛 ∪ qv(𝐶). When the context is clear, |𝜓 ⟩𝑞 may be used to denote the string |𝜓 1 ⟩𝑞1 . . . |𝜓𝑛 ⟩𝑞𝑛 of quantum state symbols, where 𝑞 = 𝑞 1, . . . , 𝑞𝑛 . Define the set of free variables in quantum term 𝜏 to be fv(𝜏) = qv(𝜏) \ 𝑞. The definition of quantum terms above differs slightly from its classical counterpart in Definition 2.3. Obviously, a quantum circuit formula 𝐶 stands for a (combinational) quantum circuit constructed from quantum gates denoted by elements of U applied to quantum variables in 𝑄. Furthermore, a quantum term 𝐶 |𝜓 1 ⟩𝑞1 . . . |𝜓𝑛 ⟩𝑞𝑛 stands for a quantum circuit formula 𝐶 with quantum variables 𝑞 = 𝑞 1, . . . , 𝑞𝑛 initialised in the state |𝜓 1 ⟩ . . . |𝜓𝑛 ⟩, where each |𝜓𝑖 ⟩ can be entangled. Conversely, a quantum circuit formula 𝐶 can be seen as a quantum term with 𝑞 = ∅. A string of quantum state symbols |𝜓 ⟩𝑞 = |𝜓 1 ⟩𝑞1 . . . |𝜓𝑛 ⟩𝑞𝑛 can also be seen as a quantum term with empty 𝐶. Given an algebra A of a quantum signature QSig, for any subset 𝑄 ′ ⊆ 𝑄 of quantum variables, we write: Ì H𝑄 ′ =

Hsort (𝑞)

𝑞 ∈𝑄 ′

for the Hilbert space of the composite system 𝑄 ′ . Then an assignment of quantum variables in 𝑄 ′ can be understood as a quantum state |𝜑⟩ ∈ H𝑄 ′ , although there is a basic difference between it and an assignment of classical variables; that is, the values of two classical variables are independent, but |𝜑⟩ could contain entanglement. Furthermore, the notion of evaluation can be generalised straightforwardly to the quantum case. As usual, for a unitary operator 𝑈 , we implicitly identify it with its extension 𝑈 ⊗ 1 by tensoring with an identity operator 1. Definition 3.4 (Evaluation). (1) Let 𝐶 be a quantum circuit formula. Then its evaluation eval(𝐶) in algebra A is a unitary operator on Hqv (𝐶 ) recursively defined as follows: (a) if 𝐶 = 𝑈 [𝑞] for some 𝑈 ∈ U, then eval(𝐶) = 𝑈𝑞A (unitary operator 𝑈 A acting on the quantum system denoted by 𝑞); (b) if 𝐶 = 𝐶 1 ; 𝐶 2 , then eval(𝐶 1 ; 𝐶 2 ) = eval(𝐶 2 ) ◦ eval(𝐶 1 ) is a composition of unitary operators. (2) Let 𝜏 = 𝐶 |𝜓 1 ⟩𝑞1 . . . |𝜓𝑛 ⟩𝑞𝑛 be a quantum term. Suppose 𝑞 = 𝑞 1, . . . , 𝑞𝑛 and 𝑟 is a string of quantum variables such that 𝑟 ⊇ fv(𝜏) and 𝑟 ∩ 𝑞 = ∅. Let |𝜑⟩ be a quantum state in H𝑟 . Then the evaluation of 𝜏 in state |𝜑⟩ is defined as the quantum state:   eval |𝜑 ⟩ (𝜏) = eval(𝐶) |𝜓 1 ⟩𝑞A1 ⊗ . . . ⊗ |𝜓𝑛 ⟩𝑞A𝑛 ⊗ |𝜑⟩𝑟 . (2) Here, eval(𝐶) = 1 if 𝐶 is empty. The notion of equation can be smoothly generalised to the quantum setting too:

8

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

Definition 3.5 (Equations). Let 𝜏1 = 𝐶 1 |𝜓 1 ⟩𝑞1 and 𝜏2 = 𝐶 2 |𝜓 2 ⟩𝑞2 be two quantum terms that satisfy 𝑞 1 ∩ fv(𝜏2 ) = 𝑞 2 ∩ fv(𝜏1 ) = ∅. Suppose 𝑟 = fv(𝜏1 ) ∪ fv(𝜏2 ) and sort (𝑟 ) = 𝑠. Then, for 𝑝 ⊆ qv(𝜏1 ) ∩ qv(𝜏2 ), 𝑒 = (∀𝑟 : 𝑠) (𝜏1 = 𝜏2 ) ⇓ 𝑝

(3)

is called an equation, and 𝑝 are called the principal variables of 𝑒. In particular, if 𝑝 = qv(𝜏1 ) ∩qv(𝜏2 ), then ⇓ 𝑝 can be dropped from Equation (3). Similar to the case of classical equations, universal quantifiers (∀𝑟 : 𝑠) in Equation (3) are often omitted in practical specifications of quantum ADTs (see Example 3.8 and Proposition 5.1). It is worth examining carefully the differences between classical Equation (1) and quantum Equation (3). First, we notice that in terms 𝜏1 and 𝜏2 , quantum variables 𝑞 1 and 𝑞 2 are already initialised, but 𝑟 are not. Thus, Equation (3) means that the equality between 𝜏1 and 𝜏2 is valid for all possible input states of 𝑟 . Second, an input state |𝜑⟩𝑟 of 𝑟 = 𝑟 1, . . . , 𝑟𝑛 may be entangled. Third, the evaluation of 𝜏1 (resp. 𝜏2 ) gives an output state |𝜓 1 ⟩ (resp. |𝜓 2 ⟩) of multiple quantum variables, but one may only be interested in a subset 𝑝 of them. Thus, the variables in 𝑝 are designated as the principal variables. Consequently, to define the validity of equations in a quantum algebra, we need the notion of a reduced density operator. For a quantum state |𝜓 ⟩ in Hilbert space H𝑝 ⊗ H𝑝 ′ , the restriction of |𝜓 ⟩ onto 𝑝 is defined as the reduced density operator |𝜓 ⟩ ↓ 𝑝 = tr𝑝 ′ (|𝜓 ⟩⟨𝜓 |) where tr𝑝 ′ stands for the partial trace over subsystem 𝑝 ′ (see Section 2.4.3 of [29] for its precise definition). Intuitively, |𝜓 ⟩ ↓ 𝑝 describes the state of subsystem 𝑝 when the whole system 𝑝 ⊎ 𝑝 ′ is in state |𝜓 ⟩ . With this preparation, we are able to introduce: Definition 3.6 (Validity). The equation 𝑒 given in Equation (3) is valid in algebra A, written A |= 𝑒, if for any quantum state |𝜑⟩ ∈ H𝑟 , we have: eval |𝜑 ⟩ (𝜏1 ) ↓ 𝑝 = eval |𝜑 ⟩ (𝜏2 ) ↓ 𝑝. 3.2

Specification of Quantum Data Types

As one may expect, the algebraic framework developed in the previous subsection can be used to specify ADTs in quantum computing. The following definition is a straightforward generalisation of Definition 2.6. Definition 3.7 (Quantum Specification). (1) A quantum specification is a quadruple QSpec = (𝑆𝑞 , K, U, 𝐸), where QSig = (𝑆𝑞 , K, U) is a quantum signature, and 𝐸 is a set of equations of the form in Equation (3). (2) A QSpec-algebra is a quantum algebra A of signature QSig such that A |= 𝑒 for every 𝑒 ∈ 𝐸. For a better understanding of quantum ADTs, let us first see the following simple example:

Quantisation of Abstract Data Types

9

Example 3.8 (Abstract data type of qubits). Consider the following quantum specification: QBIT = sorts : qbit states : |0⟩ , |1⟩ , |+⟩ , |−⟩ : qbit |𝛽 00 ⟩ , |𝛽 01 ⟩ , |𝛽 10 ⟩ , |𝛽 11 ⟩ : qbit, qbit gates : NOT, 𝐻 : qbit CNOT : qbit, qbit equations : 𝑞, 𝑞 1, 𝑞 2 : qbit NOT [𝑞] |0⟩𝑞 = |1⟩𝑞 , 𝐻 [𝑞] |0⟩𝑞 = |+⟩𝑞 ,

NOT [𝑞] |1⟩𝑞 = |0⟩𝑞 𝐻 [𝑞] |1⟩𝑞 = |−⟩𝑞

CNOT [𝑞 1, 𝑞 2 ] |+⟩𝑞1 |0⟩𝑞2 = |𝛽 00 ⟩𝑞1𝑞2 ,

CNOT [𝑞 1, 𝑞 2 ] |+⟩𝑞1 |1⟩𝑞2 = |𝛽 01 ⟩𝑞1𝑞2

CNOT [𝑞 1, 𝑞 2 ] |−⟩𝑞1 |0⟩𝑞2 = |𝛽 10 ⟩𝑞1𝑞2 ,

CNOT [𝑞 1, 𝑞 2 ] |−⟩𝑞1 |1⟩𝑞2 = |𝛽 11 ⟩𝑞1𝑞2

We can define a QBIT-algebra A as follows: A • Let Hqbit = H2 be the 2-dimensional Hilbert space. • For quantum state symbols, define |𝑏⟩ A = |𝑏⟩ for 𝑏 ∈ {0, 1}, |±⟩ A = √1 (|0⟩ ± |1⟩), and 2

|𝛽𝑎𝑏 ⟩ A = √1 (|0⟩ |𝑏⟩ + (−1)𝑎 |1⟩ |1 − 𝑏⟩) for 𝑎, 𝑏 ∈ {0, 1}. 2 • For quantum gate symbols, define NOT A = 𝑋,

𝐻 A = 𝐻,

CNOT A = CNOT,

where 𝑋 , 𝐻 , and CNOT are the Pauli 𝑋 , Hadamard, and controlled-NOT gates, respectively. It is easy to check that A satisfies all equations in QBIT, and hence A is a QBIT-algebra. 3.3

A Simple Application Example: Programming Quantum Query Algorithms

Quantum query algorithms. To further understand the role of ADTs in quantum computing, let us consider a large class of quantum algorithms, namely quantum query algorithms. Let 𝑞 𝑤 and 𝑞𝑜 be two disjoint strings of qubits of lengths 𝑙 𝑤 and 𝑙𝑜 , called the work qubits and output qubits, respectively. Suppose we are given a quantum oracle O, which is a black-box unitary operator. Then a quantum query algorithm [2] with queries to O is usually described as a quantum circuit: 𝐶 = 𝑈𝑇 O𝑈𝑇 −1 · · · 𝑈 2 O𝑈 1 O𝑈 0 where 𝑈𝑡 (𝑡 = 0, 1, . . . ,𝑇 ) are quantum gates independent of O. The circuit 𝐶 is initialised in state |0⟩𝑞 𝑤 |0⟩𝑞𝑜 . Then the algorithm outputs 𝑥 (a bit string) with probability 2

Prob(𝑥) = ⟨𝑥 |𝑞𝑜 𝐶 |0⟩𝑞 𝑤 |0⟩𝑞𝑜 . Oracles as ADTs. Oracle synthesis functionality has already been integrated into quantum programming platforms like Qiskit [19] and Q# [35]. Ideally, a programmer does not need to know the implementation details of the oracle O when programming the quantum query algorithm. Instead, it can be viewed through the lens of ADTs. Consider a quantum specification (𝑆𝑞 , K, U, 𝐸), where qbit ∈ 𝑆𝑞 , O ∈ U, and sort (O) = qbit, . . . , qbit. The equations in 𝐸 may specify properties that | {z } 𝑙 𝑤 +𝑙𝑜

the oracle O should satisfy without fixing its implementation details. In this way, the quantum

10

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

query algorithm can be programmed as: 𝑃 ≡ 𝑞 𝑤 := |0⟩𝑙 𝑤 ; 𝑞𝑜 := |0⟩𝑙𝑜 ; for 𝑖 from 0 to 𝑇 − 1 do 𝑈𝑖 [𝑞]; O [𝑞];

(calling the oracle operation)

𝑈𝑇 [𝑞]; 𝑥 := 𝑀 [𝑞𝑜 ] where 𝑞 = 𝑞 𝑤 ∪ 𝑞𝑜 and 𝑀 is the measurement in the computational basis of 𝑞𝑜 . 4

QUANTISATION OF DATA TYPES

The abstract notion of quantum ADTs was introduced in Section 3. In practical applications, a quantum ADT does not stand alone; rather, it often arises as an extension of a corresponding classical ADT. An application scenario is that, when developing a quantum program, the programmer realises that they need to apply a function, or more generally an ADT, that does not comply with certain constraints (e.g., non-unitarity) imposed by quantum mechanics. In such cases, the function or ADT must be quantised, and what the programmer actually invokes in the program is its quantisation. A typical example is a quantum oracle (see Section 3.3), which is often lifted from a black-box classical function. So, in this section, we consider how a classical data type defined in Section 2 can be extended to a quantum data type introduced in Section 3. We call this extension process quantisation. In this section, we make the following conventions. Given a classical signature, for each sort 𝑠, we assume a designated constant symbol 0𝑠 :→ 𝑠. Given a quantum signature, for any sort 𝑠, we assume a designated quantum state symbol |0𝑠 ⟩ : 𝑠. For a string 𝑠 = 𝑠 1, . . . , 𝑠𝑛 of sorts, the quantum A state |0𝑠 ⟩ in a given algebra A is then |0𝑠1 ⟩ A ⊗ . . . ⊗ |0𝑠𝑛 ⟩ A . When the context is clear, we omit the subscript 𝑠 and use |0⟩ to abbreviate |0⟩ . . . |0⟩. These designated symbols are implicitly assumed to be included in the signatures discussed below. Given an algebra 𝐴 of a signature, for each sort 𝑠, we assume that 𝐴𝑠 is finite and there is a designated bijection 𝑘𝑠𝐴 : 𝐴𝑠 → Z |𝐴𝑠 | ,

𝑘𝑠𝐴 (0𝑠𝐴 ) = 0

(4)

where for a positive integer 𝑚, Z𝑚 = {0, 1, ..., 𝑚 − 1}. Intuitively, bijection 𝑘𝑠 (𝑎) gives the default integer label for every element 𝑎 ∈ 𝐴𝑠 ; that is, we use 𝑘𝑠 to enumerate all elements of 𝐴𝑠 . Let us first consider how a classical signature can be quantised to a quantum signature. Definition 4.1 (Quantisation of signature). Let Sig = (𝑆, OP) be a signature and QSig = (𝑆𝑞 , K, U) a quantum signature. A quantisation from Sig to QSig is a mapping 𝜂 such that (1) each sort 𝑠 ∈ 𝑆 is mapped to 𝑠𝑞 = 𝜂 (𝑠); (2) each constant symbol 𝑐 :→ 𝑠 is mapped to a quantum state symbol |𝜓𝑐 ⟩ = 𝜂 (𝑐) of sort 𝑠𝑞 . We additionally require 𝜂 (0𝑠 ) = |0𝑠𝑞 ⟩; and (3) each nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠 is mapped to a triple of quantum gate symbols (𝑈𝑂 , pre𝑂 , post𝑂 ) = 𝜂 (𝑂), where sort (𝑈𝑂 ) = sort (pre𝑂 ) = sort (post𝑂 ) ∈ 𝑆𝑞+ is a string of sorts in one of the following forms: • (in-place) 𝑠 1𝑞 , . . . , 𝑠𝑛𝑞 , 𝑠𝑎 for some 𝑠𝑎 ∈ 𝑆𝑞∗ , with 𝑠𝑞 = 𝑠𝑖𝑞 for some 𝑖; • (out-of-place) 𝑠 1𝑞 , . . . , 𝑠𝑛𝑞 , 𝑠𝑞 , 𝑠𝑎 for some 𝑠𝑎 ∈ 𝑆𝑞∗ . (4) In the above, the mappings 𝑠 ↦→ 𝑠𝑞 , 𝑐 ↦→ |𝜓𝑐 ⟩, and 𝑂 ↦→ 𝑈𝑂 are injective. We need to carefully explain the above condition (3). For a nonconstant operation 𝑂, it is natural to expect its quantisation lifts its behaviour on classical data to the quantum setting. However, there

Quantisation of Abstract Data Types

11

are multiple ways to represent classical data as quantum data, e.g., encoding into computationalbasis quantum states, encoding into relative phases, encoding into quantum amplitudes. Concrete examples can be found in Sections 4.1, 4.2, 5 and 6. Therefore, the quantum gate symbols pre𝑂 and post𝑂 in 𝜂 (𝑂) serve for the representation of classical data in the quantum world, while 𝑈𝑂 serves for the lifted 𝑂 in the quantum world. In particular, the quantum gate symbol pre𝑂 (resp. post𝑂 ) corresponds to how classical data is preprocessed into (resp. postprocessed from) quantum data. Then, 𝑈𝑂 corresponds to the quantisation of 𝑂 that has quantum input and output. Their concrete interpretations in an algebra is given later. The injectivity of 𝑂 ↦→ 𝑈𝑂 in condition (4) means 𝑈𝑂 is unique for each 𝑂, but pre𝑂 and post𝑂 can be the same for different 𝑂. For convenience, if an operation symbol 𝑂 is quantised in the in-place form, we assume the index 𝑖 for 𝑠𝑞 = 𝑠𝑖𝑞 is implicitly fixed and used consistently in the other quantisation notions. The string 𝑠𝑎 of sorts represents ancilla sorts needed for the quantised operation. Next, we consider how an algebra can be quantised along the quantisation of the signature. Definition 4.2 (Quantisation of algebra). Let 𝜂 be a quantisation from Sig to QSig. Then a quantum algebra A of signature QSig is a quantisation of an algebra 𝐴 of signature Sig along 𝜂 if: (1) for each sort 𝑠 ∈ 𝑆, {|𝑎⟩ | 𝑎 ∈ 𝐴𝑠 } forms an orthonormal basis of H𝑠A ; 𝑞 (2) for each constant symbol 𝑐 :→ 𝑠, |𝜓𝑐 ⟩ A = |𝑐 𝐴 ⟩. In particular, |0𝑠𝑞 ⟩ A = |0𝑠𝐴 ⟩; and (3) for each nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠, and for all 𝑎 1 ∈ 𝐴𝑠1 , . . . , 𝑎𝑛 ∈ 𝐴𝑠𝑛 , we have:   2 ⟨𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 )| post𝑂A 𝑈𝑂A pre𝑂A |𝑎 1 ⟩ · · · |𝑎𝑛 ⟩ |0⟩ = 1. (5) Here, the subsystems involved in quantum states and gates are implicitly assumed to be ordered according to sort (𝑈𝑂 ). In particular, A , where 𝑖 is the fixed • (in-place) |0⟩ denotes |0𝑠𝑎 ⟩ , and |𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 )⟩ is a state in H𝑠A 𝑖𝑞 index in Definition 4.1; and A • (out-of-place) |0⟩ denotes |0𝑠𝑞 ,𝑠𝑎 ⟩ , and |𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 )⟩ is a state in H𝑠A . 𝑞 Intuitively, in Equation (5), pre𝑂A converts a computational-basis input (the default quantum representation of classical data) into a quantum input for 𝑈𝑂A , and post𝑂A converts the quantum output of 𝑈𝑂A into a computational-basis output. The condition in Equation (5) says that, under the preprocessing pre𝑂A and postprocessing post𝑂A , the behaviour of 𝑈𝑂A agrees with 𝑂 𝐴 on all classical inputs (with probability 1), so 𝑈𝑂A quantises 𝑂 𝐴 . In Sections 4.1, 4.2, 5 and 6, we will present illustrative examples, where the utility of the preprocessing pre𝑂 and postprocessing post𝑂 becomes more concrete. It remains to consider how a classical specification can be quantised. To this end, we need to introduce a quantisation of classical terms. Definition 4.3 (Quantisation of terms). Let 𝜂 be a quantisation from Sig to QSig. Suppose QSig contains a quantum gate symbol SUM 𝑠 : 𝑠𝑞 , 𝑠𝑞 for each sort 𝑠 in Sig, where 𝑠𝑞 = 𝜂 (𝑠). Let 𝑡 be a term in Sig. For each variable 𝑥 : 𝑠 occurring in 𝑡, designate a distinct quantum variable 𝑞𝑥 : 𝑠𝑞 . The quantisation 𝜂 (𝑡) is defined recursively as follows: (1) If 𝑡 = 𝑐 :→ 𝑠 is a constant symbol, choose a fresh variable 𝑝 : 𝑠𝑞 as the principal variable and define 𝜂 (𝑡) = |𝜓𝑐 ⟩𝑝 , where |𝜓𝑐 ⟩ = 𝜂 (𝑐); (2) If 𝑡 = 𝑥 is a variable of sort 𝑠, choose a fresh variable 𝑞 : 𝑠𝑞 as the principal variable and define 𝜂 (𝑡) = SUM 𝑠 [𝑞𝑥 , 𝑞] |0⟩𝑞 ; and (3) Suppose 𝑡 = 𝑂 (𝑡 1, . . . , 𝑡𝑛 ) is a term of sort 𝑠 and 𝜂 (𝑡𝑖 ) = 𝐶𝑖 |𝜓𝑖 ⟩ for 𝑖 = 1, ..., 𝑛, where each 𝜂 (𝑡 𝑗 ) has principal variable 𝑝 𝑗 of sort 𝑠 𝑗𝑞 . Let 𝑝 = 𝑝 1, . . . , 𝑝𝑛 . By renaming variables

12

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

if necessary, assume that, apart from the designated 𝑞𝑥 , all other quantum variables in 𝜂 (𝑡 1 ), . . . , 𝜂 (𝑡𝑛 ) are distinct. We define 𝜂 (𝑡) = 𝐶 1 ; . . . ; 𝐶𝑛 ; pre𝑂 [𝑝, 𝑟 ]; 𝑈𝑂 [𝑝, 𝑟 ]; post𝑂 [𝑝, 𝑟 ] |𝜓 1 ⟩ . . . |𝜓𝑛 ⟩ |0⟩𝑟 . Here 𝑟 is a sequence of fresh variables such that • (in-place) sort (𝑟 ) = 𝑠𝑎 and 𝑝𝑖 is chosen to be the principal variable, where 𝑖 is the fixed index in Definition 4.1; • (out-of-place) sort (𝑟 ) = 𝑠𝑞 , 𝑠𝑎 and 𝑟 = 𝑟 0, 𝑟 𝑎 , where 𝑟 0 is chosen to be the principal variable. In Definition 4.3, note that the same 𝑞𝑥 is used for every occurrence of variable 𝑥 in 𝑡. In clause (2) of this definition, the design 𝜂 (𝑡) = SUM 𝑠 [𝑞𝑥 , 𝑞] |0⟩𝑞 is subtle and needs to be carefully explained. Intuitively, if the gate symbol SUM is interpreted properly in an algebra, SUM 𝑠 [𝑞𝑥 , 𝑞] |0⟩𝑞 copies the computational-basis state of quantum variable 𝑞𝑥 to 𝑞, which is initialised in state |0⟩𝑞 . It has two purposes. First, copying in the computational basis reversibly handles the multiple occurrences of variable 𝑥 in term 𝑡, where 𝑞𝑥 is used to store the input of 𝑥 and each fresh 𝑞 corresponds to a single occurrence of 𝑥. Second, since 𝑞𝑥 are not chosen to be principal variables, tracing out 𝑞𝑥 at the end “dephases” each corresponding 𝑞 in the computational basis. This is important for the correctness of Theorem 4.5, when we transition from a classical equation with a universal quantifier (∀𝑥) over classical inputs to a quantum equation with quantifier (∀𝑞) over quantum inputs. With quantisations of classical terms, we can further define quantisations of equations in a classical specification. Definition 4.4 (Quantisation of equations). Let 𝜂 be a quantisation from Sig to QSig, and let 𝑒 = (∀𝑥 : 𝑠) (𝑡 1 = 𝑡 2 ) be a classical equation, where 𝑥 = 𝑥 1, . . . , 𝑥𝑛 is a string of all variables occurring in 𝑡 1 or 𝑡 2 . We assume that the designated variables 𝑞 = 𝑞𝑥 1 , . . . , 𝑞𝑥𝑛 (see Definition 4.3) in 𝑡 1 and 𝑡 2 are aligned, and 𝜂 (𝑡 1 ) and 𝜂 (𝑡 2 ) have the same principal variable, say 𝑝. Then, the quantisation 𝜂 (𝑒) of 𝑒 along 𝜂 is defined as follows: 𝜂 (𝑒) = (∀𝑞 : 𝑠𝑞 ) (𝜂 (𝑡 1 ) = 𝜂 (𝑡 2 )) ⇓ 𝑝, where 𝑠𝑞 is the quantisation of 𝑠. With the above preparation, we are able to present the main result of this section, which describes a way of deriving a specification of a quantised ADT by lifting from the classical specification. To describe this lifting, for 𝑎, 𝑏 ∈ 𝐴𝑠 , we define   𝑎 ⊞𝑠𝐴 𝑏 = (𝑘𝑠𝐴 ) −1 𝑘𝑠𝐴 (𝑎) + 𝑘𝑠𝐴 (𝑏) mod |𝐴𝑠 | (6) where 𝑘𝑠𝐴 is given in equation (4). Intuitively, the operator ⊞𝑠𝐴 naturally extends the binary XOR ⊕ operator up to the bijection 𝑘𝑠𝐴 . In particular, in Equation (6), the inputs 𝑎, 𝑏 are mapped to the integer domain Z |𝐴𝑠 | , added in Z |𝐴𝑠 | , and then mapped back to the domain 𝐴𝑠 . It is easy to verify that 𝑎 ⊞𝑠𝐴 0𝑠𝐴 = 0𝑠𝐴 ⊞𝑠𝐴 𝑎 = 𝑎 for any 𝑎. When the algebra 𝐴 is clear, we simply write 𝑘𝑠 and ⊞𝑠 for 𝑘𝑠𝐴 and ⊞𝑠𝐴 , respectively. Theorem 4.5 (Lifting of specification). Let Spec = (Sig, 𝐸) be a classical specification, and let 𝜂 be a quantisation from Sig to QSig. Suppose QSig contains a quantum gate symbol SUM 𝑠 : 𝑠𝑞 , 𝑠𝑞 for each sort 𝑠 in Sig, where 𝑠𝑞 = 𝜂 (𝑠). We define QSpec = (QSig, 𝜂 (𝐸)), where 𝜂 (𝐸) = {𝜂 (𝑒) | equation 𝑒 ∈ 𝐸}. If (1) 𝐴 is an algebra of Spec; and

Quantisation of Abstract Data Types

13

(2) A is a quantisation of 𝐴 along 𝜂 and SUM 𝑠A : |𝑎⟩ |𝑏⟩ ↦→ |𝑎⟩ |𝑎 ⊞𝑠 𝑏⟩ for any sort 𝑠 and any 𝑎, 𝑏 ∈ 𝐴𝑠 , then A is a quantum algebra of QSpec. Here, corresponding to the discussion below Definition 4.3, the unitary operator SUM 𝑠A : |𝑎⟩ |𝑏⟩ ↦→ |𝑎⟩ |𝑎 ⊞𝑠 𝑏⟩ is a canonical way to realise the copying in the computational basis when 𝑏 = 0. The proof of Theorem 4.5 is deferred to Appendix A. The above definitions of quantisation are general. In the following subsections, we examine two specific quantisation methods that appear commonly in quantum algorithm design. 4.1

Bit Oracle Quantisation

The first quantisation method is bit oracle quantisation (BO-quantisation for short). The BOquantisation of a classical algebra is defined as follows. Definition 4.6 (BO-quantisation). Let 𝜂 be a quantisation from Sig to QSig and 𝐴 be a Sig-algebra. Then, a quantisation A of 𝐴 along 𝜂 is a BO-quantisation if for each nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠: (1) 𝑈𝑂 is out-of-place with 𝑠𝑎 = ∅; (2) pre𝑂A = post𝑂A = 1sort (𝑈𝑂 ) ; and (3) for any 𝑎 1 ∈ 𝐴𝑠1 , . . . , 𝑎𝑛 ∈ 𝐴𝑠𝑛 , 𝑎 ∈ 𝐴𝑠 , 𝑈𝑂A (|𝑎 1 ⟩ · · · |𝑎𝑛 ⟩ |𝑎⟩) = |𝑎 1 ⟩ · · · |𝑎𝑛 ⟩ |𝑎 ⊞𝑠 𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 )⟩ .

(7)

It is easy to check that 𝑈𝑂A defined in equation (7) indeed satisfies the condition (5). When QSig includes the gate symbol SUM 𝑠 for each sort 𝑠, the BO-quantisation of terms and equations can be naturally induced by Definition 4.6, according to Definitions 4.1 and 4.4. Definition 4.6 naturally yields the common bit oracle in quantum algorithms as follows, where the designated 𝑘 bit is the identity and ⊞bit reduces to XOR. Example 4.7. Consider the following • Signature Sig = (𝑆, OP) with 𝑆 = {bit} and OP = {0bit, 𝑓 }, where 0bit :→ bit and 𝑓 : bit, . . . , bit → bit. | {z } 𝑛

• Algebra 𝐴 of signature Sig with 𝐴bit = {0, 1} and 0𝐴bit = 0, where 𝑓 𝐴 : {0, 1}𝑛 → {0, 1} is a 𝑛-ary Boolean function. Then the following gives a BO-quantisation of 𝐴: n o  • Signature QSig = (𝑆𝑞 , K, U) with 𝑆𝑞 = {qbit}, K = |0qbit ⟩ , and U = 𝑈 𝑓 , pre 𝑓 , post 𝑓 , where |0qbit ⟩ : qbit and 𝑈 𝑓 , pre 𝑓 , post 𝑓 : qbit, . . . , qbit. | {z } 𝑛+1 A • Algebra A of signature QSig: Hqbit = C2 , |0qbit ⟩ A = |0⟩, pre 𝑓A = post 𝑓A = 1, and

𝑈 𝑓A |𝑥, 𝑏⟩ = |𝑥, 𝑏 ⊕ 𝑓 𝐴 (𝑥)⟩

(8)

for any 𝑥 ∈ {0, 1}𝑛 and 𝑏 ∈ {0, 1}. In this example, the unitary operator 𝑈 𝑓A is often known as the bit oracle or standard oracle used by a quantum algorithm to query a black-box function 𝑓 . The bit oracle has been employed in the design of many quantum algorithms, e.g., the Deutsch-Jozsa algorithm [7] and the modular exponentiation subroutine of Shor’s algorithm [34]. It should be noted that on the RHS of Equation (8),

14

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

the first 𝑛 qubits are used to record the input 𝑥, and the last qubit is used to store the computational outcome 𝑓 (𝑥). In this way, 𝑈 𝑓 is made invertible and thus a unitary operator. 4.2

Phase Oracle Quantisation

The second quantisation method is phase oracle quantisation (PO-quantisation for short). The PO-quantisation of a classical algebra is defined as follows. Definition 4.8 (PO-quantisation). Let 𝜂 be a quantisation from Sig to QSig and 𝐴 be a Sig-algebra. Then, a quantisation A of 𝐴 along 𝜂 is a PO-quantisation if for each nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠: (1) 𝑈𝑂 is out-of-place with 𝑠𝑎 = ∅. (2) pre𝑂A = 1𝑠1𝑞 ,...,𝑠𝑛𝑞 ⊗ QFT |𝐴𝑠 | and post𝑂A = 1𝑠1𝑞 ,...,𝑠𝑛𝑞 ⊗ QFT †|𝐴𝑠 | , where QFT |𝐴𝑠 | is the quantum Fourier transform on Z |𝐴𝑠 | defined by 1 ∑︁ 𝑘𝑠 (𝑎) ·𝑘𝑠 (𝑏 ) QFT |𝐴𝑠 | |𝑎⟩ = √︁ 𝜔 |𝑏⟩ |𝐴𝑠 | 𝑏 ∈𝐴𝑠 for any 𝑎 ∈ 𝐴𝑠 , where 𝜔 = 𝑒 2𝜋𝑖/|𝐴𝑠 | ; and (3) for any 𝑎 1 ∈ 𝐴𝑠1 , . . . , 𝑎𝑛 ∈ 𝐴𝑠𝑛 , 𝑎 ∈ 𝐴𝑠 , 𝑈𝑂A |𝑎 1, . . . , 𝑎𝑛 ⟩ |𝑎⟩ = 𝜔 𝑘𝑠 (𝑎) ·𝑘𝑠 (𝑂 (𝑎1,...,𝑎𝑛 ) ) |𝑎 1, . . . , 𝑎𝑛 ⟩ |𝑎⟩ . 𝐴

(9)

It is also easy to check that 𝑈𝑂A defined in equation (9) satisfies the condition (5). When QSig includes the gate symbol SUM 𝑠 for each sort 𝑠, the PO-quantisation of terms and equations can be naturally induced by Definition 4.8, according to Definitions 4.1 and 4.4. Definition 4.8 naturally yields the common phase oracle (or more accurately, the controlled version of the common phase oracle) in quantum algorithms, where the designated 𝑘 bit is the identity, 𝜔 = −1 and QFT 2 = 𝐻 is the Hadamard operator. Example 4.9. Consider the same signature Sig and algebra 𝐴 as in Example 4.7. Then, the following gives a PO-quantisation of 𝐴: n o  • Signature QSig = (𝑆𝑞 , K, U): 𝑆𝑞 = {qbit}, K = |0qbit ⟩ , and U = 𝑈 𝑓 , pre 𝑓 , post 𝑓 , where |0qbit ⟩ : qbit and 𝑈 𝑓 , pre 𝑓 , post 𝑓 : qbit, . . . , qbit. | {z } 𝑛+1 A • Algebra A of signature QSig: Hqbit = C2 , |0qbit ⟩ A = |0⟩, pre 𝑓A = post 𝑓A = 1𝑛 ⊗ 𝐻 , and

𝑈 𝑓A |𝑥, 𝑏⟩ = (−1)𝑏 ·𝑓

𝐴 (𝑥 )

|𝑥, 𝑏⟩

for any 𝑥 ∈ {0, 1}𝑛 and 𝑏 ∈ {0, 1}. In this example, 𝑈 𝑓 is often known as the (controlled) phase oracle for a quantum algorithm to query a black-box function 𝑓 . The phase oracle has been applied in Grover’s search [15], amplitude amplification [4], and several other quantum algorithms. 4.3

Phase Kickback Trick

In quantum algorithms, the phase kickback trick provides a useful connection between a bit oracle and a phase oracle, and now we can view it through the lens of ADTs. For example, in the DeutschJozsa algorithm that decides whether a given Boolean function 𝑓 : {0, 1}𝑛 → {0, 1} is constant or balanced, the bit oracle 𝑈 𝑓 is defined by 𝑈 𝑓 |𝑥, 𝑦⟩ = |𝑥, 𝑦 ⊕ 𝑓 (𝑥)⟩

Quantisation of Abstract Data Types

15

for any 𝑥 ∈ {0, 1}𝑛 and 𝑦 ∈ {0, 1}. A key idea in this algorithm is that the target register is initialised in the superposition |−⟩ = √1 (|0⟩ − |1⟩). We observe: 2

𝑈 𝑓 |𝑥, −⟩ = |𝑥⟩ ⊗ (−1) 𝑓 (𝑥 ) |−⟩ = (−1) 𝑓 (𝑥 ) |𝑥⟩ ⊗ |−⟩ .

(10)

In the final expression above, the phase (−1) 𝑓 (𝑥 ) appears in front of the quantum state. On the other hand, if the target register is initialised in |+⟩ = √1 (|0⟩ + |1⟩), then 2

𝑈 𝑓 |𝑥, +⟩ = |𝑥⟩ ⊗ |+⟩ .

(11)

Combining Equations (10) and (11) gives (1𝑛 ⊗ 𝐻 )𝑈 𝑓 (1𝑛 ⊗ 𝐻 ) |𝑥, 𝑏⟩ = (−1)𝑏 ·𝑓 (𝑥 ) |𝑥, 𝑏⟩ .

(12)

More generally, the phase kickback implies a correspondence between BO-quantisation and PO-quantisation. Suppose 𝜂 is a quantisation from Sig to QSig. Let A and B be BO- and POquantisations of the same algebra 𝐴 along 𝜂, respectively. For each sort 𝑠 in Sig, suppose that A and B have the same quantum domain H𝑠A = H𝑠B𝑞 = span{|𝑎⟩ : 𝑎 ∈ 𝐴𝑠 }. 𝑞 Then, analogous to Equation (12), for any operation 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠, we have:     𝑈𝑂B = 1𝑠1𝑞 ,...,𝑠𝑛𝑞 ⊗ QFT |𝐴𝑠 | 𝑈𝑂A 1𝑠1𝑞 ,...,𝑠𝑛𝑞 ⊗ QFT †|𝐴𝑠 | ,

(13)

which is essentially equivalent to post𝑂A 𝑈𝑂A pre𝑂A = post𝑂B𝑈𝑂B pre𝑂B . This means that BO-quantisation and PO-quantisation can be related by changing how classical data are encoded into quantum data through pre𝑂 and post𝑂 . 5

ILLUSTRATIVE APPLICATION I: QUANTUM ARRAYS

Arrays are a fundamental data type widely used in classical programming. To illustrate the framework developed in Sections 3 and 4, we show how quantum arrays can be defined via the quantisation of classical arrays. In particular, this approach offers a new perspective for understanding Quantum Random Access Memories (QRAMs) [10, 11]. 5.1

Classical Arrays

For convenience of the reader, let us recall the basic theory of arrays. First, we describe the signature Sig = (𝑆, OP) of the ADT of arrays. Let I be a set of index sorts and V a set of value sorts, so that 𝑆 = I ∪ V. The value sorts and their dimensions are generated as follows: (1) val ∈ V is a primitive value sort, and dim(val) = 0; (2) if 𝐼 ∈ I and 𝜏 ∈ V, then array(𝐼, 𝜏) ∈ V, and dim(array(𝐼, 𝜏)) = dim(𝜏) + 1. A canonical algebra 𝐴 of Sig gives the following interpretation. For every 𝐼 ∈ I and 𝜏 ∈ V, define 𝐴array(𝐼,𝜏 ) = 𝐴𝐼 → 𝐴𝜏 . Consequently, if 𝜏 = array(𝐼 1, array(𝐼 2, . . . , array(𝐼𝑛 , val) . . .)), then

𝐴𝜏 = 𝐴𝐼1 → 𝐴𝐼2 → · · · → 𝐴𝐼𝑛 → 𝐴val · · · . Equivalently, 𝐴𝜏 = (𝐴𝐼1 × · · · × 𝐴𝐼𝑛 ) → 𝐴val .

16

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

For the operation symbols, let OP contain two classes of symbols: read 𝐼,𝜏 : array(𝐼, 𝜏), 𝐼 → 𝜏 write𝐼,𝜏 : array(𝐼, 𝜏), 𝐼, 𝜏 → array(𝐼, 𝜏)

(14)

where 𝐼 ∈ I and 𝜏 ∈ V. They are also called selector and store operations, respectively. For simplicity, the subscripts 𝐼, 𝜏 of read 𝐼,𝜏 and write𝐼,𝜏 will often be omitted. In the canonical algebra 𝐴, they are interpreted as follows: read 𝐴 𝐼,𝜏 : (𝑎, 𝑗) ↦→ 𝑎[ 𝑗] (15)

′ write𝐴 𝐼,𝜏 : (𝑎, 𝑗, 𝑣) ↦→ 𝑎

for 𝑎 ∈ 𝐴array(𝐼,𝜏 ) , 𝑗 ∈ 𝐴𝐼 , and 𝑣 ∈ 𝐴𝜏 , where 𝑎 ′ [𝑖] = 𝑎[𝑖] if 𝑖 ≠ 𝑗 and 𝑎 ′ [ 𝑗] = 𝑣. Intuitively, read (𝑎, 𝑗) denotes the value stored in array 𝑎 at index 𝑗, and write(𝑎, 𝑗, 𝑣) denotes the array obtained by updating 𝑎 with value 𝑣 stored at index 𝑗. We assume countably many variables and constants of each sort. The terms are constructed from variables and constants using operation symbols, and their sorts are defined in the usual way. A basic theory of arrays was first introduced by McCarthy [27], where the functions read and write are characterised by the following axioms. For every 𝐼 ∈ I and 𝜏 ∈ V: • Axiom 1 (read-over-write): ∀𝑎 : array(𝐼, 𝜏), 𝑖, 𝑗 : 𝐼, 𝑣 : 𝜏 .(𝑖 = 𝑗 → read (write(𝑎, 𝑖, 𝑣), 𝑗) = 𝑣) (𝑖 ≠ 𝑗 → read (write(𝑎, 𝑖, 𝑣), 𝑗) = read (𝑎, 𝑗)) • Axiom 2 (extensionality): ∀𝑎, 𝑏 : array(𝐼, 𝜏).(∀𝑖 : 𝐼 .read (𝑎, 𝑖) = read (𝑏, 𝑖)) → 𝑎 = 𝑏 It should be pointed out that, essentially, the above two axioms do not constitute an equational specification as in Definition 2.6. Instead, they are formulated in a first-order logical language. However, they are easy to understand for our purposes. 5.2

Quantum Arrays

Now let us examine quantum arrays through the lens of the quantisation of the classical ADT of arrays (see Section 4). Suppose QSig = (𝑆𝑞 , K, U) is the quantum signature obtained from a quantisation 𝜂 of the classical signature for arrays. For 𝐼 ∈ I and 𝜏 ∈ V, write 𝐼𝑞 = 𝜂 (𝐼 ),

𝜏𝑞 = 𝜂 (𝜏),

qarray(𝐼𝑞 , 𝜏𝑞 ) = 𝜂 (array(𝐼, 𝜏)).

In particular, write qval = 𝜂 (val). Then 𝑆𝑞 = I𝑞 ∪ V𝑞 ,

I𝑞 = {𝜂 (𝐼 ) : 𝐼 ∈ I},

V𝑞 = {𝜂 (𝜏) : 𝜏 ∈ V}.

Let 𝐴 be the canonical algebra for the signature of classical arrays considered previously. We consider the following quantised algebra A of 𝐴 along 𝜂. We define: A (1) Hqval = span{|𝑣⟩ : 𝑣 ∈ 𝐴val }; (2) for every 𝐼 ∈ I, H𝐼A = span{| 𝑗⟩ : 𝑗 ∈ 𝐴𝐼 }; and 𝑞

(3) for every 𝜏 ∈ V, H𝜏A = span{|𝑡⟩ : 𝑡 ∈ 𝐴𝜏 }. Furthermore, for every 𝐼 ∈ I and 𝜏 ∈ V, 𝑞 Ì  A Hqarray(𝐼 = span |𝑎⟩ : 𝑎 ∈ 𝐴 = H𝜏A , (16) array(𝐼,𝜏 ) 𝑞 𝑞 ,𝜏𝑞 ) 𝑗 ∈𝐴𝐼

Quantisation of Abstract Data Types

17

Ë where we denote |𝑎⟩ = 𝑗 ∈𝐴𝐼 |𝑎[ 𝑗]⟩, and the indices 𝑗 are ordered by keeping the designated 𝑘𝐼 ( 𝑗) increasing (see Section 4). By expanding the RHS of Equation (16) recursively, if 𝜏 = array(𝐼 1, array(𝐼 2, . . . , array(𝐼𝑛 , val) . . .)), then H𝜏A = 𝑞

Ì

A Hqval .

( 𝑗1 ,...,𝑗𝑛 ) ∈𝐴𝐼1 ×···×𝐴𝐼𝑛

Next, we explain how the read and write symbols in OP are quantised to gate symbols in U. As in Section 4, for each 𝐼 ∈ I and 𝜏 ∈ V, we assume that the designated 0 satisfies 0𝐴array(𝐼,𝜏 ) [ 𝑗] = 0𝜏𝐴 for any 𝑗 ∈ 𝐴𝐼 . Let 𝑘𝐼 and 𝑘𝜏 be the designated bijections for 𝐴𝐼 and 𝐴𝜏 , respectively. We recursively choose the designated bijection for the corresponding array sort to be ∑︁ |𝐴𝜏 |𝑘𝐼 ( 𝑗 ) · 𝑘𝜏 (𝑎[ 𝑗]). 𝑘 array(𝐼,𝜏 ) (𝑎) = (17) 𝑗 ∈𝐴𝐼

For the concrete one-dimensional QRAM examples below, fix an index sort idx ∈ I and write qidx = 𝜂 (idx),

array = array(idx, val),

qarray = qarray(qidx, qval).

Quantum read. The operation read 𝐴 𝐼,𝜏 can be quantised in the same way as the BO-quantisation in Definition 4.6: (1) 𝑈 read , preread , and post read have the sort qarray(𝐼𝑞 , 𝜏𝑞 ), 𝐼𝑞 , 𝜏𝑞 . A A (2) preread = post read = 1. A (3) 𝑈 read |𝑎⟩ | 𝑗⟩ |𝑣⟩ = |𝑎⟩ | 𝑗⟩ |𝑣 ⊞𝜏 𝑎[ 𝑗]⟩ for any 𝑎 ∈ 𝐴array(𝐼,𝜏 ) , 𝑗 ∈ 𝐴𝐼 , and 𝑣 ∈ 𝐴𝜏 . We simply use qread to denote the gate 𝑈 read for convenience. What qread A effectively implements is a QRAM read operation. Consider the case when 𝐴idx = Z𝑁 , 𝐴val = Z𝑀 , and their designated bijections are the identity maps. Then, an array 𝑎 of sort array stores 𝑁 classical values 𝑎[0], 𝑎[1], . . . , 𝑎[𝑁 − 1] from 𝐴val at addresses 0, 1, . . . , 𝑁 − 1. In classical computing, RAM (Random Access Memory) allows one to access a memory cell by providing an address. In QRAM (Quantum Random Access Memory), the key idea is that the address itself can be in a quantum superposition. This means one can query many memory locations simultaneously in superposition. A QRAM read implements the following transformation: ∑︁ ∑︁ 𝛽 𝑗 |𝑎[0], . . . , 𝑎[ 𝑗], . . . , 𝑎[𝑁 − 1]⟩ | 𝑗⟩ |0⟩ ↦→ 𝛽 𝑗 |𝑎[0], . . . , 𝑎[ 𝑗], . . . , 𝑎[𝑁 − 1]⟩ | 𝑗⟩ |𝑎[ 𝑗]⟩ , 𝑗

𝑗

(18) which is an instantiation of qread A . So, in one operation, we can “load” data from multiple addresses coherently. Quantum write. The operation write𝐴 𝐼,𝜏 can be quantised in-place as follows: • 𝑈 write , prewrite , and post write have the sort qarray(𝐼𝑞 , 𝜏𝑞 ), 𝐼𝑞 , 𝜏𝑞 . A A • prewrite = post write = 1. A • 𝑈 write |𝑎⟩ | 𝑗⟩ |𝑣⟩ = |𝑎 ′ ⟩ | 𝑗⟩ |𝑎[ 𝑗]⟩ for any 𝑎 ∈ 𝐴array(𝐼,𝜏 ) , 𝑗 ∈ 𝐴𝐼 , and 𝑣 ∈ 𝐴𝜏 , where 𝑎 ′ [𝑖] = 𝑎[𝑖] if 𝑖 ≠ 𝑗 and 𝑎 ′ [ 𝑗] = 𝑣. We simply use qwrite to denote the gate 𝑈 write for convenience. What qwrite A effectively implements is a QRAM swap operation. Again, consider the case when 𝐴idx = Z𝑁 , 𝐴val = Z𝑀 , and their designated bijections are the identity maps. Then, an array 𝑎 of

18

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

sort array stores 𝑁 classical values 𝑎[0], 𝑎[1], . . . , 𝑎[𝑁 − 1] from 𝐴val at addresses 0, 1, . . . , 𝑁 − 1. A QRAM swap implements the following transformation: ∑︁ ∑︁ 𝛽 𝑗 |𝑎[0], . . . , 𝑎[ 𝑗], . . . , 𝑎[𝑁 − 1]⟩ | 𝑗⟩ |𝑣⟩ ↦→ 𝛽 𝑗 |𝑎[0], . . . , 𝑣, . . . , 𝑎[𝑁 − 1]⟩ | 𝑗⟩ |𝑎[ 𝑗]⟩ . (19) 𝑗

𝑗

Therefore, in one operation, qwrite can “write” data to multiple addresses coherently. According to Theorem 4.5, by properly reexpressing Axiom 1 and Axiom 2 using equations we can derive specifications for the ADT of quantum arrays. Beyond that, quantum arrays actually satisfy extra properties. The following proposition shows that quantum array operations qread and qwrite satisfy an equation similar to the first part of the Axiom 1 for classical array operations read and write. This property is specified as a quantum equation (see Definition 3.5). Suppose that for each sort 𝑠 in Sig, SUM 𝑠 : 𝑠𝑞 , 𝑠𝑞 is a gate symbol in QSig and SUM 𝑠A |𝑎⟩ |𝑏⟩ = |𝑎⟩ |𝑎 ⊞𝑠 𝑏⟩ for any 𝑎, 𝑏 ∈ 𝐴𝑠 . Proposition 5.1. The algebra of quantum arrays with gates qread and qwrite satisfies the following specification: ∀𝑞𝑎 : qarray, 𝑞𝑖 : qidx, 𝑞 𝑣 , 𝑞𝑢 : qval (qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ]; qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ]) = (SUM [𝑞𝑢 , 𝑞 𝑣 ]; qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ])

(20)

However, a natural quantum analogue of Axiom 2 is not true. Let us consider the simplest case when 𝐴idx = 𝐴val = Z2 . Even if we restrict attention to the principal variable, the equation (qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ] |Φ⟩ = qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ] |Ψ⟩) ⇓ 𝑞 𝑣 does not imply |Φ⟩ = |Ψ⟩, because the state of a composite quantum system is not uniquely determined by the states of its subsystems, which is indeed one of the fundamental differences between classical and quantum systems. 6

ILLUSTRATIVE APPLICATION II: QUANTUM ERROR CORRECTION

Quantum error correction is fundamental to fault-tolerant quantum computing [13, 22]. To further illustrate the framework developed in Sections 3 and 4, we show how a quantum error-correcting code can be described as a quantisation of a classical error-correcting code. In particular, we first consider the quantisation of a classical 3-bit repetition code and then show how its 9-bit extension gives rise to the Shor code. 6.1

Classical Repetition Code

We first describe a classical repetition code as an ADT. Consider the signature Sig = (𝑆, OP), where 𝑆 = {lbit, pbit, idx, array}, lbit and pbit denote sorts of logical bits and physical bits, respectively. Following Section 5.1, idx is an index sort, and array = array(idx, pbit) is the sort for an array of physical bits. For simplicity, consider the canonical algebra 𝐴 of Sig for the 3-bit repetition code. It gives: 𝐴lbit = 𝐴pbit = {0, 1},

𝐴idx = {0, 1, 2},

𝐴array = 𝐴idx → 𝐴pbit .

Thus, 𝐴array consists of arrays of 3 physical bits indexed by {0, 1, 2}. For the operation symbols, let OP contain the following symbols: enc : lbit → array, flip : array, idx → array, corr : array → array.

Quantisation of Abstract Data Types

19

For 𝑎 = 𝑎[0], 𝑎[1], 𝑎[2] ∈ 𝐴array , define  Í2 maj(𝑎) =

𝑖=0 𝑎[𝑖]



2

to be the majority of 𝑎[0], 𝑎[1], 𝑎[2]. In the canonical algebra 𝐴, the operations are interpreted as enc𝐴 : 𝑥 ↦→ 𝑥, 𝑥, 𝑥 flip𝐴 : (𝑎, 𝑖) ↦→ 𝑎 ′ corr 𝐴 : 𝑎 ↦→ maj(𝑎), maj(𝑎), maj(𝑎), where 𝑎 ′ [ 𝑗] = 𝑎[ 𝑗] if 𝑗 ≠ 𝑖 and 𝑎 ′ [𝑖] = 𝑎[𝑖] ⊕ 1. Intuitively, enc(𝑥) is the code word that encodes 𝑥 by repeating it three times, flip(𝑎, 𝑖) flips the physical bit 𝑎[𝑖] in the array 𝑎, and corr (𝑎) produces a code word by replacing every entry of 𝑎 with maj(𝑎). Then, the algebra 𝐴 satisfies the following equations: ∀𝑥 : lbit. ∀𝑥 : lbit, 𝑖 : idx.

corr (enc(𝑥)) = enc(𝑥), corr (flip(enc(𝑥), 𝑖)) = enc(𝑥).

(21)

The first equation states that corr leaves a code word unchanged. The second equation states that it recovers the code word after a bit flip on any physical bit. 6.2

Quantum Repetition Code

Now let us show the 3-qubit repetition code as a quantisation of the classical 3-bit repetition code. Suppose QSig = (𝑆𝑞 , K, U) is the quantum signature obtained from a quantisation 𝜂 of the classical signature Sig in Section 6.1. Let lqbit = 𝜂 (lbit),

pqbit = 𝜂 (pbit),

qidx = 𝜂 (idx),

qarray = 𝜂 (array).

In addition, let qsyn be an ancilla sort for syndromes. Then 𝑆𝑞 = {lqbit, pqbit, qidx, qarray, qsyn}. Consider a quantum algebra A with A A Hlqbit = Hpqbit = span{|0⟩ , |1⟩}, A Hqarray =

2 Ì

A Hpqbit ,

A Hqidx = span{|0⟩ , |1⟩ , |2⟩}, A Hqsyn = span{|0⟩ , |1⟩ , |2⟩ , |⊥⟩}.

𝑖=0

Here, |⊥⟩ is the designated |0qsyn ⟩, which is a computational-basis state orthogonal to |0⟩ , |1⟩ , |2⟩. As in Section 5, we denote |𝑎⟩ = |𝑎[0], 𝑎[1], 𝑎[2]⟩. In particular, the designated |0qarray ⟩ = |0, 0, 0⟩. We choose the designated functions 𝑘 lbit , 𝑘 pbit , and 𝑘 idx to be identity functions, and define 𝑘 array as in Equation (17). Next, we explain how the operation symbols enc, flip, and corr are quantised to gate symbols in U. Quantum encoding. The operation enc𝐴 can be quantised out-of-place as follows: (1) 𝑈 enc , preenc , and post enc have sort lqbit, qarray. A = post A = 1. (2) preenc enc A |𝑥⟩ |0, 0, 0⟩ = |0⟩ |𝑥, 𝑥, 𝑥⟩ for any 𝑥 ∈ 𝐴 (3) 𝑈 enc lbit .

20

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

We simply use qenc to denote the gate 𝑈 enc for convenience. Compared with the classical enc in Section 6.1, the gate qenc encodes |𝑥⟩ as |𝑥, 𝑥, 𝑥⟩ in the computational basis and resets the logical bit to |0⟩. Note that when the logical qubit is initially in superposition, the physical qubits become entangled. Quantum flip. The operation flip𝐴 can be quantised in-place as follows: (1) 𝑈 flip , preflip , and post flip have sort qarray, qidx. A A (2) preflip = post flip = 1. A (3) 𝑈 flip |𝑎⟩ |𝑖⟩ = |flip𝐴 (𝑎, 𝑖)⟩ |𝑖⟩ for any 𝑎 ∈ 𝐴array and 𝑖 ∈ 𝐴idx .

As usual, we simply use qflip to denote the gate 𝑈 flip for convenience. Note that qflip implements the classical operation flip in the computational basis. It leaves the index unchanged and applies a Pauli 𝑋 gate to the physical qubit indexed by 𝑖. Quantum correction. The operation corr 𝐴 can be quantised in-place as follows: (1) 𝑈 corr , precorr , and post corr have sort qarray, qsyn. A = post A = 1. (2) precorr corr A (3) 𝑈 corr |𝑎⟩ |⊥⟩ = |corr 𝐴 (𝑎)⟩ |syn(𝑎)⟩ for any 𝑎 ∈ 𝐴array , where ( ⊥, 𝑎 = corr 𝐴 (𝑎), syn(𝑎) = 𝑗, 𝑗 is the unique index such that 𝑎[ 𝑗] ≠ maj(𝑎).

(22)

As usual, we simply use qcorr to denote the gate 𝑈 corr for convenience. Intuitively, qcorr implements the classical corr in the computational basis and produces the syndrome syn(𝑎). In the computational basis, when 𝑎 is a code word, the syndrome is ⊥; otherwise, it is the index of the unique physical bit that differs from maj(𝑎), which is the error location when 𝑎 is obtained from a bit-flip on a code word. Note that qcorr coherently performs the syndrome extraction and error correction together. According to Theorem 4.5, the equations in Equation (21) can be lifted to a specification of the quantum repetition code. Here, we give a direct specification that the quantum repetition code corrects a single Pauli 𝑋 error. Proposition 6.1. The quantum algebra A with gates qenc, qflip, and qcorr satisfies the following specification:   ∀𝑞𝑙 : lqbit. qenc[𝑞𝑙 , 𝑞𝑎 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 = qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 ⇓ 𝑞𝑎 , (23)  ∀𝑞𝑙 : lqbit, 𝑞𝑖 : qidx. qenc[𝑞𝑙 , 𝑞𝑎 ]; qflip[𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠  (24) = qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 ⇓ 𝑞𝑎 . The first equation states that qcorr leaves a quantum code word unchanged. The second equation states that it recovers the quantum code word after qflip introduces a Pauli 𝑋 error on any physical qubit. In both equations, 𝑞𝑎 is the only principal variable. 6.3

Shor Code

The 3-qubit quantum repetition code in Section 6.2 can only correct a Pauli 𝑋 error. Inspired by the repetition code, the Shor code [33] is the first quantum error-correcting code that can correct an arbitrary single-qubit error. Let us examine the 9-qubit Shor code as a quantisation of a 9-bit repetition code. We reuse the classical signature Sig in Section 6.1 with slight modifications: the

Quantisation of Abstract Data Types

21

operation symbol flip in Section 6.1 is replaced by two operation symbols flipX, flipZ : array, idx → array of the same sort. Consider the canonical algebra 𝐵 for a 9-bit repetition code. It gives 𝐵 lbit = 𝐵 pbit = {0, 1},

𝐵 idx = {0, 1, . . . , 8},

For 𝑎 ∈ 𝐵 array and 𝑟 ∈ {0, 1, 2}, we define   Í2 𝑡 =0 𝑎[3𝑟 + 𝑡] , 𝑚(𝑎) [𝑟 ] = 2

𝐵 array = 𝐵 idx → 𝐵 pbit .  Í2

𝑟 =0 𝑚(𝑎) [𝑟 ]

maj(𝑎) =

 .

2

Intuitively, the 9 physical bits of 𝑎 are split into three groups, where the 𝑟 th group consists of 𝑎[3𝑟 ], 𝑎[3𝑟 + 1], 𝑎[3𝑟 + 2]. The value 𝑚(𝑎) [𝑟 ] is the majority of the 𝑟 th group, while maj(𝑎) is the majority of 𝑚(𝑎) [0], 𝑚(𝑎) [1], 𝑚(𝑎) [2]. In the algebra 𝐵, the operations are interpreted as enc𝐵 (𝑥) [𝑖] = 𝑥, ( 𝑎[ 𝑗] ⊕ 1, flipX 𝐵 (𝑎, 𝑖) [ 𝑗] = flipZ 𝐵 (𝑎, 𝑖) [ 𝑗] = 𝑎[ 𝑗],

𝑗 = 𝑖, , 𝑗 ≠ 𝑖,

corr 𝐵 (𝑎) [𝑖] = maj(𝑎), where 𝑥 ∈ 𝐵 lbit , 𝑎 ∈ 𝐵 array , and 𝑖, 𝑗 ∈ 𝐵 idx . Here, although both flipX and flipZ are interpreted as a bit flip error in algebra 𝐵, their quantisations will correspond to different quantum errors later. Similar to the algebra 𝐴 for the 3-bit repetition code (see Section 6.1), the algebra 𝐵 satisfies ∀𝑥 : lbit. corr (enc(𝑥)) = enc(𝑥), ∀𝑥 : lbit, 𝑖 : idx.

corr (flipX (enc(𝑥), 𝑖)) = enc(𝑥),

∀𝑥 : lbit, 𝑖 : idx.

corr (flipZ (enc(𝑥), 𝑖)) = enc(𝑥).

(25)

Suppose QSig = (𝑆𝑞 , K, U) is the quantum signature obtained from a quantisation 𝜂 of this signature. Let lqbit = 𝜂 (lbit),

pqbit = 𝜂 (pbit),

qidx = 𝜂 (idx),

qarray = 𝜂 (array).

In addition, let qsyn be an ancilla sort for syndromes, with designated state |0qsyn ⟩ = |⊥, ⊥, ⊥, ⊥⟩. Consider a quantum algebra B with B B Hlqbit = Hpqbit = span{|0⟩ , |1⟩}, B Hqarray =

8 Ì

B Hpqbit ,

B Hqidx = span{|0⟩ , |1⟩ , . . . , |8⟩},

 B Hqsyn = span |𝑠⟩ : 𝑠 ∈ {0, 1, 2, ⊥}4 .

𝑖=0

As usual, we denote |𝑎⟩ = |𝑎[0], . . . , 𝑎[8]⟩. In particular, the designated state |0qarray ⟩ = |0⟩ ⊗9 . For a single-qubit unitary operator 𝑈 , let 𝑈𝑖 = 1⊗𝑖 ⊗ 𝑈 ⊗ 1⊗ (8−𝑖 ) , which applies 𝑈 on the qubit indexed by 𝑖. The designated functions 𝑘 lbit , 𝑘 pbit , 𝑘 idx , and 𝑘 array are chosen as in Section 6.2. Next, we explain how the operation symbols enc, flipX , flipZ, and corr are quantised to gate symbols in U. Quantum encoding. For 𝑥 ∈ {0, 1}, let  |Ψ𝑥 ⟩ =

|000⟩ + (−1)𝑥 |111⟩ √ 2

 ⊗3

The operation enc𝐵 can be quantised out-of-place as follows: (1) 𝑈 enc , preenc , and post enc have sort lqbit, qarray.

.

(26)

22

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

B = 1, and post B |0⟩ |Ψ ⟩ = |0⟩ |enc 𝐵 (𝑥)⟩ for any 𝑥 ∈ 𝐵 (2) preenc 𝑥 lbit . enc B (3) 𝑈 enc |𝑥⟩ |0⟩ ⊗9 = |0⟩ |Ψ𝑥 ⟩ for any 𝑥 ∈ 𝐵 lbit . We simply use qenc to denote the gate 𝑈 enc for convenience. Compared with Section 6.2, the gate qenc here encodes the computational-basis |𝑥⟩ into a Shor code word |Ψ𝑥 ⟩. If the logical qubit is initially in superposition, the physical qubits are in the corresponding superposition of |Ψ0 ⟩ and |Ψ1 ⟩.

Quantum flip. The operations flipX 𝐵 and flipZ 𝐵 can be quantised in-place as follows: (1) 𝑈 flipX , 𝑈 flipZ , preflipX , preflipZ , post flipX , and post flipZ have sort qarray, qidx. Î8 B B B B (2) preflipX = post flipX = 1 and preflipZ = post flipZ = ( 𝑖=0 𝐻𝑖 ) ⊗ 1, Í8 Í8 B B (3) 𝑈 flipX = 𝑖=0 𝑋𝑖 ⊗ |𝑖⟩⟨𝑖 | and 𝑈 flipZ = 𝑖=0 𝑍𝑖 ⊗ |𝑖⟩⟨𝑖 |. We simply use qflipX and qflipZ to denote the gates 𝑈 flipX and 𝑈 flipZ , respectively, for convenience. The gates qflipX and qflipZ leave the index |𝑖⟩ unchanged and apply Pauli 𝑋 and 𝑍 gates, respectively, on the physical qubit indexed by 𝑖. Thus, they introduce the corresponding Pauli errors. Quantum correction. For 𝑎 ∈ 𝐵 array , we define syn(𝑎) ∈ {0, 1, 2, ⊥}4 as follows. For 𝑟 ∈ {0, 1, 2}, ( ⊥, 𝑎[3𝑟 + 𝑡] = 𝑚(𝑎) [𝑟 ] for every 𝑡 ∈ {0, 1, 2}, syn(𝑎) [𝑟 ] = 𝑡, 𝑡 is the unique index such that 𝑎[3𝑟 + 𝑡] ≠ 𝑚(𝑎) [𝑟 ]. Further, we define ( syn(𝑎) [3] =

⊥, 𝑚(𝑎) [𝑟 ] = maj(𝑎) for every 𝑟 ∈ {0, 1, 2}, 𝑟, 𝑟 is the unique index such that 𝑚(𝑎) [𝑟 ] ≠ maj(𝑎).

Intuitively, syn(𝑎) is the syndrome produced for an arbitrary 𝑎. For each 𝑟 ∈ {0, 1, 2}, if there is an entry in the 𝑟 th group of 𝑎 that differs from 𝑚(𝑎) [𝑟 ], then syn(𝑎) [𝑟 ] records the index of this entry; otherwise, it records ⊥. Similarly, if an entry 𝑚(𝑎) [𝑟 ] differs from maj(𝑎), then syn(𝑎) [3] records the index 𝑟 ; otherwise, it records ⊥. Consequently, it is easy to check that 𝑎 ↦→ (maj(𝑎), syn(𝑎)) is a bijection. For 𝑃 ∈ {1, 𝑋, 𝑌 , 𝑍 }, 𝑖 = 3𝑟 + 𝑡, and 𝑘 ∈ {0, 1, 2, 3}, where 𝑟, 𝑡 ∈ {0, 1, 2}, let us define 𝜎 (𝑃, 𝑖) ∈ {0, 1, 2, ⊥}4 by   𝑡, 𝑘 = 𝑟 and 𝑃 ∈ {𝑋, 𝑌 },    𝜎 (𝑃, 𝑖) [𝑘] = 𝑟, 𝑘 = 3 and 𝑃 ∈ {𝑍, 𝑌 }, (27)    ⊥, 𝑜.𝑤 .  Intuitively, 𝜎 (𝑃, 𝑖) is the syndrome needed to correct the Pauli error 𝑃𝑖 . Suppose we start with a Shor code word. A Pauli 𝑋 error changes one physical qubit, so its syndrome records the information about 𝑖 = 3𝑟 + 𝑡. A Pauli 𝑍 error on any of the three physical qubits in the same group 𝑟 has the same effect, so its syndrome only records the 𝑟 . A Pauli 𝑌 error combines 𝑋 and 𝑍 , so its syndrome contains both kinds of information. B Let {|Φ𝑥,𝑠 ⟩ : 𝑥 ∈ {0, 1}, 𝑠 ∈ {0, 1, 2, ⊥}4 } be an orthonormal basis of Hqarray such that |Φ𝑥,𝜎 (𝑃,𝑖 ) ⟩ = 𝑃𝑖 |Ψ𝑥 ⟩

(28)

for 𝑥 ∈ 𝐵 lbit , 𝑃 ∈ {1, 𝑋, 𝑌 , 𝑍 }, and 𝑖 ∈ 𝐵 idx . The existence of such a basis is proved in Lemma A.2. Here, in |Φ𝑥,𝑠 ⟩, 𝑥 records the logical bit and 𝑠 records the syndrome. The operation corr 𝐵 can be quantised in-place as follows: (1) 𝑈 corr , precorr , and post corr have sort qarray, qsyn.

Quantisation of Abstract Data Types

23

B |𝑎⟩ |⊥, ⊥, ⊥, ⊥⟩ = |Φ B 𝐵 (2) precorr maj (𝑎),syn(𝑎) ⟩ |⊥, ⊥, ⊥, ⊥⟩ and post corr |Ψ𝑥 ⟩ |𝑠⟩ = |enc (𝑥)⟩ |𝑠⟩ for 4 every 𝑥 ∈ 𝐵 lbit , 𝑎 ∈ 𝐵 array , and 𝑠 ∈ {0, 1, 2, ⊥} . 4 B |Φ ⟩ |⊥, ⊥, ⊥, ⊥⟩ = |Ψ ⟩ |𝑠⟩ for every 𝑥 ∈ 𝐵 (3) 𝑈 corr 𝑥,𝑠 𝑥 lbit and 𝑠 ∈ {0, 1, 2, ⊥} . We simply use qcorr to denote the gate 𝑈 corr for convenience. Intuitively, precorr implements the bijection 𝑎 ↦→ (maj(𝑎), syn(𝑎)) by mapping |𝑎⟩ to |Φmaj (𝑎),syn(𝑎) ⟩, while leaving the initial syndrome in 𝑞𝑠 unchanged. The quantum gate qcorr maps |Φ𝑥,𝑠 ⟩ to the corrected Shor code word |Ψ𝑥 ⟩ and records the syndrome in 𝑞𝑠 . Finally, post corr maps |Ψ𝑥 ⟩ to the computational-basis repetition code word |enc𝐵 (𝑥)⟩. As in Section 5, we can derive specifications for the Shor code by lifting Equation (21) using Theorem 4.5. Beyond that, the Shor code actually satisfies stronger error-correction properties. The following equations specify that the Shor code corrects a single Pauli 𝑋 , 𝑍 , or 𝑌 error.

Proposition 6.2. The quantum algebra B with gates qenc, qflipX , qflipZ, and qcorr satisfies the following specification:  ∀𝑞𝑙 : lqbit. qenc[𝑞𝑙 , 𝑞𝑎 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠  (29) = qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ⇓ 𝑞𝑎 ,  ∀𝑞𝑙 : lqbit, 𝑞𝑖 : qidx. qenc[𝑞𝑙 , 𝑞𝑎 ]; qflipX [𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠  (30) = qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ⇓ 𝑞𝑎 ,  ∀𝑞𝑙 : lqbit, 𝑞𝑖 : qidx. qenc[𝑞𝑙 , 𝑞𝑎 ]; qflipZ [𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠  (31) = qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ⇓ 𝑞𝑎 ,  ∀𝑞𝑙 : lqbit, 𝑞𝑖 : qidx. qenc[𝑞𝑙 , 𝑞𝑎 ]; qflipX [𝑞𝑎 , 𝑞𝑖 ]; qflipZ [𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠  = qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ⇓ 𝑞𝑎 . (32) The first equation states that qcorr leaves an error-free Shor code word unchanged. The second and third equations state that qcorr recovers the code word after a Pauli 𝑋 or 𝑍 error, respectively. The fourth equation covers a Pauli 𝑌 error through sequential application of qflipX and qflipZ. In all equations, 𝑞𝑎 is the only principal variable. Following the standard quantum error-correction argument, being able to correct Pauli 𝑋, 𝑌 , 𝑍 errors means that the Shor code corrects an arbitrary single-qubit error. 7

EMBEDDINGS OF QUANTUM DATA TYPES

So far, we have only considered the quantisation of individual ADTs. In classical computing, various relationships between different ADTs have been exploited for practical applications in software engineering. In particular, an embedding allows values of one ADT to be represented as values of another while preserving the relevant operations and semantics. Consequently, embeddings between ADTs can be used for applications such as data refinement and software component reuse. To enable these kinds of applications for quantum ADTs, in this section we ask under what conditions quantisation preserves structural relationships between algebras. In classical universal algebra, an embedding faithfully maps one algebra into another while preserving all operations. This section investigates when such an embedding lifts to an embedding between the corresponding quantum algebras.

24

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

Definition 7.1 (Homomorphisms of algebras). Let 𝐴 and 𝐴′ be two algebras of signature Sig = (𝑆, OP). Then: (1) A homomorphism from 𝐴 to 𝐴′ is a family 𝑔 = (𝑔𝑠 )𝑠 ∈𝑆 of mappings 𝑔𝑠 : 𝐴𝑠 → 𝐴𝑠′ such that for each operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠, and for all 𝑎 1 ∈ 𝐴𝑠1 , . . . , 𝑎𝑛 ∈ 𝐴𝑠𝑛 , it holds that ′

𝑔𝑠 (𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 )) = 𝑂 𝐴 (𝑔𝑠1 (𝑎 1 ), . . . , 𝑔𝑠𝑛 (𝑎𝑛 )). Equivalently, the following diagram commutes: 𝑂𝐴

𝐴𝑠1 × · · · × 𝐴𝑠𝑛

𝐴𝑠

𝑔𝑠1 ×···×𝑔𝑠𝑛

𝑔𝑠

𝐴𝑠′ 1 × · · · × 𝐴𝑠′𝑛

𝑂𝐴

𝐴𝑠′

′

(2) If all 𝑔𝑠 are injective, then 𝑔 is called an embedding. (3) If all 𝑔𝑠 are bijective, then 𝑔 is called an isomorphism. Let H and H ′ be two Hilbert spaces. A linear operator 𝑇 : H → H ′ is called an isometric embedding if ⟨𝑇 (𝑥)|𝑇 (𝑦)⟩ H ′ = ⟨𝑥 |𝑦⟩ H for all 𝑥, 𝑦 ∈ H , where ⟨·|·⟩ H , ⟨·|·⟩ H ′ denote the inner products in H and H ′ , respectively. It is easy to see that 𝑇 is injective and norm-preserving: ∥𝑇 (𝑥) ∥ H ′ = ∥𝑥 ∥ H for every 𝑥 ∈ H , and the image 𝑇 (H ) is a closed subspace of H ′ . Definition 7.2 (Embeddings between quantum algebras). Let A and A ′ be two quantum algebras of signature Sig𝑞 = (𝑆𝑞 , K, U). Then an embedding from A to A ′ is a family 𝐺 = (𝐺𝑠 )𝑠 ∈𝑆𝑞 of isometric embeddings 𝐺𝑠 : H𝑠 → H𝑠′ such that (1) for each quantum state symbol |𝜓 ⟩ ∈ K of sort 𝑠 1, . . . , 𝑠𝑛 , it holds that ′

(𝐺𝑠1 ⊗ · · · ⊗ 𝐺𝑠𝑛 ) (|𝜓 ⟩ A ) = |𝜓 ⟩ A ; (2) for each quantum gate symbol 𝑈 ∈ U of sort 𝑠 1, . . . , 𝑠𝑛 , and for any |𝜑⟩ ∈

(33) Ë𝑛

𝑖=1 H𝑠𝑖 ,

′

(𝐺𝑠1 ⊗ · · · ⊗ 𝐺𝑠𝑛 ) (𝑈 A |𝜑⟩) = 𝑈 A ((𝐺𝑠1 ⊗ · · · ⊗ 𝐺𝑠𝑛 ) |𝜑⟩). Equivalently, the following diagram commutes: 𝑛 Ì

H𝑠𝑖

𝑈A

𝑖=1

𝑛 Ì

𝐺𝑠1 ⊗···⊗𝐺𝑠𝑛 𝑛 Ì 𝑖=1

H𝑠𝑖

𝑖=1 𝐺𝑠1 ⊗···⊗𝐺𝑠𝑛

H𝑠′𝑖

𝑛 Ì 𝑈A

′

𝑖=1

H𝑠′𝑖

(34)

Quantisation of Abstract Data Types

25

Ë𝑛
△ ′ = Since 𝐺𝑠1 ,Ë . . . , 𝐺𝑠𝑛 are all isometric embeddings, H (𝐺 ⊗ · · · ⊗ 𝐺 ) H is a closed 𝑠 𝑠 𝑠 1 𝑛 𝑖 𝑖=1 Ë𝑛 𝑛 ′ ′ † subspace 𝑖=1 H𝑠𝑖 → H and its inverse (𝐺𝑠 1 ⊗· · ·⊗𝐺𝑠𝑛 ) : Ëof𝑛 𝑖=1 H𝑠𝑖 . Moreover, 𝐺𝑠1 ⊗· · ·⊗𝐺𝑠𝑛 : ′ H → 𝑖=1 H𝑠𝑖 are unitary operators. Thus, the condition in Equation (34) can be rewritten as: ′

𝑈 A = (𝐺𝑠1 ⊗ · · · ⊗ 𝐺𝑠𝑛 ) † ◦ 𝑈 A ◦ (𝐺𝑠1 ⊗ · · · ⊗ 𝐺𝑠𝑛 ) . If all 𝐺𝑠 are unitary operators, then 𝐺 is called an isomorphism. In this case, 𝐺𝑠 (H𝑠 ) = H𝑠′ for Ë𝑛 ′ ′ every 𝑠 ∈ 𝑆𝑞 , and H = 𝑖=1 H𝑠𝑖 . In the remainder of this section, we give conditions under which an embedding of algebras induces an embedding of their quantisations. 7.1

Embeddings of Quantisations

Let 𝐴 and 𝐴′ be two algebras of the same signature Sig = (𝑆, OP), and let 𝑔 = (𝑔𝑠 )𝑠 ∈𝑆 : 𝐴 → 𝐴′ be an embedding. Let 𝜂 be a quantisation from Sig to QSig = (𝑆𝑞 , K, U) that satisfies 𝑆𝑞 = 𝜂 (𝑆). Let A and A ′ be quantisations of 𝐴 and 𝐴′ along 𝜂, respectively. ′ Recall that the quantisation of 𝑠 ∈ 𝑆 is 𝑠𝑞 ∈ 𝑆𝑞 along 𝜂. For each 𝑠 ∈ 𝑆, we define 𝐺𝑠𝑞 : H𝑠A → H𝑠A 𝑞 𝑞 to be the linear operator that satisfies the following condition: 𝐺𝑠𝑞 (|𝑎⟩) = |𝑔𝑠 (𝑎)⟩ for every 𝑎 ∈ 𝐴𝑠 .

(35)

We call 𝐺 = (𝐺𝑠𝑞 )𝑠 ∈𝑆 the quantisation of 𝑔 = (𝑔𝑠 )𝑠 ∈𝑆 along 𝜂. Since each 𝑔𝑠 is injective, {|𝑔𝑠 (𝑎)⟩ : 𝑎 ∈ 𝐴𝑠 } is an orthonormal set, which means each 𝐺𝑠𝑞 is an isometric embedding. If 𝑔 is further an isomorphism, then each 𝐺𝑠𝑞 is a unitary. For concreteness, we consider BO- and PO-quantisations in Section 4. For each 𝑠 ∈ 𝑆, let ′ 𝑘𝑠𝐴 : 𝐴𝑠 → Z |𝐴𝑠 | and 𝑘𝑠𝐴 : 𝐴𝑠′ → Z |𝐴𝑠′ | be the two designated bijections as in Section 4, and let ⊞𝑠𝐴 ′ and ⊞𝑠𝐴 be defined as in Section 4. We first examine when a BO-quantisation can be embedded into another. Proposition 7.3 (Embeddings of BO-qantisations). Suppose that every state symbol in K is introduced by 𝜂, and that every gate symbol in U is introduced by 𝜂. Let A and A ′ be BO-quantisations of 𝐴 and 𝐴′ , respectively, along 𝜂. If for each 𝑠 ∈ 𝑆 and 𝑎, 𝑏 ∈ 𝐴𝑠 , ′

𝑔𝑠 (𝑎 ⊞𝑠𝐴 𝑏) = 𝑔𝑠 (𝑎) ⊞𝑠𝐴 𝑔𝑠 (𝑏), or equivalently, the following diagram commutes: 𝐴𝑠 × 𝐴𝑠

⊞𝑠𝐴

𝑔𝑠 ×𝑔𝑠

𝐴𝑠 𝑔𝑠

𝐴𝑠′ × 𝐴𝑠′

⊞𝑠𝐴

′

𝐴𝑠′

then 𝐺 in Equation (35) is an embedding from A to A ′ . Next, we examine when a PO-quantisation is isomorphic to another. Unlike the BO-quantisations, compatibility with the quantum Fourier transform in Definition 4.8 forces every 𝑔𝑠 to be surjective. Consequently, the corresponding result for PO-quantisations is stated only for isomorphisms. Proposition 7.4 (Isomorphisms of PO-qantisations). Suppose that every state symbol in K is introduced by 𝜂, and that every gate symbol in U is introduced by 𝜂. Suppose 𝑔 is an isomorphism. Let A and A ′ be PO-quantisations of 𝐴 and 𝐴′ , respectively, along 𝜂. If for each 𝑠 ∈ 𝑆, ′

𝑘𝑠𝐴 ◦ 𝑔𝑠 = 𝑘𝑠𝐴 ,

26

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

or equivalently, the following diagram commutes (noting that |𝐴𝑠 | = |𝐴𝑠′ |): 𝑘𝑠𝐴

𝐴𝑠

Z |𝐴𝑠 |

𝑔𝑠

𝐴𝑠′

𝑘𝑠𝐴

′

Z |𝐴𝑠′ |

then 𝐺 in Equation (35) is an isomorphism from A to A ′ . 8

PRODUCTS OF QUANTUM DATA TYPES

Embeddings discussed in the last section describe one of the simplest structural relationships between quantum ADTs. We now turn to how to construct a new quantum ADT from simpler ones. In classical computing, products of ADTs enable us to compose independently specified abstractions while preserving their interfaces and invariants, and they find applications in composite data structures, modular software composition, and other settings. To introduce the same capability into quantum software engineering, in this section we define the notion of the product of ADTs. At the classical level, the domains of two algebras are combined using Cartesian products. At the quantum level, the corresponding quantum domains are combined using tensor products. Furthermore, we present the conditions under which these products are compatible with the quantisations of ADTs. Definition 8.1. Let 𝐴 and 𝐵 be two algebras of signature Sig = (𝑆, OP). Then their product is defined as the algebra 𝐶 = 𝐴 × 𝐵 of the same signature Sig satisfying the following conditions: (1) for each sort 𝑠 ∈ 𝑆, 𝐶𝑠 = 𝐴𝑠 × 𝐵𝑠 (Cartesian product); (2) for each operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠, 𝑂 𝐶 is defined as follows: for any 𝑎𝑖 ∈ 𝐴𝑠𝑖 and 𝑏𝑖 ∈ 𝐵𝑠𝑖 (𝑖 = 1, . . . , 𝑛), 𝑂 𝐶 ((𝑎 1, 𝑏 1 ), . . . , (𝑎𝑛 , 𝑏𝑛 )) = (𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 ), 𝑂 𝐵 (𝑏 1, . . . , 𝑏𝑛 )).

(36)

In particular, for each constant symbol 𝑐 :→ 𝑠, we have 𝑐𝐶 = (𝑐 𝐴 , 𝑐 𝐵 ). We next define the corresponding product of quantum algebras. Let 𝑠 = 𝑠 1, . . . , 𝑠𝑛 be a string of quantum sorts. Define the canonical unitary operator ! ! 𝑛  𝑛 𝑛  Ì Ì Ì A B A B 𝑇𝑠 : H𝑠𝑖 ⊗ H𝑠𝑖 → H𝑠𝑖 ⊗ H𝑠𝑖 𝑖=1

𝑖=1

𝑖=1

by 𝑛 Ì

!

𝑛 Ì

!

𝑛 Ì

!

|𝛼𝑖 𝛽𝑖 ⟩ = |𝛼𝑖 ⟩ ⊗ |𝛽𝑖 ⟩ 𝑖=1 𝑖=1 𝑖=1 for any |𝛼𝑖 ⟩ ∈ H𝑠A and |𝛽𝑖 ⟩ ∈ H𝑠B𝑖 (𝑖 = 1, . . . , 𝑛) together with linear extension. 𝑖 𝑇𝑠

(37)

Definition 8.2. Let A and B be two quantum algebras of signature QSig = (𝑆𝑞 , K, U). Then their product is defined as the quantum algebra C = A ⊗ B of the same signature QSig satisfying the following conditions: (1) for each sort 𝑠 ∈ 𝑆𝑞 , H𝑠C = H𝑠A ⊗ H𝑠B (tensor product); (2) for each quantum state symbol |𝜓 ⟩ ∈ K of sort 𝑠 1, . . . , 𝑠𝑛 , |𝜓 ⟩ C = 𝑇𝑠−1 (|𝜓 ⟩ A ⊗ |𝜓 ⟩ B ); 1 ,...,𝑠𝑛 (3) for each quantum gate symbol 𝑈 ∈ U of sort 𝑠 1, . . . , 𝑠𝑛 , 𝑈 C = 𝑇𝑠−1 ◦ (𝑈 A ⊗ 𝑈 B ) ◦ 𝑇𝑠1,...,𝑠𝑛 1 ,...,𝑠𝑛

(38)

Quantisation of Abstract Data Types

27

Ë𝑛 Ë𝑛
A B A ⊗ 𝑈 B is defined by is a unitary operator on 𝑖=1 H𝑠C𝑖 = 𝑖=1 H𝑠𝑖 ⊗ H𝑠𝑖 , where 𝑈   𝑈 A ⊗ 𝑈 B (|𝛼 1 . . . 𝛼𝑛 ⟩ ⊗ |𝛽 1 . . . 𝛽𝑛 ⟩) = 𝑈 A (|𝛼 1 . . . 𝛼𝑛 ⟩) ⊗ 𝑈 B (|𝛽 1 . . . 𝛽𝑛 ⟩), (39) for any |𝛼𝑖 ⟩ ∈ H𝑠A and |𝛽𝑖 ⟩ ∈ H𝑠B𝑖 (𝑖 = 1, . . . , 𝑛) and extending linearly. Equivalently, 𝑖 Equation (38) can be expressed by the following commutative diagram: 𝑛 Ì

𝑛 Ì

𝑈C

H𝑠C𝑖

𝑖=1

𝑖=1 𝑇𝑠−1 1 ,...,𝑠𝑛

𝑇𝑠1 ,...,𝑠𝑛 𝑛 Ì 𝑖=1

8.1

! H𝑠A 𝑖

H𝑠C𝑖

⊗

𝑛 Ì 𝑖=1

! H𝑠B𝑖

𝑛 Ì 𝑈 A ⊗𝑈 B 𝑖=1

! H𝑠A 𝑖

⊗

𝑛 Ì

! H𝑠B𝑖

𝑖=1

Products of Quantisations

Let 𝐴 and 𝐵 be two algebras of the same signature Sig = (𝑆, OP), and let 𝐶 = 𝐴 × 𝐵. Suppose 𝜂 is a quantisation from Sig to QSig that satisfies 𝑆𝑞 = 𝜂 (𝑆). Suppose that A, B, and C are quantisations of 𝐴, 𝐵, and 𝐶, respectively, along 𝜂. Recall that the quantisation of 𝑠 ∈ 𝑆 is 𝑠𝑞 ∈ 𝑆𝑞 along 𝜂. For each 𝑠 ∈ 𝑆, we define 𝐽𝑠𝑞 : H𝑠C𝑞 → H𝑠A ⊗ H𝑠B𝑞 to be a linear operator that satisfies the following condition: 𝑞 𝐽𝑠𝑞 |(𝑎, 𝑏)⟩ = |𝑎⟩ ⊗ |𝑏⟩

(40)

for every 𝑎 ∈ 𝐴𝑠 and 𝑏 ∈ 𝐵𝑠 . Note that 𝐽𝑠𝑞 is a unitary. Let 𝐽 = (𝐽𝑠𝑞 )𝑠 ∈𝑆 . For concreteness, we consider when a BO-quantisation (and PO-quantisation) is compatible with products. For each 𝐷 ∈ {𝐴, 𝐵, 𝐶} and 𝑠 ∈ 𝑆, let 𝑘𝑠𝐷 : 𝐷𝑠 → Z |𝐷𝑠 | be the designated bijection, and let ⊞𝑠𝐷 be defined as in Section 4. Proposition 8.3 (Products of BO-qantisations). Suppose that every state symbol in K is introduced by 𝜂, and that every gate symbol in U is introduced by 𝜂. Let A, B, and C be BOquantisations of 𝐴, 𝐵, and 𝐶 = 𝐴 × 𝐵, respectively, along the same quantisation 𝜂. If   (𝑎, 𝑏) ⊞𝐶𝑠 (𝑎 ′, 𝑏 ′ ) = 𝑎 ⊞𝑠𝐴 𝑎 ′, 𝑏 ⊞𝑠𝐵 𝑏 ′ (41) for any 𝑠 ∈ 𝑆, 𝑎, 𝑎 ′ ∈ 𝐴𝑠 , and 𝑏, 𝑏 ′ ∈ 𝐵𝑠 , then 𝐽 in Equation (40) is an isomorphism from C to A ⊗ B. Proposition 8.4 (Products of PO-qantisations). Suppose that every state symbol in K is introduced by 𝜂, and that every gate symbol in U is introduced by 𝜂. Let A, B, and C be POquantisations of 𝐴, 𝐵, and 𝐶 = 𝐴 × 𝐵, respectively, along the same quantisation 𝜂. If       2𝜋𝑖 𝑘𝑠𝐶 ((𝑎, 𝑏))𝑘𝑠𝐶 ((𝑎 ′, 𝑏 ′ )) 2𝜋𝑖 𝑘𝑠𝐴 (𝑎)𝑘𝑠𝐴 (𝑎 ′ ) 2𝜋𝑖 𝑘𝑠𝐵 (𝑏)𝑘𝑠𝐵 (𝑏 ′ ) exp = exp exp (42) |𝐶𝑠 | |𝐴𝑠 | |𝐵𝑠 | for any 𝑠 ∈ 𝑆, 𝑎, 𝑎 ′ ∈ 𝐴𝑠 , and 𝑏, 𝑏 ′ ∈ 𝐵𝑠 , then 𝐽 is an isomorphism from C to A ⊗ B. 9

CONCLUSION

This paper developed a universal-algebraic framework for data abstraction in quantum programming. We formally defined the notion of abstract quantum data types and a quantisation of classical data types and proved that their equational specifications can be soundly lifted to their quantisations. Generalised bit-oracle and phase-oracle quantisations arise as instances of this construction and are related through phase kickback. Further, the examples of quantum arrays, the three-qubit

28

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

repetition code, and the nine-qubit Shor code illustrate how quantum data and operations can be organised and specified within the framework. We also established conditions under which data type quantisation preserves embeddings, isomorphisms, and products. As a first step toward introducing data abstraction into quantum programming, in this paper, we examine only two typical forms of quantisation, namely bit oracles and phase oracles. One can expect that more forms of quantisation will emerge in the development of future quantum algorithms and programs. We also consider only purely quantum abstract data types in this paper. In practical applications, quantum and classical data are often involved in the same program, and measurement outcomes of quantum data are stored as classical data that subsequently participate in classical computations. This observation suggests another interesting topic for future research: classical-quantum hybrid abstract data types. We can expect that data abstraction in quantum programming enables programmers to reason about complex quantum behaviour in a manageable way as in classical programming. By hiding mathematical and physical complexity while enforcing quantum constraints, abstraction makes quantum software development more accessible, safer, and more scalable. As quantum computing matures, well-designed abstractions will be crucial for bridging the gap between theoretical algorithms and practical implementations. ACKNOWLEDGMENTS This work was supported in part by the Australian Research Council under Grant DP250102952. REFERENCES [1] Andris Ambainis. 2007. Quantum walk algorithm for element distinctness. SIAM J. Comput. 37 (2007), 210–239. [2] Andris Ambainis. 2018. Understanding quantum algorithms via query complexity. In Proceedings of the International Congress of Mathematicians (ICM). 3265–3285. [3] Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 286–300. [4] Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp. 2002. Quantum amplitude amplification and estimation. In Quantum Computation and Information. Contemporary Mathematics, Vol. 305. 53–74. [5] Luca Cardelli and Peter Wegner. 1985. On understanding types, data abstraction, and polymorphism. Comput. Surveys 17, 4 (1985), 471–523. [6] Cirq Developers. 2026. Cirq. Zenodo. https://doi.org/10.5281/zenodo.4062499 [7] David Deutsch and Richard Jozsa. 1992. Rapid solution of problems by quantum computation. Proceedings of the Royal Society of London A 439 (1992), 553–558. [8] Olivia Di Matteo. 2025. The art of abstraction in quantum software. In 2025 IEEE/ACM International Workshop on Quantum Software Engineering (Q-SE). 25–26. [9] Hartmut Ehrig and Bernd Mahr. 1985. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer. [10] Vittorio Giovannetti, Seth Lloyd, and Lorenzo Maccone. 2008. Architectures for a quantum random access memory. Physical Review A 78, Article 052310 (2008). [11] Vittorio Giovannetti, Seth Lloyd, and Lorenzo Maccone. 2008. Quantum random access memory. Physical Review Letters 100, Article 160501 (2008). [12] Joseph A. Goguen and José Meseguer. 1992. Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science 105 (1992), 217–273. [13] Daniel Gottesman. 2024. Surviving as a quantum computer in a classical world. Textbook manuscript preprint. [14] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: a scalable quantum programming language. In Proceedings of the 34th ACM Conference on Programming Language Design and Implementation (PLDI). 333–342. [15] Lov K. Grover. 1996. A fast quantum mechanical algorithm for database search. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC). 212–219. [16] Jingzhe Guo, Huazhe Lou, Jintao Yu, Riling Li, Wang Fang, Junyi Liu, Peixun Long, Shenggang Ying, and Mingsheng Ying. 2023. isQ: An Integrated Software Stack for Quantum Programming. IEEE Transactions on Quantum Engineering

Quantisation of Abstract Data Types

29

4, Article 2500116 (2023), 16 pages. [17] John V. Guttag. 1977. Abstract data types and the development of data structures. Commun. ACM 20, 6 (1977), 396–404. [18] Bettina Heim, Mathias Soeken, Sarah Marshall, Chris Granade, Martin Roetteler, Alan Geller, Matthias Troyer, and Krysta Svore. 2020. Quantum programming languages. Nature Reviews Physics 2 (2020), 709–722. [19] Ali Javadi-Abhari, Matthew Treinish, Kevin Krsulich, Christopher J. Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul D. Nation, Lev S. Bishop, Andrew W. Cross, Blake R. Johnson, and Jay M. Gambetta. 2024. Quantum computing with Qiskit. arXiv:2405.08810 [quant-ph] [20] Stacey Jeffery, Robin Kothari, and Frédéric Magniez. 2013. Nested quantum walks with quantum data structures. In Proceedings of the 24th Annual ACM-SIAM symposium on Discrete algorithms (SODA). 1474–1485. [21] Ce Jin and Jakob Nogler. 2023. Quantum speed-ups for string synchronizing sets, longest common substring, and k-mismatch matching. In Proceedings of the 34th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). 5090–5121. [22] Emanuel Knill and Raymond Laflamme. 1997. Theory of quantum error-correcting codes. Physical Review A 55 (1997), 900–911. [23] Emanuel H. Knill. 1996. Conventions for quantum pseudo-code. Technical Report. Los Alamos National Laboratory. [24] Mark Koch, Alan Lawrence, Kartik Singhal, Seyon Sivarajah, and Ross Duncan. 2025. GUPPY: Pythonic quantumclassical programming. arXiv:2510.12582 [25] Barbara Liskov. 1987. Data abstraction and hierarchy. ACM SIGPLAN Notices 23, 5 (1987), 17–34. [26] Barbara Liskov and Stephen Zilles. 1974. Programming with abstract data types. ACM SIGPLAN Notices 9, 4 (1974), 50–59. [27] John McCarthy. 1962. Towards a mathematical science of computation. In IFIP Congress 62. [28] Aran Nayebi, Scott Aaronson, Aleksandrs Belovs, and Luca Trevisan. 2015. Quantum lower bound for inverting a permutation with advice. Quantum Information & Computation 15 (2015), 901–913. [29] Michael A. Nielsen and Isaac L. Chuang. 2000. Quantum Computation and Quantum Information. Cambridge University Press. [30] Santiago Núñez-Corrales, Olivia Di Matteo, John Dumbell, Marcus Edwards, Edoardo Giusto, Scott Pakin, and Vlad Stirbu. 2025. Productive quantum programming needs better abstract machines. In 2025 IEEE International Conference on Quantum Computing and Engineering (QCE). 816–826. [31] Romain Péchoux, Simon Perdrix, Mathys Rennela, and Vladimir Zamdzhiev. 2020. Quantum programming with inductive datatypes: causality and affine type theory. In Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). 562–581. [32] Raphael Seidel, Sebastian Bock, René Zander, Matic Petrič, Niklas Steinmann, Nikolay Tcholtchev, and Manfred Hauswirth. 2024. Qrisp: a framework for compilable high-level programming of gate-based quantum computers. arXiv:2406.14792 [33] Peter W. Shor. 1995. Scheme for reducing decoherence in quantum computer memory. Physical Review A 52 (1995), R2493–R2496. [34] Peter W. Shor. 1997. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM J. Comput. 26 (1997), 1484–1509. [35] Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. 2018. Q#: enabling scalable quantum computing and development with a high-level DSL. In Proceedings of the Real World Domain Specific Languages Workshop (RWSDL). Article 7, 10 pages. [36] Tamás Varga, Yaiza Aragonés-Soria, and Manuel Oriol. 2024. Quantum types: going beyond qubits and quantum gates. In Proceedings of the 5th ACM/IEEE International Workshop on Quantum Software Engineering (Q-SE). 49–52. [37] Qisheng Wang, Zhean Xu, and Zhicheng Zhang. 2026. Quantum data structure for range minimum query. J. Comput. System Sci. 157, Article 103756 (2026). [38] Niklaus Wirth. 1976. Algorithms + Data Structures = Programs. Prentice-Hall. [39] Mingsheng Ying. 2024. Foundations of Quantum Programming (second ed.). Morgan Kaufmann. [40] Charles Yuan and Michael Carbin. 2022. Tower: data structures in quantum superposition. Proceedings of the ACM on Programming Languages 6, OOPSLA2, Article 134 (2022), 259–288 pages.

30

A

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

DEFERRED PROOFS

All of the theorems and propositions in the main text of this paper were presented without proofs. In this appendix, we give all of these proofs. We first prove the following lemma, which is useful for proving Theorem 4.5. Lemma A.1. Let 𝐴 and A be as in Theorem 4.5. Let 𝑡 be a classical term involving classical variables 𝑥 1 : 𝑠 1, . . . , 𝑥𝑛 : 𝑠𝑛 and 𝑝 be the principal variable of 𝜂 (𝑡). We use 𝑞 = 𝑞 1, . . . , 𝑞𝑛 to denote the designated variables 𝑞𝑥 1 , . . . , 𝑞𝑥𝑛 as in Definition 4.3. Denote 𝑎 = 𝑎 1, . . . , 𝑎𝑛 ∈ 𝐴𝑠1 , . . . , 𝐴𝑠𝑛 . Define 𝜎𝑎 to be an assignment of classical variables with 𝜎𝑎 (𝑥𝑖 ) = 𝑎𝑖 for 𝑖 = 1, . . . , 𝑛. For any quantum state ∑︁ |𝜑⟩𝑞 = 𝛽𝑎 |𝑎⟩𝑞 , 𝑎

we have eval |𝜑 ⟩ (𝜂 (𝑡)) ↓ 𝑝 =

∑︁

|𝛽𝑎 | 2 |eval𝜎𝑎 (𝑡)⟩⟨eval𝜎𝑎 (𝑡)|𝑝 ,

𝑎

where eval on the LHS is defined in the quantum algebra A, and eval on the RHS is defined in the classical algebra 𝐴. Proof. We first consider the lemma for the computational-basis states; that is, |𝜑⟩ = |𝑎⟩ for some 𝑎. This case can be proved by induction on the length of 𝑡 with the following induction hypothesis: • IH: Let 𝑜 denote the variables involved in the quantisation 𝜂 (𝑡) but not in 𝑝, 𝑞. For any classical assignment 𝜎 of 𝑥, let 𝑎𝑖 = 𝜎 (𝑥𝑖 ) and 𝑎 = 𝑎 1, . . . , 𝑎𝑛 . There exists a quantum state |𝛾⟩ such that: eval |𝑎⟩ (𝜂 (𝑡)) = |𝑎⟩𝑞 |eval𝜎 (𝑡)⟩𝑝 |𝛾⟩𝑜 . (43) There are three cases: • If 𝑡 = 𝑐, then 𝜂 (𝑡) = |𝜓𝑐 ⟩𝑝 and |𝜓𝑐 ⟩ A = |𝑐 𝐴 ⟩. Thus, Equation (43) holds. • If 𝑡 = 𝑥, then 𝜂 (𝑥) = SUM 𝑠 [𝑞𝑥 , 𝑞] |0⟩𝑞 . Since 𝑘𝑠 (0𝑠𝐴 ) = 0 and 𝑎 ⊞𝑠 0𝑠𝐴 = 𝑎, we have eval |𝑎⟩ (𝜂 (𝑥)) = SUM 𝑠 [𝑞𝑥 , 𝑞] A |𝑎⟩𝑞𝑥 |0𝑠𝐴 ⟩𝑞 = |𝑎⟩𝑞𝑥 |𝑎⟩𝑞 . Thus, Equation (43) holds. • If 𝑡 = 𝑂 (𝑡 1, . . . , 𝑡𝑚 ), then 𝜂 (𝑡) = 𝐶 1 ; . . . ; 𝐶𝑚 ; pre𝑂 [𝑝 1, . . . , 𝑝𝑚 , 𝑟 ]; 𝑈𝑂 [𝑝 1, . . . , 𝑝𝑚 , 𝑟 ]; post𝑂 [𝑝 1, . . . , 𝑝𝑚 , 𝑟 ] |𝜓 1 ⟩ . . . |𝜓𝑚 ⟩ |0⟩𝑟 , where each 𝜂 (𝑡𝑖 ) = 𝐶𝑖 |𝜓𝑖 ⟩ has principal variable 𝑝𝑖 . Note that in the in-place case, 𝑝 = 𝑝𝑖 for the designated index 𝑖 in Definition 4.1; in the out-of-place case, 𝑝 is the first variable in 𝑟 . By the IH for 𝑡 1, . . . , 𝑡𝑚 , there exists a |Γ⟩ such that eval |𝑎⟩ (𝐶 1 ; . . . ; 𝐶𝑚 |𝜓 1 ⟩ . . . |𝜓𝑚 ⟩) = |𝑎⟩𝑞 |𝑏 1, . . . , 𝑏𝑚 ⟩𝑝 1,...,𝑝𝑚 |Γ⟩𝑜 1,...,𝑜𝑚 ,

(44)

where each 𝑏𝑖 = eval𝜎 (𝑡𝑖 ), and 𝑜𝑖 are additional variables involved in 𝜂 (𝑡𝑖 ) but not in 𝑝𝑖 , 𝑞. By Equation (5), we further have post𝑂A 𝑈𝑂A pre𝑂A |𝑏 1, . . . , 𝑏𝑚 ⟩𝑝 1,...,𝑝𝑚 |0⟩𝑟 = |𝑂 𝐴 (𝑏 1, . . . , 𝑏𝑚 )⟩𝑝 |𝛾 ′ ⟩

(45)

for some |𝛾 ′ ⟩. Combining Equations (44) and (45), we obtain eval |𝑎⟩ (𝜂 (𝑡)) = |𝑎⟩𝑞 |eval𝜎 (𝑡)⟩𝑝 (|Γ⟩ |𝛾 ′ ⟩)𝑜 , and Equation (43) holds. Since all |𝑎⟩𝑞 are orthogonal, by linearity and the tracing out of 𝑞, it is easy to prove the lemma for any quantum state |𝜑⟩. □

Quantisation of Abstract Data Types

31

Proof of Theorem 4.5. Since A is already a quantum algebra of QSig, it suffices to show that A satisfies every equation in 𝜂 (𝐸). Consider any equation in 𝐸: 𝑒 = (∀𝑥 1 : 𝑠 1, . . . , 𝑥𝑛 : 𝑠𝑛 ) (𝑡 1 = 𝑡 2 ). We use 𝑞 = 𝑞 1, . . . , 𝑞𝑛 to denote the designated variables 𝑞𝑥 1 , . . . , 𝑞𝑥𝑛 corresponding to 𝑥 1, . . . , 𝑥𝑛 , as in Definition 4.3. Let 𝑝 be the common principal variable of 𝜂 (𝑡 1 ) and 𝜂 (𝑡 2 ), as in Definition 4.4. Consider an arbitrary quantum state ∑︁ |𝜑⟩𝑞 = 𝛽𝑎 |𝑎⟩𝑞 . 𝑎

Since 𝐴 is an algebra of Spec and 𝑒 ∈ 𝐸, we have 𝐴 |= 𝑒. Therefore, for every 𝑎 ∈ 𝐴𝑠1 × · · · × 𝐴𝑠𝑛 , eval𝜎𝑎 (𝑡 1 ) = eval𝜎𝑎 (𝑡 2 ).

(46)

Applying Lemma A.1 to 𝑡 1 and 𝑡 2 , and using Equation (46), we obtain eval |𝜑 ⟩ (𝜂 (𝑡 1 )) ↓ 𝑝 = eval |𝜑 ⟩ (𝜂 (𝑡 2 )) ↓ 𝑝, which is essentially A |= 𝜂 (𝑒) by the validity of equations (see Definition 3.6). The conclusion then follows. □ Proof of Proposition 5.1. Note that in Equation (20), all variables are principal variables. To show that the equation is valid in algebra A, by linearity, it suffices to consider any computationalbasis state of variables 𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 , 𝑞𝑢 : |𝜑⟩ = |𝑎⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣⟩𝑞 𝑣 |𝑢⟩𝑞𝑢 . Let 𝑎 ′ be an array with 𝑎 ′ [𝑖] = 𝑎[𝑖] for 𝑖 ≠ 𝑗 and 𝑎 ′ [ 𝑗] = 𝑢. By evaluating the LHS of Equation (20), we have eval |𝜑 ⟩ (qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ]; qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ])   = qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ] qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ] |𝑎⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣⟩𝑞 𝑣 |𝑢⟩𝑞𝑢   = qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ] |𝑎 ′ ⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣⟩𝑞 𝑣 |𝑎[ 𝑗]⟩𝑞𝑢 = |𝑎 ′ ⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣 ⊞ 𝑢⟩𝑞 𝑣 |𝑎[ 𝑗]⟩𝑞𝑢 . By evaluating the RHS of Equation (20), we have eval |𝜑 ⟩ (SUM [𝑞𝑢 , 𝑞 𝑣 ]; qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ])   = qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ] SUM [𝑞𝑢 , 𝑞 𝑣 ] |𝑎⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣⟩𝑞 𝑣 |𝑢⟩𝑞𝑢   = qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ] |𝑎⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣 ⊞ 𝑢⟩𝑞 𝑣 |𝑢⟩𝑞𝑢 = |𝑎 ′ ⟩𝑞𝑎 | 𝑗⟩𝑞𝑖 |𝑣 ⊞ 𝑢⟩𝑞 𝑣 |𝑎[ 𝑗]⟩𝑞𝑢 . By linearity, we have eval |𝜑 ⟩ (qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ]; qread [𝑞𝑎 , 𝑞𝑖 , 𝑞 𝑣 ]) = eval |𝜑 ⟩ (SUM [𝑞𝑢 , 𝑞 𝑣 ]; qwrite[𝑞𝑎 , 𝑞𝑖 , 𝑞𝑢 ]) for any quantum state |𝜑⟩, and the conclusion follows. □

32

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

Proof of Proposition 6.1. Note that in Equations (23) and (24), 𝑞𝑎 is the only principal variable. By Equations (21) and (22) and the definition of qcorr, for every 𝑥 ∈ {0, 1} and 𝑖 ∈ {0, 1, 2}, we have qcorr [𝑞𝑎 , 𝑞𝑠 ] |enc𝐴 (𝑥)⟩𝑞𝑎 |⊥⟩𝑞𝑠 (47) = |corr 𝐴 (enc𝐴 (𝑥))⟩𝑞𝑎 |syn(enc𝐴 (𝑥))⟩𝑞𝑠 = |enc𝐴 (𝑥)⟩𝑞𝑎 |⊥⟩𝑞𝑠 , qcorr [𝑞𝑎 , 𝑞𝑠 ] |flip𝐴 (enc𝐴 (𝑥), 𝑖)⟩𝑞𝑎 |⊥⟩𝑞𝑠 (48) = |corr 𝐴 (flip𝐴 (enc𝐴 (𝑥), 𝑖))⟩𝑞𝑎 |syn(flip𝐴 (enc𝐴 (𝑥), 𝑖))⟩𝑞𝑠 = |enc𝐴 (𝑥)⟩𝑞𝑎 |𝑖⟩𝑞𝑠 . To prove that Equation (23) is valid in A, consider an arbitrary state of the variable 𝑞𝑙 : ∑︁ |𝜑⟩𝑞𝑙 = 𝛼𝑥 |𝑥⟩𝑞𝑙 . 𝑥 ∈ {0,1}

By evaluating the LHS and using Equation (47), we have   ∑︁ eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝛼𝑥 |𝑥, 𝑥, 𝑥⟩𝑞𝑎 |⊥⟩𝑞𝑠 . 𝑥

By evaluating the RHS, we have   ∑︁ eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝛼𝑥 |𝑥, 𝑥, 𝑥⟩𝑞𝑎 |⊥⟩𝑞𝑠 . 𝑥

Both evaluations give the same state, so Equation (23) is valid. To prove that Equation (24) is valid in A, consider an arbitrary state of variables 𝑞𝑙 , 𝑞𝑖 : ∑︁ 𝛼𝑥,𝑖 |𝑥⟩𝑞𝑙 |𝑖⟩𝑞𝑖 . |𝜑⟩𝑞𝑙 𝑞𝑖 = 𝑥 ∈ {0,1} 𝑖 ∈ {0,1,2}

By evaluating the LHS and using Equation (48), we have   ∑︁ eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ]; qflip[𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝛼𝑥,𝑖 |𝑥, 𝑥, 𝑥⟩𝑞𝑎 |𝑖⟩𝑞𝑖 |𝑖⟩𝑞𝑠 . 𝑥,𝑖

By evaluating the RHS, we have   ∑︁ 𝛼𝑥,𝑖 |𝑥, 𝑥, 𝑥⟩𝑞𝑎 |𝑖⟩𝑞𝑖 |⊥⟩𝑞𝑠 . eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝑥,𝑖

Since 𝑞𝑎 is the principal variable, we trace out 𝑞𝑙 , 𝑞𝑖 , 𝑞𝑠 . Both sides of Equation (24) give 2 ∑︁

∑︁

𝛼𝑥,𝑖 𝛼𝑥 ′ ,𝑖 |𝑥, 𝑥, 𝑥⟩⟨𝑥 ′, 𝑥 ′, 𝑥 ′ |𝑞𝑎 .

𝑖=0 𝑥,𝑥 ′ ∈ {0,1}

Therefore, Equation (24) is valid. The conclusion immediately follows. □  Lemma A.2. There exists an orthonormal basis |Φ𝑥,𝑠 ⟩ : 𝑥 ∈ {0, 1}, 𝑠 ∈ {0, 1, 2, ⊥}4 that satisfies Equation (28).   ⊗3 B Proof. We first consider the following orthonormal basis of Hpqbit :   |000⟩ ± |111⟩ |100⟩ ± |011⟩ |010⟩ ± |101⟩ |001⟩ ± |110⟩ , , , √ √ √ √ 2 2 2 2

Quantisation of Abstract Data Types

33

Let 𝑖 = 3𝑟 + 𝑡, where 𝑟, 𝑡 ∈ {0, 1, 2}. For 𝑃 ∈ {1, 𝑋, 𝑌 , 𝑍 }, applying 𝑃𝑖 to the state in Equation (26) gives   ⊗𝑟     ⊗ (2−𝑟 ) |000⟩ + (−1)𝑥 |111⟩ |000⟩ + (−1)𝑥 |111⟩ |000⟩ + (−1)𝑥 |111⟩ 𝑃𝑖 |Ψ𝑥 ⟩ = ⊗ 𝑃𝑡 ⊗ , (49) √ √ √ 2 2 2 where 𝑃𝑡 applies 𝑃 on the qubit indexed by 𝑡 within a group of three qubits. In particular, for different 𝑃𝑡 , we have  |100⟩ + (−1)𝑥 |011⟩   , 𝑡 = 0, √   2 𝑥      𝑥  |010⟩ + (−1) |101⟩  |000⟩ + (−1) |111⟩ , 𝑡 = 1, √ = 𝑋𝑡 √  2 𝑥 2     |001⟩ + (−1) |110⟩ , 𝑡 = 2,  √   2    |000⟩ + (−1)𝑥 |111⟩ |000⟩ − (−1)𝑥 |111⟩ 𝑍𝑡 = , (50) √ √ 2 2  |100⟩ − (−1)𝑥 |011⟩   , 𝑡 = 0, √    2 𝑥      |010⟩ − (−1) |101⟩  |000⟩ + (−1)𝑥 |111⟩ , 𝑡 = 1, √ =i 𝑌𝑡 √  2 𝑥 2    |001⟩ − (−1) |110⟩   , 𝑡 = 2. √   2  From Equation (27), 𝜎 (1, 𝑖) = (⊥, ⊥, ⊥, ⊥) for every 𝑖 ∈ 𝐵 idx , and 1𝑖 |Ψ𝑥 ⟩ = |Ψ𝑥 ⟩. Apart from the case 𝑃 = 𝑃 ′ = 1, 𝜎 (𝑃, 𝑖) = 𝜎 (𝑃 ′, 𝑖 ′ ) for distinct pairs (𝑃, 𝑖) ≠ (𝑃 ′, 𝑖 ′ ) only if 𝑃 = 𝑃 ′ = 𝑍 and 𝑖, 𝑖 ′ ∈ {3𝑟, 3𝑟 + 1, 3𝑟 + 2} for some 𝑟 ∈ {0, 1, 2}. Moreover, for every 𝑥 ∈ 𝐵 lbit and 𝑟 ∈ {0, 1, 2}, we have 𝑍 3𝑟 |Ψ𝑥 ⟩ = 𝑍 3𝑟 +1 |Ψ𝑥 ⟩ = 𝑍 3𝑟 +2 |Ψ𝑥 ⟩ . Thus, for every 𝑥 ∈ 𝐵 lbit , 𝑃, 𝑃 ′ ∈ {1, 𝑋, 𝑌 , 𝑍 }, and 𝑖, 𝑖 ′ ∈ 𝐵 idx , 𝜎 (𝑃, 𝑖) = 𝜎 (𝑃 ′, 𝑖 ′ ) ⇒ 𝑃𝑖 |Ψ𝑥 ⟩ = 𝑃𝑖′′ |Ψ𝑥 ⟩ . By Equations (27), (49) and (50), for every 𝑥, 𝑥 ′ ∈ 𝐵 lbit , 𝑃, 𝑃 ′ ∈ {1, 𝑋, 𝑌 , 𝑍 }, and 𝑖, 𝑖 ′ ∈ 𝐵 idx , it is easy to verify that ( 1, 𝑥 = 𝑥 ′ and 𝜎 (𝑃, 𝑖) = 𝜎 (𝑃 ′, 𝑖 ′ ), † ′ ⟨Ψ𝑥 | 𝑃𝑖 𝑃𝑖 ′ |Ψ𝑥 ′ ⟩ = 0, 𝑜.𝑤 . Therefore, Equation (28) is well-defined and these |Φ𝑥,𝜎 (𝑃,𝑖 ) ⟩ can be extended to an orthonormal B basis of Hqarray . □ Proof of Proposition 6.2. Note that in Equations (29) to (32), 𝑞𝑎 is the only principal variable. By Equations (27) and (28) and the definition of qcorr, for every 𝑥 ∈ 𝐵 lbit , we have qcorr [𝑞𝑎 , 𝑞𝑠 ] |Ψ𝑥 ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = qcorr [𝑞𝑎 , 𝑞𝑠 ] |Φ𝑥,(⊥,⊥,⊥,⊥) ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = |Ψ𝑥 ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 .

(51)

Similarly, for every 𝑥 ∈ 𝐵 lbit , 𝑃 ∈ {𝑋, 𝑌 , 𝑍 }, and 𝑖 ∈ 𝐵 idx , qcorr [𝑞𝑎 , 𝑞𝑠 ] 𝑃𝑖 |Ψ𝑥 ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = qcorr [𝑞𝑎 , 𝑞𝑠 ] |Φ𝑥,𝜎 (𝑃,𝑖 ) ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = |Ψ𝑥 ⟩𝑞𝑎 |𝜎 (𝑃, 𝑖)⟩𝑞𝑠 .

(52)

34

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

To prove that Equation (29) is valid in B, consider an arbitrary state of the variable 𝑞𝑙 : ∑︁ |𝜑⟩𝑞𝑙 = 𝛼𝑥 |𝑥⟩𝑞𝑙 . 𝑥 ∈ {0,1}

By evaluating the LHS and using Equation (51), we have   ∑︁ eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝛼𝑥 |Ψ𝑥 ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 . 𝑥

By evaluating the RHS, we have   ∑︁ eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝛼𝑥 |Ψ𝑥 ⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 . 𝑥

Both evaluations give the same state, so Equation (29) is valid. To prove that Equations (30) to (32) are valid in B, consider an arbitrary state of variables 𝑞𝑙 , 𝑞𝑖 : ∑︁ |𝜑⟩𝑞𝑙 𝑞𝑖 = 𝛼𝑥,𝑖 |𝑥⟩𝑞𝑙 |𝑖⟩𝑞𝑖 . 𝑥 ∈ {0,1} 𝑖 ∈ {0,1,...,8}

By evaluating the LHSs and using Equation (52), we have   eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ]; qflipX [𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ∑︁ = |0⟩𝑞𝑙 𝛼𝑥,𝑖 |Ψ𝑥 ⟩𝑞𝑎 |𝑖⟩𝑞𝑖 |𝜎 (𝑋, 𝑖)⟩𝑞𝑠 , 𝑥,𝑖



eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ]; qflipZ [𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ∑︁ = |0⟩𝑞𝑙 𝛼𝑥,𝑖 |Ψ𝑥 ⟩𝑞𝑎 |𝑖⟩𝑞𝑖 |𝜎 (𝑍, 𝑖)⟩𝑞𝑠 ,



𝑥,𝑖



eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ]; qflipX [𝑞𝑎 , 𝑞𝑖 ]; qflipZ [𝑞𝑎 , 𝑞𝑖 ]; qcorr [𝑞𝑎 , 𝑞𝑠 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 ∑︁ = i |0⟩𝑞𝑙 𝛼𝑥,𝑖 |Ψ𝑥 ⟩𝑞𝑎 |𝑖⟩𝑞𝑖 |𝜎 (𝑌 , 𝑖)⟩𝑞𝑠 .



𝑥,𝑖

By evaluating the RHS, we have   ∑︁ eval |𝜑 ⟩ qenc[𝑞𝑙 , 𝑞𝑎 ] |0⟩𝑞𝑎 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 = |0⟩𝑞𝑙 𝛼𝑥,𝑖 |Ψ𝑥 ⟩𝑞𝑎 |𝑖⟩𝑞𝑖 |⊥, ⊥, ⊥, ⊥⟩𝑞𝑠 . 𝑥,𝑖

Since 𝑞𝑎 is the principal variable, we trace out 𝑞𝑙 , 𝑞𝑖 , 𝑞𝑠 . Both sides of Equations (30) to (32) give 8 ∑︁

∑︁

𝛼𝑥,𝑖 𝛼𝑥 ′ ,𝑖 |Ψ𝑥 ⟩⟨Ψ𝑥 ′ |𝑞𝑎 .

𝑖=0 𝑥,𝑥 ′ ∈ {0,1}

Therefore, Equations (30) to (32) are valid. The conclusion immediately follows.

□

Proof of Proposition 7.3. As observed after Equation (35), every 𝐺𝑠𝑞 is an isometric embedding. It suffices to verify the two conditions in Definition 7.2. (1) Let |𝜓 ⟩ ∈ K be a quantum state symbol. Then, there is a constant symbol 𝑐 :→ 𝑠 such that ′ |𝜓 ⟩ = 𝜂 (𝑐). Since 𝑔 is a homomorphism, 𝑔𝑠 (𝑐 𝐴 ) = 𝑐 𝐴 , which means ′

′

𝐺𝑠𝑞 |𝜓 ⟩ A = 𝐺𝑠𝑞 |𝑐 𝐴 ⟩ = |𝑐 𝐴 ⟩ = |𝜓 ⟩ A . Consequently, Equation (33) holds. (2) Let 𝑈 ∈ U be a quantum gate symbol. It suffices to consider the following cases.

Quantisation of Abstract Data Types

35

• Suppose 𝑈 = pre𝑂 or 𝑈 = post𝑂 for some nonconstant operation symbol 𝑂. This case is trivial because pre𝑂B = post𝑂B = 1 for B ∈ {A, A ′ }. • Suppose 𝑈 = 𝑈𝑂 for some nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠. Write 𝑠𝑖𝑞 = 𝜂 (𝑠𝑖 ) and 𝑠𝑞 = 𝜂 (𝑠). For 𝑎𝑖 ∈ 𝐴𝑠𝑖 and 𝑎 ∈ 𝐴𝑠 , we have   𝐺𝑠1𝑞 ⊗ . . . ⊗ 𝐺𝑠𝑛𝑞 ⊗ 𝐺𝑠𝑞 𝑈𝑂A |𝑎 1 ⟩ · · · |𝑎𝑛 ⟩ |𝑎⟩ = |𝑔𝑠1 (𝑎 1 )⟩ · · · |𝑔𝑠𝑛 (𝑎𝑛 )⟩ |𝑔𝑠 (𝑎 ⊞𝑠𝐴 𝑂 𝐴 (𝑎 1, . . . , 𝑎𝑛 ))⟩ ′

′

= |𝑔𝑠1 (𝑎 1 )⟩ · · · |𝑔𝑠𝑛 (𝑎𝑛 )⟩ |𝑔𝑠 (𝑎) ⊞𝑠𝐴 𝑂 𝐴 (𝑔𝑠1 (𝑎 1 ), . . . , 𝑔𝑠𝑛 (𝑎𝑛 ))⟩   ′ = 𝑈𝑂A 𝐺𝑠1𝑞 ⊗ . . . ⊗ 𝐺𝑠𝑛𝑞 ⊗ 𝐺𝑠𝑞 |𝑎 1 ⟩ · · · |𝑎𝑛 ⟩ |𝑎⟩ . ′

The second equality follows from the condition about ⊞𝑠𝐴 and ⊞𝑠𝐴 and the fact that 𝑔 is a homomorphism. By linearity, Equation (34) holds. Thus, 𝐺 satisfies Definition 7.2 and is an embedding from A to A ′ . □ Proof of Proposition 7.4. As observed after Equation (35), every 𝐺𝑠𝑞 is unitary. It suffices to verify the two conditions in Definition 7.2. For each 𝑠 ∈ 𝑆, let 𝑁𝑠 = |𝐴𝑠 | = 𝐴𝑠′ and 𝜔𝑠 = 𝑒 2𝜋𝑖/𝑁𝑠 . (1) Let |𝜓 ⟩ ∈ K be a quantum state symbol. Similar to the proof of Proposition 7.3, 𝐺𝑠𝑞 |𝜓 ⟩ A = ′ |𝜓 ⟩ A and therefore Equation (33) holds. (2) Let 𝑈 ∈ U be a quantum gate symbol. It suffices to consider the following cases. • Suppose 𝑈 = pre𝑂 or post𝑂 for some nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠. For any 𝑎 ∈ 𝐴𝑠 , since 𝑔𝑠 is bijective, 1 ∑︁ 𝑘𝑠𝐴 (𝑎)𝑘𝑠𝐴 (𝑏 ) 𝐺𝑠𝑞 QFT |𝐴𝑠 | |𝑎⟩ = √︁ 𝜔𝑠 |𝑔𝑠 (𝑏)⟩ |𝐴𝑠 | 𝑏 ∈𝐴𝑠 ∑︁ ′ ′ 1 𝑘 𝐴 (𝑔 (𝑎) )𝑘𝑠𝐴 (𝑔𝑠 (𝑏 ) ) (53) = √︁ 𝜔𝑠 𝑠 𝑠 |𝑔𝑠 (𝑏)⟩ |𝐴𝑠 | 𝑔𝑠 (𝑏 ) ∈𝐴𝑠′ = QFT |𝐴𝑠 | 𝐺𝑠𝑞 |𝑎⟩ . Ë𝑛 ′ Here, the second equality uses 𝑘𝑠𝐴 = 𝑘𝑠𝐴 ◦ 𝑔𝑠 . Tensoring Equation (53) with 𝑖=1 𝐺𝑠𝑖𝑞 followed by linearity leads to Equation (34) for 𝑈 = pre𝑂 . Taking the adjoints proves it for 𝑈 = post𝑂 . • Suppose 𝑈 = 𝑈𝑂 for some nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠. For 𝑎𝑖 ∈ 𝐴𝑠𝑖 and 𝑎 ∈ 𝐴𝑠 , Equation (9) gives (𝐺𝑠1𝑞 ⊗ . . . ⊗ 𝐺𝑠𝑛𝑞 ⊗ 𝐺𝑠𝑞 )𝑈𝑂A |𝑎 1, . . . , 𝑎𝑛 ⟩ |𝑎⟩ 𝑘 𝐴 (𝑎)𝑘𝑠𝐴 (𝑂 𝐴 (𝑎 1 ,...,𝑎𝑛 ) )

= 𝜔𝑠 𝑠

|𝑔𝑠1 (𝑎 1 ), . . . , 𝑔𝑠𝑛 (𝑎𝑛 )⟩ |𝑔𝑠 (𝑎)⟩

′ ′ ′ 𝑘𝑠𝐴 (𝑔𝑠 (𝑎) )𝑘𝑠𝐴 (𝑂 𝐴 (𝑔𝑠1 (𝑎 1 ),...,𝑔𝑠𝑛 (𝑎𝑛 ) ) )

= 𝜔𝑠

|𝑔𝑠1 (𝑎 1 ), . . . , 𝑔𝑠𝑛 (𝑎𝑛 )⟩ |𝑔𝑠 (𝑎)⟩

′ = 𝑈𝑂A (𝐺𝑠1𝑞 ⊗ . . . ⊗ 𝐺𝑠𝑛𝑞 ⊗ 𝐺𝑠𝑞 ) |𝑎 1, . . . , 𝑎𝑛 ⟩ |𝑎⟩ . ′

The second equality follows from 𝑘𝑠𝐴 ◦ 𝑔𝑠 = 𝑘𝑠𝐴 and the fact that 𝑔 is a homomorphism. By linearity, Equation (34) holds. Thus, 𝐺 satisfies Definition 7.2 and is an isomorphism from A to A ′ . □ Proof of Proposition 8.3. As observed after Equation (40), every 𝐽𝑠𝑞 is unitary. It suffices to verify the two conditions in Definition 7.2.

36

Mingsheng Ying, Zhicheng Zhang, and Kean Chen

(1) Let |𝜓 ⟩ ∈ K be a quantum state symbol, so |𝜓 ⟩ = 𝜂 (𝑐) for a constant symbol 𝑐 :→ 𝑠. Since |𝜓 ⟩ has the single sort 𝑠𝑞 , 𝑇𝑠𝑞 = 1. Then 𝐽𝑠𝑞 |𝜓 ⟩ C = 𝐽𝑠𝑞 |(𝑐 𝐴 , 𝑐 𝐵 )⟩ = |𝑐 𝐴 ⟩ ⊗ |𝑐 𝐵 ⟩ = |𝜓 ⟩ A⊗ B . Consequently, Equation (33) holds. (2) Let 𝑈 ∈ U be a quantum gate symbol. It suffices to consider the following cases. • Suppose 𝑈 = pre𝑂 or 𝑈 = post𝑂 for some nonconstant operation symbol 𝑂. This case is trivial because pre𝑂D = post𝑂D = 1 for D ∈ {A, B, C}, and Equation (38) further implies that pre𝑂A⊗ B = post𝑂A⊗ B = 1. Therefore, Equation (34) holds in both cases. • Suppose 𝑈 = 𝑈𝑂 for some nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠. Let us denote 𝑎 = 𝑎 1, . . . , 𝑎𝑛 , 𝑏 = 𝑏 1, . . . , 𝑏𝑛 , and (𝑎, 𝑏) = (𝑎 1, 𝑏 1 ), . . . , (𝑎𝑛 , 𝑏𝑛 ). For 𝑎𝑖 ∈ 𝐴𝑠𝑖 , 𝑏𝑖 ∈ 𝐵𝑠𝑖 , 𝑎 ∈ 𝐴𝑠 , and 𝑏 ∈ 𝐵𝑠 , we have (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 )𝑈𝑂C |(𝑎, 𝑏)⟩ |(𝑎, 𝑏)⟩ = (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) |(𝑎, 𝑏)⟩ |(𝑎, 𝑏) ⊞𝐶𝑠 𝑂 𝐶 ((𝑎, 𝑏))⟩ 𝑛   Ì = (|𝑎𝑖 ⟩ ⊗ |𝑏𝑖 ⟩) ⊗ |𝑎 ⊞𝑠𝐴 𝑂 𝐴 (𝑎)⟩ ⊗ |𝑏 ⊞𝑠𝐵 𝑂 𝐵 (𝑏)⟩ 𝑖=1

  B A = 𝑇𝑠−1 |𝑎⟩ ⊗ 𝑈 |𝑏⟩ |𝑏⟩ 𝑈 |𝑎⟩ ,...,𝑠 ,𝑠 𝑂 𝑂 1𝑞 𝑛𝑞 𝑞 = 𝑈𝑂A⊗ B (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) |(𝑎, 𝑏)⟩ |(𝑎, 𝑏)⟩ . Here, the first equality follows from Equation (7); the second follows from Equations (36), (40) and (41); the third follows from Equations (7) and (37); and the last follows from Equations (37) and (38). By linearity, Equation (34) holds. Thus, 𝐽 satisfies Definition 7.2 and is an isomorphism from C to A ⊗ B.

□

Proof of Proposition 8.4. As shown in the proof of Proposition 8.3, Equation (33) holds. It remains to verify Equation (34) for every 𝑈 ∈ U through the following cases. • Suppose that 𝑈 = pre𝑂 or 𝑈 = post𝑂 for some nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠. Equation (42) implies that for each sort 𝑠 ∈ 𝑆,   𝐽𝑠𝑞 QFT |𝐶𝑠 | = QFT |𝐴𝑠 | ⊗ QFT |𝐵𝑠 | 𝐽𝑠𝑞 . (54) Consequently, (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 )pre𝑂C = (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) (1𝑠1𝑞 ,...,𝑠𝑛𝑞 ⊗ QFT |𝐶𝑠 | )   = (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ) ⊗ (QFT |𝐴𝑠 | ⊗ QFT |𝐵𝑠 | ) 𝐽𝑠𝑞 = 𝑇𝑠−1 (pre𝑂A ⊗ pre𝑂B )𝑇𝑠1𝑞 ,...,𝑠𝑛𝑞 ,𝑠𝑞 (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) 1𝑞 ,...,𝑠𝑛𝑞 ,𝑠𝑞 = pre𝑂A⊗ B (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ), where the second equality uses Equation (54), the third follows from Equation (37), and the final follows from Equation (38). Combining the above together, Equation (34) holds for 𝑈 = pre𝑂 . Taking adjoints proves it for 𝑈 = post𝑂 .

Quantisation of Abstract Data Types

37

• Suppose 𝑈 = 𝑈𝑂 for some nonconstant operation symbol 𝑂 : 𝑠 1, . . . , 𝑠𝑛 → 𝑠. Write 𝑎 = 𝑎 1, . . . , 𝑎𝑛 , 𝑏 = 𝑏 1, . . . , 𝑏𝑛 , and (𝑎, 𝑏) = (𝑎 1, 𝑏 1 ), . . . , (𝑎𝑛 , 𝑏𝑛 ). For 𝑎𝑖 ∈ 𝐴𝑠𝑖 , 𝑏𝑖 ∈ 𝐵𝑠𝑖 , 𝑎 ∈ 𝐴𝑠 , and 𝑏 ∈ 𝐵𝑠 , let 𝑎 ′ = 𝑂 𝐴 (𝑎) and 𝑏 ′ = 𝑂 𝐵 (𝑏). By Equation (36), 𝑂 𝐶 ((𝑎, 𝑏)) = (𝑎 ′, 𝑏 ′ ). Then we have (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 )𝑈𝑂C |(𝑎, 𝑏)⟩ |(𝑎, 𝑏)⟩   2𝜋𝑖 𝑘𝑠𝐶 ((𝑎, 𝑏))𝑘𝑠𝐶 ((𝑎 ′, 𝑏 ′ )) = exp (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) |(𝑎, 𝑏)⟩ |(𝑎, 𝑏)⟩ |𝐶𝑠 |     2𝜋𝑖 𝑘𝑠𝐴 (𝑎)𝑘𝑠𝐴 (𝑎 ′ ) 2𝜋𝑖 𝑘𝑠𝐵 (𝑏)𝑘𝑠𝐵 (𝑏 ′ ) = exp exp (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) |(𝑎, 𝑏)⟩ |(𝑎, 𝑏)⟩ |𝐴𝑠 | |𝐵𝑠 | = 𝑈𝑂A⊗ B (𝐽𝑠1𝑞 ⊗ . . . ⊗ 𝐽𝑠𝑛𝑞 ⊗ 𝐽𝑠𝑞 ) |(𝑎, 𝑏)⟩ |(𝑎, 𝑏)⟩ . Here, the first equality follows from Equation (9); the second follows from Equation (42); and the last follows from Equations (9) and (38). By linearity, Equation (34) holds. Thus, 𝐽 satisfies Definition 7.2 and is an isomorphism from C to A ⊗ B. □

Related documents

• Mysterious Quantifiers#693339
• Abstract Syntax Notation X (ASN.X)#449139
• What do quantifier particles do?#771964
• Quantized mereology#973395
• YANG Data Types and Groupings for Cryptography#134745