Logiska relationer
Logiska relationer är en bevismetod som används i programmeringsspråkssemantik för att visa att två denotationssemantik är likvärdiga.
För att beskriva processen, låt oss beteckna de två semantikerna med där . För varje typ finns det en särskild associerad relation mellan och . Denna relation är definierad så att för varje programfras är de två beteckningarna relaterade: . En annan egenskap hos denna relation är att relaterade beteckningar för marktyper är likvärdiga i någon mening, vanligtvis lika. Slutsatsen är då att båda denotationerna uppvisar likvärdigt beteende på markmässiga villkor, och därför är likvärdiga.
![{\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)
- https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/ahmed-1.pdf
- POPLmark Reloaded : Bevis som involverar logiska relationer som används som riktmärke för korrekturassistenter .
Kategorier: