Manuscript Hawk04-D@1 · Hawk04-D-v1.tex · section · 39b16f67

Enter, discard, and finite soundness

Complete interfaces and the finite operational core › Enter, discard, and finite soundness · lines 441–456

Hawk04-D@1#eq:Enter

Let $S$ be a measured finite register and $T$ the surviving quantum register. In the computational basis, put $M_{x} = ⟨ x ∣_{S} \otimes I_{T}$ . Define the destructive instrument

M_{S} (X) = x \sum ∣ x ⟩ ⟨ x ∣_{K} \otimes M_{x} X M_{x}^{†} .

The output names are $K, T$ , not $S$ ; $K$ carries the diagonal classical algebra. Define

dropBit_{K} (x \sum ∣ x ⟩ ⟨ x ∣_{K} \otimes X_{x}) = x \sum X_{x} .

Displayed formulas in this passage

Hawk04-D@1#eq:Enter · line 447
$M_{S} (X) = x \sum ∣ x ⟩ ⟨ x ∣_{K} \otimes M_{x} X M_{x}^{†} .$
unlabeled · line 453
$dropBit_{K} (x \sum ∣ x ⟩ ⟨ x ∣_{K} \otimes X_{x}) = x \sum X_{x} .$

Nearby in this section

proposition: Proposition: Readout, forgetting, and complete accounting
section: Enter, discard, and finite soundness
proposition: Proposition: Finite-program soundness
section: Enter, discard, and finite soundness