Логические отношения
Логические отношения — это метод доказательства, используемый в семантике языков программирования, чтобы показать, что две денотационные семантики эквивалентны.
Для описания процесса обозначим две семантики через , где . Для каждого типа , существует определенное связанное отношение между и . Это отношение определяется так, что для каждой программной фразы , эти два обозначения связаны: . Другое свойство этого отношения состоит в том, что связанные обозначения основных типов в некотором смысле эквивалентны, обычно равны. Таким образом, вывод состоит в том, что оба обозначения демонстрируют эквивалентное поведение в основных терминах и, следовательно, эквивалентны.
![{\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)
Ссылки
[ редактировать ]https://www.cs.uoregon.edu/research/summerschool/summer16/notes/AhmedLR.pdf
https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed-1.pdf
- POPLmark Reloaded : доказательства, включающие логические отношения, используемые в качестве эталона для помощников по доказательству .
 | Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |