論理関係

論理関係は、2 つの表示的意味論が同等であることを示すためにプログラミング言語の意味論で使用される証明方法です。

このプロセスを説明するために、2 つのセマンティクスを で表します。ここで、 です。各型について、と の間には特定の関連関係があります。この関係は、各プログラム フレーズ について、2 つの表記が に関連付けられるように定義されます。この関係のもう 1 つの特性は、基底型の関連する表記が何らかの意味で同等であり、通常は等しいことです。したがって、両方の表記は基底項に対して同等の動作を示すため、同等であるという結論になります。 ${\displaystyle [\![\cdot ]\!]_{i}}$${\displaystyle i\in \{1,2\}}$ ${\displaystyle A}$ ${\displaystyle \sim}$${\displaystyle [\![A]\!]_{1}}$${\displaystyle [\![A]\!]_{2}}$${\displaystyle M}$${\displaystyle [\![M]\!]_{1}\sim [\![M]\!]_{2}}$

https://www.cs.uoregon.edu/research/サマースクール/サマー16/notes/AhmedLR.pdf

https://www.cs.uoregon.edu/research/サマースクール/サマー13/lectures/ahmed-1.pdf

• POPLmark Reloaded:証明支援システムのベンチマークとして使用される論理関係を含む証明。