⁴Some semantics manage to combine σ and Σ by making objects immutable (reference typing is indistinguishable from copying if nothing can be modified anyway), but mutability is sufficiently important that we define then separately.