Las relaciones lógicas son un método de prueba empleado en la semántica del lenguaje de programación para demostrar que dos semánticas denotacionales son equivalentes.
Para describir el proceso, denotemos las dos semánticas por , donde . Para cada tipo , existe una relación asociada particular entre y . Esta relación se define de modo que para cada frase de programa , las dos denotaciones están relacionadas: . Otra propiedad de esta relación es que las denotaciones relacionadas para los tipos básicos son equivalentes en algún sentido, generalmente iguales. La conclusión es entonces que ambas denotaciones exhiben un comportamiento equivalente en términos básicos, por lo tanto son equivalentes.
https://www.cs.uoregon.edu/research/summerschool/summer16/notes/AhmedLR.pdf
https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed-1.pdf
![{\displaystyle [\![\cdot ]\!]_{i}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/150bd12ce12b667cfc9209aacf3cbe36df4de700)
![{\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)