Manuscript X-Enter@1 · X-Enter.tex · section · 484b71bc

Programs and records

Frozen finite interface and selective formula › Programs and records · lines 405–454

X-Enter@1#eq:instrument, X-Enter@1#eq:recordchannel

The quantum type $Q$ denotes an owned qubit; $Bit$ denotes a classical bit; $1$ denotes the unit output. Tensor contexts split ownership. Conditionals use the same resources in their alternatives, exactly one of which executes.

Let $P_{4}$ be the class of finite first-order programs

P : Q ⊸ Bit^{\otimes m} \otimes Q^{\otimes k}

whose executions use at most four live qubits, including the input. Here $m, k$ are nonnegative integers and $Q^{\otimes 0} = 1$ . Programs use fixed finite-register unitaries, fresh zero-state allocation, finite classical control, and destructive Enter only. Every quantum name is consumed or returned. Code and gates remain fixed during gauge comparisons.

Complete histories are finite. Their path maps satisfy

Φ_{y}^{P} (ρ) = h : out (h) = y \sum K_{h} ρ K_{h}^{†}, h \sum K_{h}^{†} K_{h} = I .

Indeed, fix a history and compose allocation isometries, gates, and destructive measurement bras. Branch normalizations cancel against their probabilities. Backward induction on the finite outcome tree, using $\sum_{b} ∣ b ⟩ ⟨ b ∣ = I$ , gives completeness.

Thus the $Φ_{y}^{P}$ are completely positive selective maps whose sum is trace preserving. Define

Φ_{P} (ρ) = y \sum ∣ y ⟩ ⟨ y ∣ \otimes Φ_{y}^{P} (ρ), Rec_{P} (ρ) = Φ_{P} (ρ) .

This instrument notation includes probabilities and conditional quantum outputs Watrous (Section 2.3.2). Failure branches are retained. No postselected renormalization defines the record.

Displayed formulas in this passage

X-Enter@1#eq:instrument · line 426
$Φ_{y}^{P} (ρ) = h : out (h) = y \sum K_{h} ρ K_{h}^{†}, h \sum K_{h}^{†} K_{h} = I .$
X-Enter@1#eq:recordchannel · line 442
$Φ_{P} (ρ) = y \sum ∣ y ⟩ ⟨ y ∣ \otimes Φ_{y}^{P} (ρ), Rec_{P} (ρ) = Φ_{P} (ρ) .$
unlabeled · line 414
$P : Q ⊸ Bit^{\otimes m} \otimes Q^{\otimes k}$