Typed Quantum Circuits and Proto-Quipper-M

Prerequisites. Direct starred prerequisites: Chapter 184. No later core chapter depends on this route.

A program of the quantum lambda calculus of chapter 184 owns quantum data. Its configuration $[Q,L,M]$ contains a register, and reducing the term changes that register. Suppose instead we want a program that describes a circuit: a value that can be stored, printed, applied twice, or transformed, without executing anything. The first attempt is to write a function that produces a term, but the calculus of chapter 184 has no type of circuits. The only way to apply a gate there is to reduce a configuration, and the result is a changed register rather than a description.

The obstruction sharpens once the description is parameterized. Consider the family $${\mathrm{rep}}_n:=\text{“apply the gate }H\text{ to the wire }n\text{ times”},$$ whose size is selected by a classical natural number. Two facts must hold simultaneously: $n$ may be inspected, duplicated, and compared, since it controls a recursion; and the wire may not be duplicated, by theorem 184.4. A single linear context cannot carry both. Typing $n$ linearly forbids the recursion that reads it twice — once for the test and once for the recursive call — while typing the wire duplicably reintroduces cloning.

The calculus of this chapter resolves this by splitting the judgment: one context of parameters, available at circuit-generation time and freely duplicable, and one context of states, the wires, which are linear. The splitting is not a convention imposed on the programmer; it is forced by the two requirements just displayed, and every construct of the language is placed on one side of it.

Parameters and states

The three grammars encode the split. A value of parameter type exists at generation time and may be duplicated; a value of simple type is a bundle of wires in the circuit being built; and $\mathrm{Circ}(T,U)$, itself a parameter type, is the type of a completed circuit from interface $T$ to interface $U$ — a description, duplicable precisely because it is not a wire.

Nothing about quantum mechanics has been used. $\mathcal{M}$ is an arbitrary symmetric monoidal category, and a “circuit” is a morphism in it; the quantum instance is one choice among many, and it is deferred to section 185.4 so that the theorems below are visibly independent of it.

Boxing and unboxing

The phase distinction determines two operations. A circuit is built by running a function on fresh wires and recording what happened; that is boxing. A recorded circuit is inserted into the circuit under construction; that is application.

Three side conditions carry the discipline, and each is visible in the rules. The argument of $\mathsf{box}$ is typed in an empty label context, so a circuit description may not capture a wire of the surrounding circuit; that is the exact prohibition that makes $\mathrm{Circ}(T,U)$ a parameter type. The argument is also duplicable, of type $!(T⊸U)$, so that boxing may run it on freshly generated labels. And $\mathsf{apply}$ splits the label context, so that the wires fed to a circuit are not also used elsewhere.

Safety and soundness

The definition says exactly which wires belong to whom: the circuit built so far consumes the input labels and produces $Q^{″}\cup Q^{\prime }$, of which the term owns $Q^{″}$ and the environment owns $Q^{\prime }$.

Clauses (i)–(v) are Propositions 5.2, 5.3, 5.4, 5.6, and 5.7 of Rios and Selinger, A Categorical Model for a Quantum Circuit Description Language, arXiv:1706.02630, which states them and omits their proofs. The proofs are in Rios’s thesis, On a Categorically Sound Quantum Programming Language for Circuit Description, Dalhousie University, 2021, where subject reduction is Theorem 6.4.2, error freeness is Theorem 6.5.1, and soundness is Theorem 9.2.1, the last proved by rule induction over the evaluation relation with the cases grouped as axioms, inductive rules, substitution rules, and circuit rules. This book imports the five statements at exactly the signature displayed above, with the thesis as the proof owner; the extended abstract alone does not discharge them, and no statement here is inferred from the implementations named in section 185.4.

Proof of Lemma 185.10 — The boxing case of soundness

Proof. Both sides have the form $[[C]]$ followed by $[[N]]\otimes \mathrm{id}$ for the respective terms $N$, and $C$ is unchanged by the boxing rule, so it suffices to prove $[[{\mathsf{box}}_{T}M]]=[[(\overrightarrow{\ell },D,V)]]$ as morphisms $I\to [[\mathrm{Circ}(T,U)]]$. By definition 185.4 the left side is the name in ${\mathcal{M}}_{\mathcal{L}}$ of the morphism $[[T]]\to [[U]]$ determined by $M$; by definition 185.5 the right side is the name of the morphism recorded by $D$ together with the output labels named by $V$. The hypothesis $({\mathrm{id}}_Q,(\mathsf{force}M)\overrightarrow{\ell })\Downarrow (D,V)$ and clause (iv) of theorem 185.9 applied to that smaller configuration — whose starting circuit is the identity — give $[[({\mathrm{id}}_Q,(\mathsf{force}M)\overrightarrow{\ell })]]=[[(D,V)]]$, and the left side of that equation is exactly the morphism named by $[[{\mathsf{box}}_{T}M]]$. Taking names of equal morphisms gives the claim. ◻

Lemma 185.10 is not an independent proof of clause (iv): it uses that clause at a smaller configuration. It is written out because it exhibits the mechanism — boxing is the name of a morphism, and generation computes that morphism — which the statement of the theorem does not display.

The generic theorem and its quantum instance

Every statement above holds for an arbitrary symmetric monoidal category $\mathcal{M}$ with a chosen interpretation of wire constants. The quantum instance is obtained by choosing $\mathcal{M}$ to be a category of quantum circuits: objects are finite tensors of wire types, and morphisms are circuits built from a fixed gate set, composed and tensored, taken up to the equations of the chosen circuit formalism. Nothing in theorem 185.9 changes; what changes is what a generated value means.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 185.3, then exercise 185.4; the implementation project exercise 185.6 may be attempted at any time.

Exercise 185.3¶

★★☆ Let $$\mathrm{swapbox}:={\mathsf{box}}_{\alpha \otimes \alpha }(\mathsf{lift}(\lambda p^{\alpha \otimes \alpha }.\mathsf{let}⟨u,v⟩=p\mathsf{in}⟨v,u⟩)).$$ Derive its type, compute the generated circuit and its labelled interface, and then compute the circuit generated by the term that applies $\mathrm{swapbox}$ twice to a pair $p$. State which equation of definition 184.25 makes the second circuit equal to the identity in $\mathcal{M}$, and whether the two generated circuits are equal as data.

Referenced from 4 locations

• Typed Quantum Circuits and Proto-Quipper-M

Exercise 185.4¶

★★☆ Locate the parameter/state violation in each of the three terms $${\mathsf{box}}_{\alpha }(\mathsf{lift}(\lambda w^{\alpha }.⟨w,w⟩)),\lambda w^{\alpha }.\mathsf{lift}w,\lambda n^{\mathsf{nat}}.\mathsf{apply}(n,n),$$ naming for each the rule of definition 185.4 or definition 185.1 that fails.

Referenced from 3 locations

• Typed Quantum Circuits and Proto-Quipper-M

Exercise 185.5¶

★★☆ Compare $\mathrm{repbox}3$ of example 185.6 with the term of chapter 184 that applies $H$ three times to a qubit of a register. Say precisely what each one produces, what each one consumes, and why the first may be used twice while the second may not.

Referenced from 2 locations

• Typed Quantum Circuits and Proto-Quipper-M

Exercise 185.6¶

★★★ Practical project.typed-circuit-builder Implement in Agda or Kappa a typed circuit builder for the fragment of definition 185.1, definition 185.2 containing labels, pairs, linear abstraction, $\mathsf{lift}$, $\mathsf{force}$, $\mathsf{box}$, $\mathsf{apply}$, and natural-number recursion at parameter types. Represent a circuit as a list of gate applications on labels together with input and output label tuples; represent typing contexts as a parameter context and a label context, and enforce that the label context is split at every binary rule and empty at every $\mathsf{box}$.

The invariant to maintain is the one displayed after definition 185.4: the body of a $\mathsf{box}$ is typed in an empty label context, and no label occurs twice in the two halves of any context split. The concrete result is a function taking a closed term of type $\mathrm{Circ}(T,U)$ and returning the generated circuit together with its input and output label tuples.

Acceptance test. Golden generated circuits: $\mathrm{repbox}n$ for $n\in \{0,1,3\}$ produces circuits with $0$, $1$, and $3$ gate applications and in every case the interface $({\ell }_0:\alpha )\to ({\ell }_n:\alpha )$; $\mathrm{swapbox}$ of exercise 185.3 produces a circuit whose output tuple is the reverse of its input tuple; the term of example 185.7 is rejected, with the checker naming the empty-label- context premise; and ${\mathsf{box}}_{\alpha }(\mathsf{lift}(\lambda w^{\alpha }.⟨w,w⟩))$ is rejected, with the checker naming the context split. A mutation that types the body of $\mathsf{box}$ in the ambient label context must accept the term of example 185.7 and then produce a generated circuit whose input tuple does not match its declared interface, which the invariant check must report.

The program builds finite circuits over a fixed gate set. It illustrates theorem 185.9 and proves no clause of it, and a golden circuit is evidence about one input only.

Referenced from 3 locations

• Typed Quantum Circuits and Proto-Quipper-M

Bibliographic notes