Introduction and logical scope

Fix a quantum programming language: its types, allocation, tensor composition, coherent gates, and classical control. Leave only the outcome law and conditional update of a destructive measurement primitive unspecified. Which strategies interpret that primitive while satisfying specified equations between experiments?

The primitive considered here is $\mathsf{Enter}$, destructive computational-basis readout of a finite qubit register. A configuration contains one global pure state. Runtime qubit names are access rights to its tensor factors; they are not individual pure-state assignments. Readout consumes the measured names, returns classical bits, and leaves a state on the surviving factors.

This manuscript gives a self-contained, scope-restricted presentation of the finite Enter-calculus characterization of Cheung EnterCalculus. The central result is Theorem thm:main. Here “Born–Lüders” means projective conditioning followed by removal of the measured factors, not retention of those factors. The distinction between outcome probabilities and state change is essential; the historical projective update is discussed in Lüders' work and its English translation LudersTranslation.