Chapter 184Optional

Quantum Lambda Calculi and Linear Quantum Data

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

In every calculus so far, a value may be named, used twice, and discarded: $let x = V in ⟨ x, x ⟩$ is a program. For a value that is a quantum bit, the first of those three operations is impossible. The impossibility is not a design decision about a language; it is a theorem about linear maps, proved in theorem 184.4 below, and any language whose values include quantum bits must either reject that program or be unsound with respect to the physics it claims to describe.

Rejecting it is not enough either. A quantum program measures, and measurement is probabilistic and changes the state that later computation reads; a term alone cannot carry that state, because two variables in different parts of a term may refer to entangled qubits whose joint state is not the pair of their separate states (lemma 184.3). So the calculus must be built on configurations that separate a classical term from a quantum store, its reduction must be probabilistic, and its type system must ensure that a well-typed configuration never asks for a duplicate of a stored qubit.

This chapter constructs the linear algebra that makes those requirements precise, fixes one calculus that meets them, and proves its safety theorem. The proof obligations are exactly two: that reduction preserves typing together with the store invariant, and that a well-typed configuration is never stuck in a way that would require an impossible physical operation. Both are proved. What is not proved — and is stated as such — is any claim that the categorical model developed at the end is adequate or fully abstract for this language.

The quantum minimum

Definition 184.1 — Qubits and registers ¶

Let $C^{2}$ have the standard basis written $| 0 ⟩, | 1 ⟩$ and the Hermitian inner product $⟨ ϕ ∣ ψ ⟩ : = \sum_{i} \overset{―}{ϕ_{i}} ψ_{i}$ . A qubit state is a unit vector $| ψ ⟩ = α | 0 ⟩ + β | 1 ⟩$ with $| α |^{2} + | β |^{2} = 1$ . An $n$ -qubit register state is a unit vector of $⨂_{i = 0}^{n - 1} C^{2} ≅ C^{2^{n}}$ , whose standard basis is written $| b_{0} \dots b_{n - 1} ⟩$ for $b_{i} \in {0, 1}$ . A linear map $U$ on a finite-dimensional inner-product space is unitary when $U^{†} U = id$ , where the adjoint $U^{†}$ is the unique linear map with $⟨ U^{†} ϕ ∣ ψ ⟩ = ⟨ ϕ ∣ U ψ ⟩$ for all $ϕ, ψ$ .

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Two physical assumptions are used below and are not derived: an isolated system evolves by a unitary map, and a measurement in the standard basis returns outcome $b$ with probability given by the Born rule of definition 184.5. Everything else in this section is linear algebra.

Example 184.2 — Two gates and a Bell state ¶

Let $H : = \frac{1}{\sqrt{2}} (\begin{matrix} 1 & 1 \\ 1 & - 1 \end{matrix})$ and let $CNOT$ act on $C^{2} \otimes C^{2}$ by $| b_{0} b_{1} ⟩ \mapsto | b_{0} (b_{0} \oplus b_{1}) ⟩$ . Both are unitary: $H^{†} = H$ and $H^{2} = id$ , while $CNOT$ permutes an orthonormal basis. Then $(H \otimes id) | 00 ⟩ = \frac{1}{\sqrt{2}} (| 0 ⟩ + | 1 ⟩) \otimes | 0 ⟩ = \frac{1}{\sqrt{2}} (| 00 ⟩ + | 10 ⟩),$ and applying $CNOT$ gives $| Φ^{+} ⟩ : = \frac{1}{\sqrt{2}} (| 00 ⟩ + | 11 ⟩)$ .

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Lemma 184.3 — The Bell state is entangled ¶

There are no $| ϕ ⟩, | χ ⟩ \in C^{2}$ with $| Φ^{+} ⟩ = | ϕ ⟩ \otimes | χ ⟩$ .

Referenced from 5 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Lemma 184.3 — The Bell state is entangled

Proof. Write $| ϕ ⟩ = a | 0 ⟩ + b | 1 ⟩$ and $| χ ⟩ = c | 0 ⟩ + d | 1 ⟩$ . Then $| ϕ ⟩ \otimes | χ ⟩ = a c | 00 ⟩ + a d | 01 ⟩ + b c | 10 ⟩ + b d | 11 ⟩$ , so equality with $| Φ^{+} ⟩$ requires $a c = \frac{1}{\sqrt{2}}, a d = 0, b c = 0, b d = \frac{1}{\sqrt{2}} .$ From $a c \neq 0$ we get $a \neq 0$ and $c \neq 0$ ; then $a d = 0$ gives $d = 0$ and $b c = 0$ gives $b = 0$ , whence $b d = 0 \neq \frac{1}{\sqrt{2}}$ . ◻

Lemma 184.3 is the reason a program state cannot store a qubit inside a term: the joint state of two qubits is not determined by two separate qubit expressions.

Theorem 184.4 — No cloning ¶

There is no linear map $U : C^{2} \otimes C^{2} \to C^{2} \otimes C^{2}$ such that $U (| ψ ⟩ \otimes | 0 ⟩) = | ψ ⟩ \otimes | ψ ⟩$ for every qubit state $| ψ ⟩$ .

Referenced from 6 locations

Proof of Theorem 184.4 — No cloning

Proof. Suppose $U$ is such a map. Taking $| ψ ⟩ = | 0 ⟩$ and $| ψ ⟩ = | 1 ⟩$ gives $U | 00 ⟩ = | 00 ⟩$ and $U | 10 ⟩ = | 11 ⟩$ . Taking $| + ⟩ : = \frac{1}{\sqrt{2}} (| 0 ⟩ + | 1 ⟩)$ and using linearity, $U (| + ⟩ \otimes | 0 ⟩) = \frac{1}{\sqrt{2}} (U | 00 ⟩ + U | 10 ⟩) = \frac{1}{\sqrt{2}} (| 00 ⟩ + | 11 ⟩),$ whereas the assumed property requires $| + ⟩ \otimes | + ⟩ = \frac{1}{2} (| 00 ⟩ + | 01 ⟩ + | 10 ⟩ + | 11 ⟩)$ . The coefficient of $| 01 ⟩$ is $0$ in the first and $\frac{1}{2}$ in the second. ◻

Only linearity was used: no unitarity, no norm, no physics. The theorem therefore constrains every calculus whose values may be arbitrary quantum states, independently of which gates it provides.

Definition 184.5 — Measurement ¶

Let $| Q ⟩$ be an $n$ -qubit state and $0 \leq i < n$ . Write $| Q ⟩ = α | Q_{0} ⟩ + β | Q_{1} ⟩$ , where $| Q_{b} ⟩$ is a normalized state in which the $i$ -th qubit is $| b ⟩$ and $| α |^{2} + | β |^{2} = 1$ ; this decomposition exists and is unique up to phase. Measuring the $i$ -th qubit in the standard basis yields outcome $0$ with probability $| α |^{2}$ and leaves the register in state $| Q_{0} ⟩$ , and outcome $1$ with probability $| β |^{2}$ , leaving $| Q_{1} ⟩$ .

Referenced from 6 locations

Quantum Lambda Calculi and Linear Quantum Data

Definition 184.6 — Density matrices and channels ¶

A density matrix on a finite-dimensional space $V$ is a positive semidefinite linear map $ρ : V \to V$ with $tr ρ = 1$ ; a pure state $| ψ ⟩$ corresponds to $ρ = | ψ ⟩ ⟨ ψ |$ . For a bipartite space $V \otimes W$ , the partial trace ${tr}_{W}$ is the unique linear map with ${tr}_{W} (A \otimes B) = tr (B) \cdot A$ . A channel is a completely positive trace-preserving linear map on density matrices.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Example 184.7 — Discarding is not an error ¶

Take $| Φ^{+} ⟩$ and discard the second qubit. With $ρ = | Φ^{+} ⟩ ⟨ Φ^{+} | = \frac{1}{2} (| 00 ⟩ ⟨ 00 | + | 00 ⟩ ⟨ 11 | + | 11 ⟩ ⟨ 00 | + | 11 ⟩ ⟨ 11 |)$ , the partial trace over the second factor kills the two cross terms, since $tr (| 0 ⟩ ⟨ 1 |) = 0$ , and gives ${tr}_{2} ρ = \frac{1}{2} | 0 ⟩ ⟨ 0 | + \frac{1}{2} | 1 ⟩ ⟨ 1 | = \frac{1}{2} id .$ The same matrix is obtained by measuring the first qubit of $| Φ^{+} ⟩$ and forgetting the outcome. Discarding a qubit is therefore a perfectly good operation — it is a channel — and it is not the operation forbidden by theorem 184.4. A type system for quantum data must forbid duplication; it need not forbid discarding, and the calculus fixed below does not.

Referenced from 8 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.1 ¶

★☆☆ Verify that $CNOT$ is unitary by exhibiting its matrix in the basis $| 00 ⟩, | 01 ⟩, | 10 ⟩, | 11 ⟩$ and computing ${CNOT}^{†} CNOT$ . Then compute $(id \otimes H) | Φ^{+} ⟩$ and say whether the result is entangled.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.2 ¶

★★☆ Show that theorem 184.4 still holds if $U$ is only required to satisfy $U (| ψ ⟩ \otimes | 0 ⟩) = e^{i θ (ψ)} | ψ ⟩ \otimes | ψ ⟩$ for some phase depending on $| ψ ⟩$ . Then show that a map cloning the two basis states alone does exist, and identify exactly which hypothesis the clone of $| + ⟩$ violates.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.3 ¶

★★☆ Measure the first qubit of $| Φ^{+} ⟩$ using definition 184.5: compute $α$ , $β$ , $| Q_{0} ⟩$ , $| Q_{1} ⟩$ , and the two probabilities, and then compute the state of the second qubit conditional on each outcome. Compare with example 184.7 and explain why the two calculations agree on the density matrix but differ in what an observer knows.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

A calculus with classical control

The calculus fixed for this chapter is that of Selinger and Valiron, A Lambda Calculus for Quantum Computation with Classical Control, arXiv cs/0404056. Its shape is forced by the previous section: a configuration carries a quantum register separately from the term, and the type system is affine linear.

Definition 184.8 — Terms, values, and program states ¶

Terms and values are $\begin{aligned} M, N ::= & x ∣ M N ∣ λ x . M ∣ ⟨ M, N ⟩ ∣ let ⟨ x_{1}, x_{2} ⟩ = M in N \\ ∣ & if M then N else P ∣ 0 ∣ 1 ∣ * ∣ meas ∣ new ∣ U, \\ V, W ::= & x ∣ λ x . M ∣ 0 ∣ 1 ∣ * ∣ meas ∣ new ∣ U ∣ ⟨ V, W ⟩, \end{aligned}$ where $U$ ranges over a set of built-in unitary gates, each with an arity. A program state is a triple $[Q, L, M]$ in which $Q$ is a normalized vector of $⨂_{i < n} C^{2}$ for some $n \geq 0$ , $M$ is a term, and $L$ is an injective linking function from a set of variables containing $FV (M)$ to ${0, \dots, n - 1}$ . We write $p_{i}$ for the variable $x$ with $L (x) = i$ and abbreviate $[Q, L, M]$ to $[Q, M]$ .

Referenced from 5 locations

Quantum Lambda Calculi and Linear Quantum Data

The linking function is the device that answers lemma 184.3: the term mentions names, the register holds one joint state, and the correspondence between them is explicit and injective.

Definition 184.9 — Probabilistic reduction ¶

Write $[Q, M] ⟶_{p} [Q^{'}, M^{'}]$ for a step taken with probability $p$ . The root rules are $\begin{aligned} [Q, (λ x . M) V] & ⟶_{1} [Q, M [V / x]], \\ [Q, let ⟨ x_{1}, x_{2} ⟩ = ⟨ V_{1}, V_{2} ⟩ in N] & ⟶_{1} [Q, N [V_{1} / x_{1}, V_{2} / x_{2}]], \\ [Q, if 0 then M else N] & ⟶_{1} [Q, N], \\ [Q, if 1 then M else N] & ⟶_{1} [Q, M], \\ [Q, U ⟨ p_{j_{1}}, \dots, p_{j_{n}} ⟩] & ⟶_{1} [Q^{'}, ⟨ p_{j_{1}}, \dots, p_{j_{n}} ⟩], \\ [Q, new b] & ⟶_{1} [Q \otimes | b ⟩, p_{n}], \\ [α Q_{0} + β Q_{1}, meas p_{i}] & ⟶_{| α |^{2}} [Q_{0}, 0], \\ [α Q_{0} + β Q_{1}, meas p_{i}] & ⟶_{| β |^{2}} [Q_{1}, 1], \end{aligned}$ where in the gate rule the indices $j_{1}, \dots, j_{n}$ are pairwise distinct and $Q^{'}$ is obtained from $Q$ by applying $U$ to those qubits, in the $new$ rule $Q$ has $n$ qubits so that $p_{n}$ names the new one, and in the measurement rules $Q_{0}, Q_{1}$ are the normalized states of definition 184.5 for the qubit named $p_{i}$ . These rules are closed under the left-to-right call-by-value evaluation contexts for application, pairing, $let$ , and $if$ .

Referenced from 5 locations

Quantum Lambda Calculi and Linear Quantum Data

Definition 184.10 — Types and subtyping ¶

Types are $A, B ::= α ∣ X ∣! A ∣ (A ⊸ B) ∣ ⊤ ∣ (A \otimes B),$ where $α$ ranges over the type constants $bit$ and $qbit$ and $X$ over type variables; $! A$ is the type of duplicable values. Subtyping $A <: B$ is generated by $α <: α, X <: X, ⊤ <: ⊤,$ $\frac{A <: B}{! A <: B}, \frac{! A <: B}{! A <:! B}, \frac{A <: A^{'} B <: B^{'}}{A^{'} ⊸ B <: A ⊸ B^{'}},$ $\frac{A_{1} <: B_{1} A_{2} <: B_{2}}{A_{1} \otimes A_{2} <: B_{1} \otimes B_{2}} .$

Referenced from 4 locations

Quantum Lambda Calculi and Linear Quantum Data

Definition 184.11 — Typing ¶

Judgments have the form $Δ ⊢ M : B$ with $Δ$ a function from variables to types. Writing $! Δ$ for a context all of whose types begin with $!$ , the rules are $\frac{A <: B}{Δ, x : A ⊢ x : B}, \frac{A_{c} <: B}{Δ ⊢ c : B},$ $\frac{Γ_{1},! Δ ⊢ M : A ⊸ B Γ_{2},! Δ ⊢ N : A}{Γ_{1}, Γ_{2},! Δ ⊢ M N : B},$ $\frac{x : A, Δ ⊢ M : B}{Δ ⊢ λ x . M : A ⊸ B}, \frac{Γ,! Δ, x : A ⊢ M : B FV (M) \cap | Γ | = \emptyset}{Γ,! Δ ⊢ λ x . M :!^{n + 1} (A ⊸ B)},$ $\frac{! Δ, Γ_{1} ⊢ M_{1} :!^{n} A_{1}! Δ, Γ_{2} ⊢ M_{2} :!^{n} A_{2}}{! Δ, Γ_{1}, Γ_{2} ⊢ ⟨ M_{1}, M_{2} ⟩ :!^{n} (A_{1} \otimes A_{2})}, \frac{}{Δ ⊢ * :!^{n} ⊤},$ $\frac{! Δ, Γ_{1} ⊢ M :!^{n} (A_{1} \otimes A_{2})! Δ, Γ_{2}, x_{1} :!^{n} A_{1}, x_{2} :!^{n} A_{2} ⊢ N : A}{! Δ, Γ_{1}, Γ_{2} ⊢ let ⟨ x_{1}, x_{2} ⟩ = M in N : A},$ $\frac{Γ_{1},! Δ ⊢ P : bit Γ_{2},! Δ ⊢ M : A Γ_{2},! Δ ⊢ N : A}{Γ_{1}, Γ_{2},! Δ ⊢ if P then M else N : A},$ with the constants typed by $\begin{aligned} A_{0} & = A_{1} =! bit, & A_{new} & =! (bit ⊸ qbit), \\ A_{meas} & =! (qbit ⊸! bit), & A_{U} & =! ({qbit}^{n} ⊸ {qbit}^{n}) . \end{aligned}$ A program state $[Q, L, M]$ is well typed of type $B$ , written $[Q, L, M] : B$ , when $Δ ⊢ M : B$ is derivable for $Δ = {x : qbit ∣ x \in FV (M)}$ .

Referenced from 10 locations

Quantum Lambda Calculi and Linear Quantum Data

Three features of definition 184.11 carry the whole discipline. Contexts are split in the binary rules, so a linear variable cannot be used twice. The duplicable part $! Δ$ is shared rather than split, so a duplicable value may be used any number of times. And the axiom permits an unused $Δ$ , so weakening is available: a value may be discarded, which by example 184.7 is the partial trace and not an error.

Example 184.12 — A derivation and a trace ¶

Let $M$ be the term $let ⟨ x, y ⟩ = ⟨ new 0, new 0 ⟩ in let ⟨ x^{'}, y^{'} ⟩ = CNOT ⟨ H x, y ⟩ in meas x^{'} .$ Typing: $new 0$ has type $qbit$ by the constant rule and application; the pair has type $qbit \otimes qbit$ with $n = 0$ ; the gate has type ${qbit}^{2} ⊸ {qbit}^{2}$ after one subtyping step; and $meas x^{'}$ has type $! bit$ . The two halves of the pair are typed in disjoint contexts, which is what prevents writing $⟨ x, x ⟩$ .

Reduction from the empty register: two $new$ steps give $[| 00 ⟩, \dots]$ with $x = p_{0}$ , $y = p_{1}$ ; the gate steps give $[| Φ^{+} ⟩, \dots]$ by example 184.2; and the measurement step gives $[| 00 ⟩, 0]$ with probability $\frac{1}{2}$ and $[| 11 ⟩, 1]$ with probability $\frac{1}{2}$ . The final configuration still holds one qubit, named by a variable that no longer occurs in the term; it has been discarded, and example 184.7 says what its state is.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Safety

Two properties are to be proved. Reduction must preserve typing, so that the discipline of definition 184.11 still holds after a step; and a well-typed configuration must never be stuck at a term that would require an impossible operation — a gate applied to a duplicated qubit name, or a gate applied to a function.

Definition 184.13 — Error state ¶

A program state $[Q, L, M]$ is an error state when $M$ is not a value and no reduction rule of definition 184.9 applies to it; the two cases to keep in mind are $[Q, U ⟨ p_{i}, p_{i} ⟩]$ , where the gate rule fails because the indices are not distinct, and $[Q, H (λ x . x)]$ , where no rule applies because the argument is not a qubit name.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Lemma 184.14 — Weakening and duplicable values ¶

If $x \notin FV (M)$ and $Δ, x : A ⊢ M : B$ , then $Δ ⊢ M : B$ .
If $V$ is a value and $Δ ⊢ V :! A$ , then for every $x \in FV (V)$ there is a type $C$ with $x :! C \in Δ$ .
If $A <:! B$ then $A =! C$ for some $C$ .

Referenced from 7 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Lemma 184.14 — Weakening and duplicable values

Proof. (iii) is an induction on the derivation of $A <:! B$ : the only rules whose conclusion has a $!$ on the right are the two rules for $!$ , and both have a $!$ on the left of the conclusion.

(i) Induction on the typing derivation. The context is only ever split or shared, never inspected, and every rule permits an arbitrary unused part of the context; the axiom permits it explicitly.

(ii) Induction on $V$ . If $V = x$ then the axiom gives $A^{'} <:! A$ for the declared type $A^{'}$ of $x$ , and (iii) gives $A^{'} =! C$ . If $V$ is an abstraction with type $! A$ , the only rule deriving a type beginning with $!$ for an abstraction is the second abstraction rule, whose conclusion requires all free variables of $V$ to be typed in $! Δ$ . The constants have closed types, and for a pair the introduction rule with $n \geq 1$ types both components in contexts whose shared part is $! Δ$ , so the induction hypothesis applies. ◻

Lemma 184.15 — Linear substitution ¶

Let $V$ be a value. If $Γ_{1},! Δ, x : A ⊢ M : B$ and $Γ_{2},! Δ ⊢ V : A$ , then $Γ_{1}, Γ_{2},! Δ ⊢ M [V / x] : B$ .

Referenced from 5 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Lemma 184.15 — Linear substitution

Proof. Induction on the derivation of $Γ_{1},! Δ, x : A ⊢ M : B$ , with the contexts $Γ_{1}, Γ_{2}$ tracked explicitly.

Axiom. If $M = x$ then $M [V / x] = V$ and $A <: B$ , so the conclusion follows from the derivation of $V$ by the subtyping in the axiom of definition 184.11. If $M = y \neq x$ then $M [V / x] = y$ , and lemma 184.14(i) discards the unused hypothesis on $x$ and adds the unused $Γ_{2}$ .

Application. Let $M = M_{1} M_{2}$ , typed from $Γ_{1}^{'},! Δ ⊢ M_{1} : A^{'} ⊸ B$ and $Γ_{1}^{″},! Δ ⊢ M_{2} : A^{'}$ with $Γ_{1} = Γ_{1}^{'}, Γ_{1}^{″}$ . The variable $x$ occurs in exactly one of the two subcontexts, since contexts are split; say in $Γ_{1}^{'}$ . The induction hypothesis substitutes into $M_{1}$ using $Γ_{2}$ , and $M_{2} [V / x] = M_{2}$ because $x \notin FV (M_{2})$ . Reassembling with the application rule gives the conclusion. If instead $x : A$ lies in the shared part, then $A =! C$ ; then $V$ is typed in $Γ_{2},! Δ$ with $Γ_{2}$ consisting of duplicable types by lemma 184.14(ii), so $Γ_{2}$ may be shared between the two premises, and the induction hypothesis applies to both.

Abstraction. For the linear rule, the induction hypothesis applies to the body. For the duplicable rule, its side condition $FV (M) \cap | Γ | = \emptyset$ is preserved because $FV (M [V / x]) \subseteq (FV (M) ∖ {x}) \cup FV (V)$ and the free variables of $V$ are duplicable by lemma 184.14(ii).

Pairing, $let$ , and $if$ . Each is a splitting rule and is treated exactly as the application case, with the same distinction between $x$ occurring in a split part and $x$ occurring in the shared duplicable part. ◻

Theorem 184.16 — Subject reduction ¶

If $[Q, L, M] : B$ and $[Q, L, M] ⟶_{p} [Q^{'}, L^{'}, M^{'}]$ with $p > 0$ , then $[Q^{'}, L^{'}, M^{'}] : B$ .

Referenced from 7 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Theorem 184.16 — Subject reduction

Proof. Induction on the derivation of the reduction step. The contextual cases follow from the induction hypothesis, because each evaluation context is built by a typing rule whose other premises are unchanged. For the root rules:

Beta and $let$ use lemma 184.15, the substituted terms being values.

Conditional discards one branch; both branches were typed at $B$ in the same context, and lemma 184.14(i) discards the context used for the guard.

Gate. The term $U ⟨ p_{j_{1}}, \dots, p_{j_{n}} ⟩$ has type ${qbit}^{n}$ , and so does the resulting tuple of names; the register changes but $L$ and the set of free variables do not, so the typing context $Δ = {x : qbit}$ is unchanged.

New. The term $new b$ has type $qbit$ , and the result $p_{n}$ has type $qbit$ in the extended context; $L^{'}$ extends $L$ injectively by $p_{n} \mapsto n$ , so the invariant that free variables are linked injectively into the register is preserved.

Measurement. The term $meas p_{i}$ has type $! bit$ and the results $0$ and $1$ have type $! bit$ by the constant rule. The variable $p_{i}$ disappears from the term, and $L^{'}$ is $L$ restricted accordingly; the register loses no qubit, so the linking function remains injective into ${0, \dots, n - 1}$ . ◻

Lemma 184.17 — Shape of values ¶

Let $Δ = x_{1} : qbit, \dots, x_{n} : qbit$ and let $V$ be a value. If $Δ ⊢ V : A ⊸ B$ then $V$ is $new$ , $meas$ , a gate $U$ , or an abstraction. If $Δ ⊢ V : A \otimes B$ then $V = ⟨ V_{1}, V_{2} ⟩$ . If $Δ ⊢ V : bit$ then $V \in {0, 1}$ .

Referenced from 6 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Lemma 184.17 — Shape of values

Proof. By inspection of the rules that can conclude a judgment for a value in such a context, together with definition 184.10: a variable in $Δ$ has type $qbit$ , and $qbit <: A ⊸ B$ , $qbit <: A \otimes B$ , and $qbit <: bit$ all fail, since subtyping relates a type constant only to itself. The remaining values are the listed ones. ◻

Theorem 184.18 — Progress and safety ¶

Let $[Q, L, M] : B$ . Then $[Q, L, M]$ is not an error state. Either $M$ is a value, or there is a state $[Q^{'}, L^{'}, M^{'}]$ with $[Q, L, M] ⟶_{p} [Q^{'}, L^{'}, M^{'}]$ ; and in the second case the probabilities of all single-step reductions from $[Q, L, M]$ sum to $1$ .

Referenced from 12 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Theorem 184.18 — Progress and safety

Proof. Induction on $M$ . If $M$ is a value there is nothing to prove. Otherwise $M$ has one of the forms $P N$ , $N V$ , $⟨ N, P ⟩$ , $⟨ V, N ⟩$ , $if N then P else R$ , or $let ⟨ x, y ⟩ = N in P$ with $N$ not a value, in which case the induction hypothesis applies to $N$ — whose free variables are still all of type $qbit$ — and the corresponding evaluation-context rule lifts its reductions, preserving the total probability $1$ .

The remaining cases are redexes. For $V W$ with both parts values, lemma 184.17 says that $V$ is $new$ , $meas$ , a gate, or an abstraction. For an abstraction the beta rule applies with probability $1$ . For $new$ the argument has type $bit$ , so it is $0$ or $1$ by lemma 184.17, and the $new$ rule applies. For $meas$ the argument has type $qbit$ ; a value of that type in this context is a variable, hence some $p_{i}$ , and the two measurement rules apply with probabilities summing to $| α |^{2} + | β |^{2} = 1$ . For a gate $U$ of arity $n$ the argument has type ${qbit}^{n}$ , so by lemma 184.17 it is a tuple of values of type $qbit$ , hence a tuple of names $p_{j_{1}}, \dots, p_{j_{n}}$ ; these are pairwise distinct because the tuple was typed by the pairing rule, which splits the context, so no variable occurs in two components, and $L$ is injective. Hence the gate rule applies.

In every case a rule applies, so $[Q, L, M]$ is not an error state. ◻

Corollary 184.19 — What the type system establishes ¶

For a well-typed program state, no reduction sequence reaches a configuration in which a gate is applied to two occurrences of one qubit name or to a non-qubit, and every maximal reduction sequence either converges to a value or is infinite.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Corollary 184.19 — What the type system establishes

Proof. The first claim is theorem 184.16 followed by theorem 184.18 at each step. The second is the same statement read as a dichotomy: by progress, a well-typed non-value always reduces. ◻

Remark 184.20 — Exactly what is and is not forbidden ¶

The system is affine: contexts are split in binary rules, so no linear variable is used twice, but the axiom allows unused hypotheses, so a variable may be used zero times. Duplication is therefore rejected — the term $λ x . ⟨ x, x ⟩$ has no type with $x : qbit$ , since the pairing rule would have to place $x$ in both $Γ_{1}$ and $Γ_{2}$ — while discarding is accepted, and example 184.7 identifies the discarding operation as the partial trace. Nothing in theorem 184.18 says that the described physical operation is realizable by any particular hardware, that a gate set is universal, or that an algorithm written in the calculus is faster than a classical one. Those are three further claims with three different kinds of proof.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.4 ¶

★☆☆ Show that $λ x . ⟨ x, x ⟩$ has no type $qbit ⊸ qbit \otimes qbit$ , and that it does have the type $! bit ⊸! bit \otimes! bit$ . Point at the exact premise of the pairing rule that distinguishes the two cases.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.5 ¶

★☆☆ Give a typing derivation for $λ x . 0$ at type $qbit ⊸! bit$ and describe the channel that the corresponding program implements on a one-qubit register.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.6 ¶

★★☆ Delete the injectivity requirement on $L$ from definition 184.8. Exhibit a program state that is well typed in the sense of definition 184.11, reduces, and violates the conclusion of theorem 184.18; then identify the step of the proof of theorem 184.18 that used injectivity.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Type inference by decoration

Proposition 184.21 — No principal types ¶

The term $M : = λ x . λ y . x y$ has the types $T_{1} : = (A ⊸ B) ⊸ (A ⊸ B)$ and $T_{2} : =! (A ⊸ B) ⊸! (A ⊸ B)$ , and neither is a substitution instance or a subtype of the other; moreover the most general type of which both are substitution instances, namely $X ⊸ X$ , is not a type of $M$ .

Referenced from 4 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Proposition 184.21 — No principal types

Proof. Both typings are derivable: $T_{1}$ by the linear abstraction rule twice, and $T_{2}$ by the duplicable abstraction rule, whose side condition is met because $FV (M) = \emptyset$ . Neither is an instance of the other because substitution does not insert or delete a $!$ ; neither is a subtype of the other because definition 184.10 relates $! C$ and $C$ only in the direction $! C <: C$ , and the two occurrences of the affected type in $T_{1}$ and $T_{2}$ appear in opposite variance positions. Finally $X ⊸ X$ is not derivable for $M$ , since the body $x y$ requires the type of $x$ to be an arrow. ◻

Inference must therefore proceed differently: strip the exponentials, infer an ordinary simple type, and then search for a decoration.

Definition 184.22 — Skeleton and lifting ¶

Intuitionistic types are $U, V ::= α ∣ X ∣ (U \Rightarrow V) ∣ (U \times V) ∣ ⊤$ . The skeleton map $(-)^{†}$ deletes every $!$ : $\begin{aligned} (!^{n} α)^{†} & = α, & (!^{n} X)^{†} & = X, & (!^{n} ⊤)^{†} & = ⊤, \\ (!^{n} (A ⊸ B))^{†} & = A^{†} \Rightarrow B^{†}, & (!^{n} (A \otimes B))^{†} & = A^{†} \times B^{†}, \end{aligned}$ and the lifting map $(-)^{♣}$ reads the clauses backwards, producing a quantum type with no $!$ . A quantum derivation $π$ has a skeleton $π^{†}$ , obtained by applying $(-)^{†}$ to every judgment in it; a decoration of an intuitionistic derivation $ρ$ is a quantum derivation $π$ with $π^{†} = ρ$ .

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Theorem 184.23 — Decoration is sound and complete for typability ¶

Let $M$ be a term.

(Soundness) If $π$ is a quantum derivation of $Γ ⊢ M : A$ , then $π^{†}$ is an intuitionistic derivation of $Γ^{†} ⊢ M : A^{†}$ .
(Completeness) If $M$ is quantum typable and $ρ$ is any intuitionistic derivation of $Δ ⊢ M : U$ with $| Δ | = | Γ |$ , then $M$ has a quantum derivation whose skeleton is $ρ$ .
(Decidability) Quantum typability is decidable: infer an intuitionistic derivation $ρ$ , which is decidable, and search the finitely many decorations of $ρ$ that use no repeated exponential.

Referenced from 4 locations

Quantum Lambda Calculi and Linear Quantum Data

Clause (i) is proved by induction on $π$ : every quantum rule becomes the corresponding intuitionistic rule once the exponentials are deleted, the two abstraction rules both becoming the intuitionistic abstraction rule, and the context splittings becoming context sharing. Clause (ii) is Lemma 13 of the selected paper, and clause (iii) is the algorithm of its Section 5.3, using its Lemma 15 to bound the search to decorations without repeated exponentials. What is imported is the statement that a quantum typing exists whenever some decoration of the intuitionistic derivation is valid, together with the finiteness bound that makes the search terminate. The algorithm returns a type, not a description of all types; by proposition 184.21 no most general type exists.

Example 184.24 — Three rejections ¶

The following terms are rejected, each for a different reason visible in the rules. The term $λ x . ⟨ x, x ⟩$ at $qbit$ fails because the pairing rule splits the context (exercise 184.4). The term $λ x . if x then 0 else 1$ at $qbit ⊸! bit$ fails because the conditional requires the guard to have type $bit$ and $qbit <: bit$ is not derivable: a qubit cannot be inspected without measurement. The term $H (λ x . x)$ fails because $A_{H} =! (qbit ⊸ qbit)$ forces the argument to have type $qbit$ , and by lemma 184.17 an abstraction does not.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.7 ¶

★★☆ Infer the intuitionistic type of $λ f . λ x . f (f x)$ , enumerate its decorations without repeated exponentials, and determine which are valid quantum derivations. Then explain what your answer says about applying a quantum gate twice to the same qubit.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.8 ¶

★★☆ Exhibit two quantum derivations with the same skeleton whose conclusions have incomparable types, and conclude that $(-)^{†}$ is not injective on derivations. Relate this to proposition 184.21.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

A model with duals

The linear discipline of definition 184.11 suggests a model in which the tensor is not a categorical product. The pure unitary fragment — terms without $meas$ , $new$ , and $if$ , and with types built from $qbit$ , $\otimes$ , and $⊤$ — is interpreted below in finite-dimensional Hilbert spaces, and the additional structure that this model carries beyond a monoidal category is exactly what the graphical calculus of section 184.6 uses.

Definition 184.25 — Symmetric monoidal category ¶

A symmetric monoidal category is a category $C$ (definition 141.8) with a functor $\otimes : C \times C \to C$ , an object $I$ , and natural isomorphisms $α_{A, B, C} : (A \otimes B) \otimes C \to A \otimes (B \otimes C)$ , $λ_{A} : I \otimes A \to A$ , $ρ_{A} : A \otimes I \to A$ , and $σ_{A, B} : A \otimes B \to B \otimes A$ , subject to the pentagon and triangle coherence equations and to $σ_{B, A} \circ σ_{A, B} = id$ .

Referenced from 4 locations

Example 184.26 — Finite-dimensional Hilbert spaces ¶

Let $FdHilb$ have finite-dimensional complex inner-product spaces as objects and linear maps as morphisms, with $\otimes$ the tensor product and $I = C$ . The structural isomorphisms are the usual ones, and $σ$ exchanges tensor factors on basis vectors.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Definition 184.27 — Compact closure ¶

A symmetric monoidal category is compact closed when every object $A$ has a dual: an object $A^{*}$ with morphisms $η_{A} : I \to A^{*} \otimes A$ and $ε_{A} : A \otimes A^{*} \to I$ satisfying the snake equations $ρ_{A} \circ ({id}_{A} \otimes ε_{A}^{σ}) \circ α^{- 1} \circ (η_{A}^{σ} \otimes {id}_{A}) \circ λ_{A}^{- 1} = {id}_{A},$ and its mirror image for $A^{*}$ , where the superscript $σ$ marks the symmetry inserted to make the composite typecheck.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Proposition 184.28 — Hilbert spaces are compact closed ¶

Let $A$ have orthonormal basis $e_{1}, \dots, e_{n}$ and let $A^{*}$ be the dual space with dual basis $e^{1}, \dots, e^{n}$ . Define $η_{A} (1) : = \sum_{i} e^{i} \otimes e_{i}$ and $ε_{A} (x \otimes f) : = f (x)$ . Then equation 184.1 holds, so $FdHilb$ is compact closed.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Proposition 184.28 — Hilbert spaces are compact closed

Proof. Evaluate the composite on a basis vector $e_{j}$ , suppressing the structural isomorphisms, which act as identities on these elements: $e_{j} \mapsto (\sum_{i} e^{i} \otimes e_{i}) \otimes e_{j} \mapsto \sum_{i} e^{i} \otimes ε (e_{i} \otimes e_{j})^{σ} = \sum_{i} δ_{i j} e_{i} = e_{j},$ where the middle step applies $ε$ to the second and third factors after the symmetry, giving $e^{i} (e_{j}) = δ_{i j}$ . The mirror equation is the same calculation with the roles of $A$ and $A^{*}$ exchanged, using $e^{i} (e_{j}) = δ_{i j}$ again. ◻

Definition 184.29 — Dagger and dagger compactness ¶

A dagger on a category is an identity-on-objects contravariant functor $(-)^{†}$ with $f^{† †} = f$ . A dagger symmetric monoidal category is dagger compact when it is compact closed and $ε_{A} = η_{A}^{†} \circ σ_{A, A^{*}}$ . In $FdHilb$ the dagger is the adjoint of definition 184.1, and the displayed equation holds by the calculation $⟨ η_{A} (1) ∣ f \otimes x ⟩ = \sum_{i} \overset{―}{⟨ e^{i} ∣ f ⟩} ⟨ e_{i} ∣ x ⟩ = f (x)$ read as the definition of $ε_{A}$ up to the symmetry.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Proposition 184.30 — Typing soundness for the unitary fragment ¶

Interpret $qbit$ by $C^{2}$ , $⊤$ by $C$ , $A \otimes B$ by the tensor product, and a context $Δ = x_{1} : A_{1}, \dots, x_{n} : A_{n}$ by $⨂_{i} [[A_{i}]]$ . Every derivation of $Δ ⊢ M : B$ in the unitary fragment determines a linear map $[[M]] : [[Δ]] \to [[B]]$ , and the map is unitary when every gate constant occurring in $M$ is interpreted by a unitary.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Proof of Proposition 184.30 — Typing soundness for the unitary fragment

Proof. Induction on the derivation. The axiom gives an identity or a structural isomorphism. Pairing gives a tensor of the two interpretations, which is defined because the contexts are disjoint — this is exactly where the splitting of contexts is used, and it is why the interpretation exists at all. The $let$ rule composes with the associativity isomorphism. A gate constant gives its matrix. Unitarity is preserved by tensor and composition, and the structural isomorphisms are unitary. ◻

Remark 184.31 — What is claimed for the model ¶

Proposition 184.30 is a typing-soundness statement: every well-typed term of the unitary fragment has a denotation. Nothing here claims that denotational equality implies operational equivalence, that the interpretation is adequate, or that it is fully abstract; those statements are about the whole calculus, including $meas$ and $new$ , and they are not proved in this book. The terms involving measurement are interpreted not in $FdHilb$ but in the category of completely positive maps between density matrices, obtained from $FdHilb$ by Selinger’s CPM construction; that construction is dagger compact as well, and the operations of definition 184.6 are its morphisms. This chapter uses that fact only to say which category the mixed-state operations live in.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Teleportation, twice

Example 184.32 — As a typed program ¶

Let $bell$ be the term $let ⟨ a, b ⟩ = ⟨ new 0, new 0 ⟩ in CNOT ⟨ H a, b ⟩$ of type $qbit \otimes qbit$ , and let $\begin{aligned} tele : = λ q . & let ⟨ a, b ⟩ = bell in \\ let ⟨ x, y ⟩ = CNOT ⟨ q, a ⟩ in \\ let m_{1} = meas (H x) in \\ let m_{2} = meas y in C m_{1} m_{2} b, \end{aligned}$ where $C m_{1} m_{2} b$ applies $Z$ when $m_{1} = 1$ and $X$ when $m_{2} = 1$ . Typing: $tele$ has type $qbit ⊸ qbit$ . The variable $q$ is consumed by the gate; $a$ and $y$ are consumed by $CNOT$ and $meas$ ; $b$ is returned. Every context split is forced, and no rule would allow $q$ to appear twice.

Reduction: after $bell$ the register is $| ψ ⟩ \otimes | Φ^{+} ⟩$ where $| ψ ⟩ = α | 0 ⟩ + β | 1 ⟩$ is the input qubit. Applying $CNOT$ to the first two qubits and $H$ to the first rewrites the state as $\frac{1}{2} \sum_{m_{1}, m_{2} \in {0, 1}} | m_{1} m_{2} ⟩ \otimes X^{m_{2}} Z^{m_{1}} | ψ ⟩,$ an identity checked by expanding both sides on the basis $| 0 ⟩, | 1 ⟩$ for $| ψ ⟩$ . The two measurements therefore each return $0$ or $1$ with probability $\frac{1}{2}$ , and in the branch $(m_{1}, m_{2})$ the third qubit is $X^{m_{2}} Z^{m_{1}} | ψ ⟩$ ; the correction $C$ applies $Z^{m_{1}}$ and $X^{m_{2}}$ , which are self-inverse, leaving $| ψ ⟩$ . Two classical bits were produced and consumed, and the linear typing shows that the input qubit no longer exists: the value of $q$ was consumed by a gate, and only $b$ is returned.

Referenced from 5 locations

Quantum Lambda Calculi and Linear Quantum Data

Example 184.33 — As an equation between morphisms ¶

Read equation 184.1 with $A = C^{2}$ . The composite $(id \otimes ε) \circ (η \otimes id)$ sends a state $| ψ ⟩$ placed on the left wire to the same state on the right wire, having passed through the pair created by $η$ ; that is precisely the statement that a state can be moved along an entangled pair. In the graphical notation, in which a morphism is a box, composition is vertical, $\otimes$ is horizontal, and $η, ε$ are a cup and a cap, the equation says that a wire bent twice may be straightened.

The equation is not yet teleportation, and the difference is exactly the corrections in example 184.32: $ε$ is a single morphism, while a measurement in the Bell basis produces one of four outcomes, each corresponding to $ε \circ (id \otimes U_{m})$ for one of the four Pauli maps $U_{m}$ . Teleportation is therefore the snake equation together with the fact that each $U_{m}$ is invertible and its inverse is applicable by a classically controlled gate. The graphical calculus makes the first half visible; the second half is classical control, which is definition 184.9 and not a property of the monoidal structure.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Safe uncomputation, compared. A high-level quantum language may provide automatic uncomputation of temporary values. In Silq, a term marked $qfree$ is one whose action is a permutation of basis states, and the type system permits a temporary value produced by a $qfree$ computation to be discarded silently, inserting its inverse. The rule delta against definition 184.11 is: add an annotation $qfree$ on functions, and add a discard rule permitting $Γ, x : A ⊢ M : B$ to conclude $Γ ⊢ let x = N in M : B$ when $N$ is $qfree$ and $x$ is unused. In the calculus of this chapter that rule is unnecessary for typability, since weakening is already admissible; the difference is operational, because Silq’s rule promises that the discarded value leaves no entanglement, whereas example 184.7 shows that plain discarding may leave a mixed state. Neither Silq’s theorem nor its implementation is imported: the comparison is a rule delta and an example, and theorem 184.18 is unaffected by it.

Exercise 184.9 ¶

★★☆ Verify equation 184.1 in $FdHilb$ for $A = C^{2}$ by writing $η (1) = e^{1} \otimes e_{1} + e^{2} \otimes e_{2}$ and evaluating the composite on $e_{1}$ and on $e_{2}$ separately. Then compute what the composite does if $η (1)$ is replaced by $e^{1} \otimes e_{1}$ alone, and say which equation fails.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.10 ¶

★★☆ Complete the expansion asserted in example 184.32: expand $| ψ ⟩ \otimes | Φ^{+} ⟩$ , apply $CNOT$ to the first two qubits and $H$ to the first, and collect terms to obtain the displayed sum. Then write the correction $C$ as a term of the calculus and give its typing derivation.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Boundary

The type system of definition 184.11 prevents the specified ill-formed uses of quantum data: duplication of a linear variable, application of a gate to a non-qubit, and inspection of a qubit without measurement (example 184.24). Theorem 184.18 is a statement about configurations of this calculus and about nothing else. In particular it does not establish that a physical device implements a gate, that a described process is unitary, that an algorithm has a claimed speedup, or that a compiled circuit is efficient. Quantum error correction, cryptographic security, and hardware compilation require their own theorems with their own hypotheses. Circuit generation — producing a reusable circuit value rather than executing a computation on a register — is a different problem with its own staging discipline, and it is not treated here.

Suggested first pass.

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

Exercise 184.11 ¶

★★☆ Write out the pairing case of lemma 184.15 in full, including the subcase in which $x :! C$ lies in the shared duplicable part of the context. State exactly where lemma 184.14(ii) is used and what would go wrong without it.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.12 ¶

★★☆ The following argument is wrong. “Subject reduction holds for the calculus without the injectivity condition on $L$ , because the typing of a program state depends only on $M$ , and theorem 184.16 only ever inspects $M$ .” Identify the step of the proof of theorem 184.18 that fails under this hypothesis, exhibit the resulting error state, and state the invariant that the corrected argument must carry.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.13 ¶

★★★ Define, for finite-dimensional spaces $A$ and $B$ , the set of completely positive maps from density matrices on $A$ to density matrices on $B$ , and verify that the measurement of definition 184.5 followed by forgetting the outcome is such a map by exhibiting its Kraus operators. Then compute the map determined by $λ x . 0$ of exercise 184.5 and compare it with example 184.7.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.14 ¶

★★☆ Prove clause (i) of theorem 184.23 in full by induction on the quantum derivation, displaying the two abstraction cases separately. Then explain why the converse direction cannot be proved the same way, and which finiteness statement replaces it.

Referenced from 2 locations

Quantum Lambda Calculi and Linear Quantum Data

Exercise 184.15 ¶

★★★ Practical project.quantum-lambda-safety-checker Implement in Agda or Kappa a checker and simulator for the calculus of definition 184.8, definition 184.11, definition 184.9. Represent program states as a triple of a state vector over a fixed set of exact amplitudes — rationals together with the single irrational $1 / \sqrt{2}$ , represented symbolically — a linking function, and a term. Implement: the subtyping relation; the typing rules with context splitting; the reduction relation, with measurement returning both branches and their probabilities rather than sampling; and a check that the linking function stays injective.

The invariant to maintain is the one proved in theorem 184.16, theorem 184.18: after every step the state is well typed at the same type, the linking function is injective, and the probabilities of the available single-step reductions sum to $1$ . The concrete result is a function taking a closed term and returning either a typing error, or its type together with the tree of reachable configurations with their probabilities.

Acceptance test. The program of example 184.12 is accepted at type $! bit$ and produces exactly two final configurations, each of probability $\frac{1}{2}$ , with registers $| 00 ⟩$ and $| 11 ⟩$ . The term $λ x . ⟨ x, x ⟩$ is rejected at $qbit ⊸ qbit \otimes qbit$ and accepted at $! bit ⊸! bit \otimes! bit$ . The terms $H (λ x . x)$ and $λ x . if x then 0 else 1$ at $qbit$ are rejected, with the checker naming the premise that fails. The term $tele$ of example 184.32, applied to a qubit prepared in $α | 0 ⟩ + β | 1 ⟩$ , yields four configurations of probability $\frac{1}{4}$ whose returned qubit is in state $α | 0 ⟩ + β | 1 ⟩$ in every branch. A mutation of the typing rules that shares rather than splits the context in the pairing rule must accept $λ x . ⟨ x, x ⟩$ at $qbit$ and must then produce an error state on the gate rule, which the invariant check must report.

The program simulates a fixed finite gate set on small registers with exact symbolic amplitudes. It illustrates theorem 184.16, theorem 184.18 and proves neither, and its simulator output is not evidence about physical hardware.

Referenced from 3 locations

Quantum Lambda Calculi and Linear Quantum Data

Bibliographic notes

The calculus, its probabilistic reduction on program states, its affine linear type system with subtyping, and the safety and inference results of section 184.2, section 184.3, section 184.4 are those of Selinger and Valiron, A Lambda Calculus for Quantum Computation with Classical Control, arXiv cs/0404056: definition 184.8 is its Definition 1, lemma 184.15 its Lemma 10, theorem 184.16 its Theorem 1, theorem 184.18 its Theorem 2 with Corollary 2, and theorem 184.23 its Lemma 13 with the algorithm of its Section 5.3. The decoration technique for linear type inference is due to Danos, Joinet, and Schellinx. Valiron’s later author-released Haskell embedding, retained in the reference library, implements a related discipline with a QRAM simulator; it is implementation evidence, targets a historical compiler, and is not a release accompanying the paper.

The compact-closed and dagger structure of section 184.5 is that of Abramsky and Coecke’s categorical quantum mechanics, with the CPM construction for mixed states due to Selinger; proposition 184.28 is the standard verification in $FdHilb$ , and the reading of teleportation as the snake equation together with classical corrections (example 184.33) is theirs. Vicary’s lecture notes and the Edinburgh course on quantum programming semantics are the recommended companions for the graphical calculus; de Wolf’s and Watrous’s texts supply the quantum-information background compressed into section 184.1, and Valiron’s current notes bridge from linear algebra to the calculus. The safe-uncomputation comparison of section 184.6 is the design problem solved by Silq, in Bichsel, Baader, Gehr, and Vechev, Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics, PLDI 2020; that paper and its artifact are retained in the reference library and own no statement above.