Definition: Name discipline

A quantum context is a finite set of pairwise distinct live quantum names. A unitary instruction acts on names in the context and preserves them. Allocation introduces a globally fresh name. The instruction $\mathsf{Enter}(q)$ removes $q$ from the quantum context and returns one classical basis value. Subsequent instructions may use only live quantum names. Classical computation does not introduce a quantum name.