Логические отношения - Logical relations

Логические отношения площадь метод доказательства занят в семантика языка программирования чтобы показать, что два денотационная семантика эквивалентны.

Для описания процесса обозначим обе семантики как ${\displaystyle [\![-]\!]_{i}}$, ${\displaystyle i=1,2}$. Для каждого типа ${\displaystyle A}$, мы связываем частное отношение ${\displaystyle a\sim b}$ между ${\displaystyle [\![A]\!]_{1}}$ и ${\displaystyle [\![A]\!]_{2}}$. Мы определяем это отношение так, чтобы для всей программной фразы ${\displaystyle M}$, эти два обозначения связаны: ${\displaystyle [\![M]\!]_{1}\sim [\![M]\!]_{2}}$. Другое свойство этого отношения состоит в том, что соответствующие обозначения для типы грунта в некотором смысле эквивалентны, обычно равны. Отсюда следует вывод, что оба обозначения демонстрируют эквивалентное поведение в основных терминах, следовательно, эквивалентны.

Рекомендации

• https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed-1.pdf
• POPLmark Reloaded: Доказательства, включающие логические отношения, используемые в качестве ориентира для помощники доказательства.