Definition. Computational adequacy (of semantics) [cs-H4U2]

2025-02-24 · Lîm Tsú-thuàn
Domain-Theoretic Foundations of Functional Programming

denotationally equal [local-0]

Let P,QP, Q be programs of type σ\sigma, we say PP and QQ is denotationally equal if

⟦P⟧=⟦Q⟧∈Dσ\llbracket P \rrbracket = \llbracket Q \rrbracket \in D_{\sigma}

correctness [local-1]

We say the operational semantics correct with respect to the denotational semantic iff PP and VV are denotationally equal whenever

P⇓VP \Downarrow V

completeness [local-2]

We say the operational semantics complete with respect to the denotational semantic iff

P⇓V‾P \Downarrow \overline{V}

whenever ⟦P⟧=V∈Dσ\llbracket P \rrbracket = V \in D_{\sigma}.

The V‾\overline{V} represents the expression of VV, e.g. 11 has an expression 1 in many programming languages.

In case the operational semantics is both correct and complete (with respect to) the denotational semantics for all programs and values, we say the denotational semantics is computationally adequate. i.e.

P⇓V‾  ⟺  ⟦P⟧=VP \Downarrow \overline{V} \iff \llbracket P \rrbracket = V