 Definition 1.1 (Denotational equivalence). Given any two program phrases \(e,e'\), they are denotationally equivalent, written \(e \simeq_{\mathcal{M}}e'\), when \({\mathcal{M}}(e) = {\mathcal{M}}(e')\).