Sized Types for low-level Quantum Metaprogramming

TL;DR

This paper introduces metaQASM, a typed extension of openQASM that enables safe, static metaprogramming of quantum circuit families with size-parametrized registers, ensuring finite circuit generation.

Contribution

It presents a novel sized type system for quantum programming languages, supporting subtyping and guaranteeing strong normalization for circuit family metaprogramming.

Findings

Supports subtyping over register sizes

Ensures all well-typed programs are strongly normalizing

Enables static unrolling of circuit families

Abstract

One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, an ability which is of particular importance in the context of quantum computing as algorithms frequently use arithmetic over non-standard word lengths. In this work, we introduce metaQASM, a typed extension of the openQASM language supporting the metaprogramming of circuit families. Our language and type system, built around a lightweight implementation of sized types, supports subtyping over register sizes and is moreover type-safe. In particular, we prove that our system is strongly normalizing, and as such any well-typed metaQASM program can be statically unrolled into a finite circuit.

Equations

$$|\psi ⟩=\sum _{\mathbf{x}\in {\mathbb{F}}_2^n}{\alpha }_{\mathbf{x}}|\mathbf{x}⟩,$$

$$\mathrm{CNOT}|x⟩|y⟩=|x⟩|x\oplus y⟩,T|x⟩=e^{\frac{2\pi i}{8}x}|x⟩,$$

$$H|x⟩=\frac{1}{\sqrt{2}}\sum _{x^{\prime }\in \{0,1\}}(-1{)}^{x\cdot x^{\prime }}|x^{\prime }⟩.$$

$$H_l|\psi ⟩=(I^{\otimes l-1}\otimes H\otimes I^{\otimes n-l})|\psi ⟩$$

$$\text{inference}x\in \text{dom}(\sigma )⟨x,\sigma ,\eta ,|\psi ⟩⟩\Downarrow \sigma (x)\text{inference}⟨x,\sigma ,\eta ,|\psi ⟩⟩\Downarrow (l_0,\dots ,l_{I^{\prime }})I\le I^{\prime }⟨x[I],\sigma ,\eta ,|\psi ⟩⟩\Downarrow l_I$$

$$\text{inference}⊢\cdot :\cdot \text{inference}⊢\sigma :\Gamma ⊢\sigma [x\leftarrow (l_0,\dots ,l_{I-1})]:\Gamma ,x:\beta [I]$$

$$\text{inference}⊢\sigma :\Gamma \Gamma ,x_1:{\tau }_1,\dots ,x_n:{\tau }_n⊢U:\text{Unit}⊢\sigma [x\leftarrow \lambda x_1:{\tau }_1,\dots ,x_n:{\tau }_n.U]:\Gamma ,x:\text{Circuit(τ1,…,τn)}$$

$$\text{inference}x:\tau \in \Gamma \Gamma ⊢x:\tau \text{inference}\Gamma ⊢x:\beta [I^{\prime }]I\le I^{\prime }-1\Gamma ⊢x[I]:\beta \text{inference}\Gamma ⊢E:\beta [I^{\prime }]I\le I^{\prime }\Gamma ⊢E:\beta [I]$$

$$\text{inference}\Gamma ,x:\text{Bit}[I]⊢C:\text{Unit}\Gamma ⊢\text{creg x[I] in { C }}:\text{Unit}\text{inference}\Gamma ,x:\text{Qbit}[I]⊢C:\text{Unit}\Gamma ⊢\text{qreg x[I] in { C }}:\text{Unit}$$

$$\text{inference}\Gamma ,x_1:{\tau }_1,\dots ,x_n:{\tau }_n⊢U:\text{Unit}\Gamma ,x:\text{Circuit(τ1,…,τn)}⊢C:\text{Unit}\Gamma ⊢\text{gate x(x1:τ1,…,xn:τn) { U } in { C }}:\text{Unit}$$

$$\text{inference}\Gamma ⊢E_1:\text{Qbit}\Gamma ⊢E_2:\text{Bit}\Gamma ⊢\text{measure E1 -> E2}:\text{Unit}\text{inference}\Gamma ⊢E:\text{Qbit}\Gamma ⊢\text{reset E}:\text{Unit}$$

$$\text{inference}\Gamma ⊢E:\text{Bit}\Gamma ⊢U:\text{Unit}\Gamma ⊢\text{if(E==I) { U }}:\text{Unit}\text{inference}\Gamma ⊢C_1:\text{Unit}\Gamma ⊢C_2:\text{Unit}\Gamma ⊢\text{C1; C2}:\text{Unit}$$

$$C=\text{gate x(x1:τ1,…,xn:τn) { U } in { C }}$$

$$⟨\text{gate x(x1:τ1,…,xn:τn) { U }},\sigma ,\eta ,|\psi ⟩⟩\Downarrow ⟨\sigma [x\leftarrow \lambda x_1,\dots ,x_n.U],\eta ,|\psi ⟩⟩.$$

$$⊢\sigma [x\leftarrow \lambda x_1:{\tau }_1,\dots ,x_n:{\tau }_n.U]:\Gamma ,x:\text{Circuit(τ1,…,τn)},$$

$$⟨C,\varnothing ,\lambda l.0,|00\cdots ⟩⟩\Downarrow ⟨\sigma ,\eta ,|\psi ⟩⟩.$$

$$(y_1,\dots ,y_m)$$

$$\text{inference}⟨\text{U},\sigma ,\eta ,|{\psi }^{\prime }⟩⟩\Downarrow |\psi ⟩⟨\text{reverse U},\sigma ,\eta ,|\psi ⟩⟩\Downarrow |{\psi }^{\prime }⟩$$

$$\text{inference}⟨i,\sigma ,\eta ,|\psi ⟩⟩\Downarrow i\text{inference}⟨I_1,\sigma ,\eta ,|\psi ⟩⟩\Downarrow i_1⟨I_2,\sigma ,\eta ,|\psi ⟩⟩\Downarrow i_2\star \in \{+,-,\cdot \}⟨I_1\star I_2,\sigma ,\eta ,|\psi ⟩⟩\Downarrow i_1\star i_2$$

$$\text{inference}⟨E,\sigma ,\eta ,|\psi ⟩\Downarrow \Pi y_1,\dots ,y_m.\lambda x_1:{\tau }_1,\dots ,x_n:{\tau }_n.U⟨\text{instance(I1,…,Im) E},\sigma ,\eta ,|\psi ⟩\Downarrow (\lambda x_1:{\tau }_1,\dots ,x_n:{\tau }_n.U)\{I_1/y_1,\dots ,I_m/y_m\}$$

$$\text{inference}⟨C,\sigma [x\leftarrow \Pi y_1,\dots ,y_m.\lambda x_1:{\tau }_1,\dots ,x_n:{\tau }_n.U],\eta ,|\psi ⟩⟩\Downarrow ⟨{\sigma }^{\prime },{\eta }^{\prime },|{\psi }^{\prime }⟩⟩⟨\text{family(y1,…,ym) x(x1:τ1,…,xn:τn) { U } in { C }},\sigma ,\eta ,|\psi ⟩⟩\Downarrow ⟨\sigma ,{\eta }^{\prime },|{\psi }^{\prime }⟩⟩$$

$$\Delta ⊢\tau ::\ast$$

$$v=\Pi y_1,\dots ,y_m.\lambda x_1:{\tau }_1,\dots ,x_n:{\tau }_n.U.$$

$$C=\text{family(y1,…,ym) x(x1:τ1,…,xn:τn) { U } in { C }}.$$

$$⟨C,\varnothing ,\lambda l.0,|00\cdots ⟩⟩\Downarrow ⟨\sigma ,\eta ,|\psi ⟩⟩.$$

Full text

Metaprogramming.

1 Introduction

Quantum computers have the potential to solve a number of important problems, including integer factorization [29], quantum simulation [23], approximating the Jones polynomial [1] and unstructured searching [12] asymptotically faster than the best known classical algorithms. These algorithms are typically described abstractly and make heavy use of classical arithmetic such as modular exponentiation. To make such algorithms concrete, efficient, reversible implementations of large swaths of a classical arithmetic and computation is needed – moreover, due to the limited space constraints and special-purpose nature of quantum circuits, these operations are typically needed in a multitude of bit sizes.

In part due to the increasing viability of quantum computing and the scaling of NISQ [28] devices, there has been a recent explosion in quantum programming tools. Such tools range from software development kits (e.g., Qiskit [5], ProjectQ [32], Strawberry Fields [19], Pyquil [30]) to Embedded domain-specific languages (e.g., Quipper [11], Qwire [27], $Q|SI\rangle$ [22]) and standalone languages and compilers (e.g., QCL [26], QML [2], ScaffCC [16], Q# [33]). Going beyond strict programming tools, software for the synthesis, optimization, and simulation of quantum circuits and programs (e.g., Revkit [31], TOpt [15], Feynman [3], PyZX [20], Quantum++ [9], QX [17]) are becoming more and more abundant.

The proliferation of both hardware and software tools for quantum computing has in turn spurred a need for standardization and portability [14, 24]. One such standard which has recently grown in popularity is the Quantum Assembly Language and its many various dialects (e.g., openQASM [6], QASM-HL [16], cQASM [18]). As a lightweight, modular language for specifying simple quantum circuits, programs with a well-defined syntax, QASM support – in particular, for the openQASM dialect – has been built-in to an increasingly large number of software tools, particularly standalone programs like circuit optimizers, as a way to support interoperability.

One feature that is noticeably lacking in these dialects is the ability to define families of quantum circuits parametrized over different register sizes, and by extension to generate concrete instances. This creates a barrier for the use of QASM in writing portable libraries of quantum circuit families, particularly for classical operations such as arithmetic. As a result, software designers typically end up re-implementing code – typically implemented in the host language for EDSLs, and hence not easily re-usable – for generating instances of simple operations such as adders and multipliers. Alternatively, programmers resort to using other compilers such as Quipper, Q# or ReVerC [4] to generate individual instances, which complicates the compilation or simulation process. While recent progress towards the development of portable libraries of circuit families with high-level non-embedded languages, standardization remains an on-going process, and moreover a low-level approach is preferable in many situations, including as compilation targets and middle-ends.

In this paper we make progress towards the design of a low-level language for quantum programming that supports the metaprogramming of sized circuit families. In particular, we develop a typed extension of the untyped open quantum assembly language (openQASM) with metaprogramming over lightweight sized types à la dependent ML [34]. Our language, metaQASM, is further shown to be type-safe and strongly-normalizing, while the non-meta fragment is both more expressive than openQASM and admits a simpler syntax, owing to the type system. For the purposes of this paper, we focus on the type system design and metatheory of such a language, leaving implementation to future work.

1.1 Quantum metaprogramming

Most QRAM-based quantum programming languages are metaprogramming languages – called circuit description languages – in that they typically operate by building quantum circuits to be sent in a single batch to a quantum processor. Such quantum circuits can typically be composed, reversed, and depend on the result of classical computations.

In this paper, we are interested in a particular type of quantum circuit metaprogramming, wherein circuit families are parametrized over shapes [11, 27], such as the number of input qubits. Existing languages offer varying support for such metaprogramming, either implicitly (e.g., uniform or transversal families of circuits in openQASM, iteration and qubit arrays in Q#), or more explicitly (e.g., the generic QData type-class in Quipper, which can be instantiated via explicit type applications). Our approach differs from previous attempts by explicitly parametrizing registers and circuit families with size parameters. We adopt a typed approach for a number of reasons:

• •

it allows the light-weight verification of libraries of circuit generators,

• •

it provides a means of self-documentation, and

• •

it allows explicit generation of sized-specialized instances.

The ability to generate instances of circuit families in various sizes without executing them is particularly important for the purposes of resource estimation, and for benchmarking tools that operate on fixed-size but arbitrary input circuits, such as circuit optimizers [14].

As an illustration, given an in-place family of adders written in the style of (imperative) Quipper with the type

inplace_add :: [Qubit] -> [Qubit] -> Circ (),

one may wish to generate a static, optimized instance of inplace_add operating on $2$-qubit registers, using an external circuit optimizer. Doing so requires the specialization to (and serialization of) a function

inplace_add2 :: (Qubit, Qubit) -> (Qubit, Qubit) -> Circ ().

One possible method of generating such a function is to write the body of inplace_add2 using a call to the generic inplace_add applied to the $4$ input qubits. However, this quickly gets unwieldy, both in the boilerplate code defining a particular instance, and in the large number of parameters.

A more common solution is to use dummy parameters, whereby the generic function is “applied” to lists of qubits, which are then taken by the serialization method as meaning arbitrary inputs. For instance, the following Quipper111The function inplace_add2 could instead be directly generated by writing the adder as inplace_add :: QData qa => qa -> qa -> Circ (), then specializing qa to the finite type (Qubit, Qubit) using type applications. However, the non-generic serialization functions in Quipper appear to work only for small finite tuple types. code [10] prints out a PDF representation of inplace_add2 using dummy parameters qubit :: Qubit

print_generic PDF inplace_add [qubit, qubit] [qubit, qubit].

The use of dummy parameters is partly a question of style, though it can cause problems when combining optimizations with initialized dummy parameters. In either case, the use explicitly sized circuit families carries further benefits to both readability and correctness [27].

1.2 Organization

The remainder of this paper is organized as follows. Section 2 gives a brief overview of quantum computing. Section 3 reviews the openQASM language and defines a formal semantics for it. Sections 4 and 5 extend openQASM with types and metaprogramming capabilities, and finally Section 6 concludes the paper.

2 Quantum computing

We give a brief overview of the basics of quantum computing. For a more in-depth introduction of quantum computation we direct the reader to [25], while an overview of quantum programming can be found in [8].

In the circuit model, the state of an $n$-qubit quantum system is described as a unit vector in a dimension $2^{n}$ complex vector space. The $2^{n}$ elementary basis vectors form the computational basis, and are denoted by $|\mathbf{x}\rangle$ for bit strings $\mathbf{x}\in\{0,1\}^{n}$ – these are called the classical states. A general quantum state may then be written as a superposition of classical states

[TABLE]

for complex $\alpha_{\mathbf{x}}$ and having unit norm. The states of two $n$ and $m$ qubit quantum systems $|\psi\rangle$ and $|\psi\rangle$ may be combined into an $n+m$ qubit state by taking their tensor product $|\psi\rangle\otimes|\psi\rangle$. If to the contrary the state of two qubits cannot be written as a tensor product the two qubits are said to be entangled.

Quantum circuits, in analogy to classical circuits, carry qubits from left to right along wires through gates which transform the state. In the unitary circuit model gates are required to implement unitary operators on the state space – that is, quantum gates are modelled by complex-valued matrices $U$ satisfying $UU^{\dagger}=U^{\dagger}U=I$, where $U^{\dagger}$ is the complex conjugate of $U$. As a result, unitary quantum computations must be reversible, and in particular the quantum circuits performing classical computations are precisely the set of reversible circuits.

The standard universal quantum gate set, known as Clifford+$T$, consists of the two-qubit controlled-NOT gate ($\mathrm{CNOT}$), and the single-qubit Hadamard ($H$) and $T$ gates. As quantum circuits implement linear operators, we may define the above three gates by their effect on classical states:

[TABLE]

[TABLE]

Figure 1 gives a pictorial representation of a quantum circuit over $\mathrm{CNOT}$, $H$, and $T$ gates. $\mathrm{CNOT}$ gates are written as a solid dot on their first argument and an exclusive-OR symbol ($\oplus$) on their second argument.

More general quantum operations include qubit initialization and measurement, which effectively convert between classical and quantum data. As neither operation is unitary and hence not (directly) reversible, we regard them as functions of the classical computer rather than gates in a quantum circuit.

3 openQASM

The open quantum assembly language (openQASM [6]) is a low-level, untyped imperative quantum programming language, developed as a dialect of the informal QASM language. One of the key additions of the openQASM language is that of modularity, in the form of a simple module and import system. As this work is largely concerned with the question of making this modularity more powerful – specifically, to support the modular definition of entire circuit families – we first give a brief overview of the openQASM language.

The official specification of openQASM can be found in [6]. Programs in openQASM are structured as sequences of declarations and commands. Programmers can declare statically-sized classical or quantum registers, define unitary circuits (called gates in openQASM), apply gates or circuits, measure or initialize qubits and condition commands on the value of classical bits. Gate arguments are restricted to individual qubits, where the application of gates to one or more register of the same size is syntactic sugar for the application of a single gate in parallel across the registers. The listing below gives an example of an openQASM program performing quantum teleportation:

⬇

OPENQASM 2.0;

qreg q[3];

creg c0[1];

creg c1[1];

h q[1];

cx q[1],q[2];

cx q[0],q[1];

h q[0];

measure q[0] -> c0[0];

measure q[1] -> c1[0];

if(c0==1) z q[2];

if(c1==1) x q[2];

We give a slightly different syntax from the above, and from the concrete syntax [6], as it will be more convenient and readable for our purposes. As is common in imperative languages, we leave some of the concrete syntactic classes of openQASM [6] separate in our formalization – since all operations in openQASM nominally have unit type, this allows terms with unitary and non-unitary effects to be distinguished, without relying on an effect system or monadic types. In particular, terms of the class $U$ of unitary statements represent computations with purely unitary effects, while commands $C$ may have non-unitary effects, such as measurement. Statements of the form

$E$($E_{1},\dots,E_{n}$)

represent the application of a unitary gate or named circuit $E$ to the (quantum) arguments $E_{1}$ through $E_{n}$. While the openQASM specification includes built-in cx (controlled-NOT) and parametrized single qubit gates U, we drop the parametrized U gate in favour of built-in Hadamard and $T/T^{\dagger}$ gates h and t/tdg, respectively.

The commands creg, qreg and gate declare classical registers, quantum registers, and unitary circuits, respectively. The if statement differs from the formal openQASM definition by testing the value of a single classical bit, rather than a classical register – this was done to simplify the semantics of the language. Locations $l$ and values $V$ do not appear directly in openQASM programs, but are used to define the semantics. In particular, values of the form $(l_{0},\dots,l_{I-1})$ denote registers and $\lambda x_{1},\dots,x_{n}.U$ denote unitary circuits. We leave out a number of features of openQASM which are orthogonal to the extensions we describe here, namely classical arithmetic and the barrier and opaque terms. We also write parentheses around arguments and parameters.

As no formal semantics of openQASM is given in [6], we define an operational semantics in Section 3. Our semantics is defined with respect to a configuration $\langle S,\sigma,\eta,|\psi\rangle\rangle$, which stores a term $S$ taken from some syntactic class (e.g., $C$, $U$, $E$), an environment $\sigma$ which maps variables to values, a classical heap $\eta$ storing the value of the classical bits, and a quantum state $|\psi\rangle$. Gates applied to qubit $l$ of a quantum state are written by added a subscript to the intended gate, e.g.,

[TABLE]

$\sigma[x\leftarrow v]$ denotes the environment mapping $x$ to $v$ or $\sigma(x)$ otherwise, and $S\{X/x\}$ denotes the substitution of $X$ for $x$ in $S$. We assume for convenience that no valid program will run out of classical memory or quantum bits. We say $\langle S,\sigma,\eta,|\psi\rangle\rangle\Downarrow v$ if $S$ reduces to $v$, where the form of $v$ depends on the syntactic class of $S$ – for instance, expressions evaluate to locations, arrays or circuits while commands produce a new environment, heap and quantum state. Note that we use a call-by-name evaluation strategy, as openQASM has only globally scoped variables.

Rather than give a full probabilistic reduction system to account for measurement probabilities, it suffices for our purposes to make the semantics non-deterministic. In particular, rules are given for both of the possible measurement outcomes in measure $E_{1}$ -> $E_{2}$, setting the classical bit to the result $c\in\{0,1\}$ and non-destructively applying the projector $P^{c}=|c\rangle\langle c|$ (appropriately normalized) to the measured qubit.