Na verdade, tenho duas perguntas:
Quem primeiro usou as relações lógicas para relacionar a semântica?
Rastreei-os de volta à " Sobre a relação entre a semântica direta e a continuação " de Reynold , mas não posso afirmar que fiz uma pesquisa exaustiva.
Eu encontrei referências a relações lógicas datadas anteriormente (Tait, 67), mas não para relacionar semântica.
Qual é a melhor introdução atual para relações lógicas?
Conheço os " Type Systems for Programming Languages " de Mitchell no Handbook of TCS. Que outras exposições existem?
reference-request
pl.programming-languages
denotational-semantics
logical-relations
Ohad Kammar
fonte
fonte
Respostas:
O segundo parágrafo do Memorando de 1973 de Plotkin sobre definibilidade lambda e relações lógicas diz o seguinte:
Isso não diz explicitamente que o termo foi cunhado por Gordon. Mas, dado que o memorando é intitulado "definibilidade lambda e relações lógicas" como se "relação lógica" fosse uma idéia já conhecida, e o segundo parágrafo diz "construa certas relações ditas , lógicas", acho muito provável que Gordon cunhou o termo e Plotkin o usou daí. (Plotkin me confirmou que tudo o que ele escreveu no memorando está correto.)
Gordon é creditado novamente no topo da p. 12,
A versão publicada do artigo ("definibilidade lambda na hierarquia completa de tipos" em To HB Curry: Ensaios sobre lógica combinatória, cálculo lambda e formalismo ) tem essa observação. Ele também possui uma observação que poderia ser interpretada como uma explicação do termo "relação lógica":
Na minha opinião, esta é uma explicação extremamente satisfatória de por que as relações lógicas são "lógicas". O cálculo do Lambda é lógico e, portanto, as funções definidas com ele serão uniformes em relação aos tipos de base. Eles não podem "ver" as permutações que podemos fazer com os valores dos tipos de base. Visto dessa maneira, o que Gordon e Plotkin queriam dizer com "lógico" é essencialmente o mesmo que Reynolds chama de "paramétrico".
No entanto, o termo "relação lógica" não aparece na versão publicada do artigo. É possível que os árbitros tenham contestado que o termo seja confuso e Plotkin tenha decidido melhor evitar o termo. Mas Statman voltou à antiga terminologia e o termo voltou à linguagem popular.
fonte
Plotkin usou relações lógicas em seu artigo de 1973 inédito, mas amplamente divulgado e influente "Lambda Definability and Logical Relations". Eu tenho uma cópia desta nota na minha página da web.
Eu costumava pensar que era daí que o nome veio, mas quando perguntei a Rick Statman sobre isso, ele me disse que Mike Gordon cunhou o termo relação lógica para descrever o método de Tait, e que ele e Gordon Plotkin o buscaram. Eu acho que foi assim que entrou no jargão da linguagem de programação, embora você possa ter certeza perguntando ao Plotkin.
fonte