Relation to other approaches

Quantum lambda calculi with classical control already provide well-developed operational and typing frameworks; the affine calculus of Selinger and Valiron is a representative example SelingerValiron. The present language uses strict, branch-wise linear ownership. Its characterization question concerns a variable measurement transition in a fixed language, rather than type safety alone.

Gleason's theorem concerns measures on Hilbert-space subspaces subject to a different assumption package Gleason. The present proof does not begin with probabilities for all effects or projectors. It characterizes one fixed-basis primitive; other measurements are represented later by programs.

The uniform-correlation argument uses a system/environment permutation mechanism related to envariance arguments ZurekEnvariance. Its premises are stated explicitly as operational requirements. The importance of distinguishing such premises from derived probabilities is emphasized in the analysis of Schlosshauer and Fine SchlosshauerFine. Neither envariance nor a separate noncontextuality axiom is imported as an additional premise.

Finally, the companion manuscripts discussed in Section sec:interfaces concern implementation and observational boundaries. They are not premises of Theorem thm:main.