The concrete finite semantics

We use the relevant types

A quantum name is an access right to one factor of a global state. Allocation $\mathsf{new}$ supplies $|0⟩$. A gate consumes and returns its named quantum arguments. Destructive readout consumes the measured name and returns a classical bit.

For a computational-basis readout of $S$,

and the explicitly specified transition has probability

and normalized residual ${M_{\kappa }}^S\psi /\text{norm}{M_{\kappa }}^S\psi$ on positive branches. This is the concrete semantics considered in CheungEnter,CheungI.

A conditional has the same quantum context in its two alternatives but executes only one alternative. Thus it does not duplicate quantum ownership. Classical deletion is represented by

There is no corresponding silent deletion of a quantum name.