Logical relations
Logical relations are a proof method employed in programming language semantics to show that two denotational semantics are equivalent.
To describe the process, let us denote the two semantics by , . For each type , we associate a particular relation between and . We define this relation such that for all program phrase , the two denotations are related: . Another property of this relation is that related denotations for ground types are equivalent in some sense, usually equal. The conclusion is then that both denotations exhibit equivalent behavior on ground terms, hence are equivalent.
![{\displaystyle [\![-]\!]_{i}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/30fb104fc3f9d6e56ab74ab8ba7b9052de9ea992)
![{\displaystyle [\![A]\!]_{1}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/15751d4784b43fa2875b69b2fdca820a82c69791)
![{\displaystyle [\![A]\!]_{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/52ff30c819d657bc838e86acfdc9e3430ec3a6e7)
![{\displaystyle [\![M]\!]_{1}\sim [\![M]\!]_{2}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/15c50096d64dcad0f1b814f06567e079dae72383)
References
 | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |