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

Erasure

Retained diagnostic branches and exact decoding › Erasure · lines 1212–1227

With $ι_{0}$ , every program receives the same state. Invariance is bought by ignoring the coefficient.

With $ι_{1}$ , deliberate erasure remains well typed:

P_{erase} = λ q : Q . let b = Enter (q) in if b then ⟨ 0, * ⟩ else ⟨ 0, * ⟩ .

The input qubit and its measured bit are consumed. The constant output does not invariantize an informative record.

Displayed formulas in this passage

unlabeled · line 1218
$P_{erase} = λ q : Q . let b = Enter (q) in if b then ⟨ 0, * ⟩ else ⟨ 0, * ⟩ .$