 This formulation highlights another valuable aspect of compositionality, namely the referentially transparency of all contexts, equivalently their extensionality: denotationally equivalent phrases can be substituted in any context leaving unchanged the denotation of the resulting phrase. The implication (\(\ref{compositionality}\)) states, in particular, that \({\simeq_{\mathcal{M}}}\) is a congruence. In order to compare denotational and operational congruence, therefore, we must carve a congruence out of the naive operational equivalence defined by setting \(e \sim e'\) if and only if \({\mathcal{O}}(e) = {\mathcal{O}}(e')\). This can be done by exploiting program contexts \(C\blbr\), representing a program with a “hole” that can be filled by program phrases \(e\) of suitable type to yield a complete program \(C[e]\).