¿Cuál es el origen de las relaciones lógicas?

15

En realidad tengo dos preguntas:

  1. ¿Quién utilizó primero las relaciones lógicas para relacionar la semántica?

    Los rastreé hasta " La relación entre la semántica directa y de continuación " de Reynold , pero no puedo afirmar que haya hecho una búsqueda exhaustiva.

    He encontrado referencias a relaciones lógicas que datan antes (Tait, '67), pero no para relacionar la semántica.

  2. ¿Cuál es la mejor introducción actual para las relaciones lógicas?

Conozco los " Sistemas de tipos para lenguajes de programación " de Mitchell del Manual de TCS. ¿Qué otras exposiciones hay?

reference-request pl.programming-languages denotational-semantics logical-relations Ohad Kammar
fuente
2
Hay un capítulo sobre Relaciones lógicas en Fundamentos de Mitchell para lenguajes de programación . La parte inferior de la primera página ofrece una breve descripción histórica, citando los principales documentos. Podría escribir esto si no puedes conseguir el libro de Mitchell.
Dave Clarke
Puedo tenerlo en mis manos, ¡gracias! Echaré un vistazo cuando llegue a la oficina.
Ohad Kammar 01 de
OK, el libro es mucho más elaborado que el capítulo del manual, aunque cubren aproximadamente el mismo material (menos Sconing, lamentablemente). Las notas históricas son casi idénticas, con la notable excepción de que el libro menciona el informe técnico de Plotkin que NeelK da a continuación.
Ohad Kammar 01 de

Respuestas:

6

El segundo párrafo del Memo de Plotkin de 1973 sobre la capacidad de definición de Lambda y las relaciones lógicas dice esto:

"La definición de [relación] lógica se deriva de una correspondiente de M. Gordon para el cálculo λ escrito".

Esto no dice explícitamente que el término fue acuñado por Gordon. Pero, dado que el memo se titula "Definibilidad de Lambda y relaciones lógicas" como si la "relación lógica" fuera una idea ya conocida, y el segundo párrafo dice "construir ciertas, llamadas relaciones lógicas", creo que es muy probable que Gordon acuñó el término y Plotkin lo usó por lo tanto. (Plotkin me confirmó que todo lo que escribió en el memo es correcto).

Gordon se acredita nuevamente en la parte superior de la p. 12,

"M. Gordon propuso, como posible remedio, que las relaciones ... deberían extenderse, no solo permutaciones".

La versión publicada del artículo ("Definibilidad de Lambda en la jerarquía de tipo completo" en To HB Curry: Ensayos sobre lógica combinatoria, cálculo de Lambda y formalismo ) tiene este comentario. También tiene una observación que podría interpretarse como una explicación del término "relación lógica":

Debido a la naturaleza "lógico" de los elementos -definable, deben ser invariante bajo permutaciones de D .λre

En mi opinión, esta es una explicación extremadamente satisfactoria de por qué las relaciones lógicas son "lógicas". El cálculo de Lambda es lógico y, por lo tanto, las funciones definidas al usarlo serán uniformes con respecto a los tipos base. No pueden "ver" las permutaciones que podríamos hacer con los valores de los tipos base. Visto de esta manera, lo que Gordon y Plotkin quieren decir con "lógico" es esencialmente lo mismo que Reynolds llama "paramétrico".

Sin embargo, el término "relación lógica" no aparece en la versión publicada del documento. Es posible que los árbitros hayan objetado que el término sea confuso y Plotkin haya decidido que es mejor evitarlo. Pero, Statman volvió a la antigua terminología y el término ha vuelto al lenguaje popular.

Uday Reddy
fuente
14

Plotkin usó las relaciones lógicas en su trabajo inédito pero sin embargo ampliamente circulado e influyente de 1973 "Lambda Definability and Logical Relations". Tengo una copia de esta nota en mi página web.

Solía ​​pensar que de ahí viene el nombre, pero cuando le pregunté a Rick Statman sobre esto, me dijo que Mike Gordon acuñó el término relación lógica para describir el método de Tait, y que él y Gordon Plotkin lo tomaron de él. Creo que así es como entró en la jerga del lenguaje de programación, aunque puede asegurarse preguntándole a Plotkin.

Neel Krishnaswami
fuente
1
Esto casi suena como un jugoso chisme de TCS.
Dave Clarke
55
No le pidas a Gordon, solo debes obligarlo a participar en este sitio, como hice con Dana.
Andrej Bauer
1
Bien, le pregunté a Gordon Plotkin y a Mike Gordon. Ambos están de acuerdo en que Gordon Plotkin acuñó el término "relaciones lógicas", y cada uno afirmó que la idea de usar las relaciones vino del otro.
Ohad Kammar
1
La tesis de Gandy ahora está disponible gratuitamente en línea: repository.cam.ac.uk/handle/1810/245090
Ohad Kammar
2
@OhadKammar: La "definibilidad Lambda de Plotkin en la jerarquía de tipos completos" le da crédito a Howard al decir que Howard también utilizó la idea de usar relaciones en lugar de permutaciones "para definir sus funciones hereditariamente mayorizables [Tro]". La cita es para un libro, pero el único capítulo de Howard es el apéndice, "Funcionalidades heredables de tipo finito": download.springer.com/static/pdf/314/… (de link.springer.com/book/10.1007 % 2FBFb0066739 ).
Blaisorblade