Jakie jest pochodzenie relacji logicznych?

Mam dwa pytania:

1. Kto pierwszy użył relacji logicznych do powiązania semantyki?

   Prześledziłem je z powrotem do „Reynolds of the Relation Between Direct and Continuation Semantics ” Reynolda , ale nie mogę twierdzić, że przeprowadziłem wyczerpujące poszukiwania.

   Znalazłem odniesienia do relacji logicznych datowanych wcześniej (Tait, '67), ale nie do powiązania semantyki.

2. Jakie jest najlepsze obecne wprowadzenie do relacji logicznych?

Znam „ Systemy typów dla języków programowania ” Mitchella z podręcznika TCS. Jakie są inne ekspozycje?

Drugi akapit Memo Plotkina z 1973 r. W sprawie definicji lambda i relacji logicznych mówi:

„Definicja logicznej [relacji] pochodzi od odpowiadającej M. Gordon dla typowanego rachunku λ.”

To nie mówi wprost, że termin ten został wymyślony przez Gordona. Ale biorąc pod uwagę, że notatka nosi tytuł „Lambda-definiowalność i relacje logiczne”, tak jakby „relacja logiczna” jest już znaną ideą, a drugi akapit mówi „konstruować pewne, tak zwane , relacje logiczne”, myślę, że jest bardzo prawdopodobne że Gordon ukuł ten termin, a Plotkin go użył. (Plotkin potwierdził mi, że wszystko, co napisał w notatce, jest poprawne).

Gordon zostaje ponownie przypisany na początku strony p. 12,

„M. Gordon zaproponował jako możliwy środek zaradczy, że stosunki… powinny zostać rozszerzone - nie tylko permutacje”.

Opublikowana wersja artykułu („Definiowalność Lambda w hierarchii pełnego typu” w To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism ) ma tę uwagę. Ma także uwagę, którą można interpretować jako wyjaśnienie terminu „relacja logiczna”:

$\lambda$$D$

Moim zdaniem jest to niezwykle satysfakcjonujące wyjaśnienie, dlaczego relacje logiczne są „logiczne”. Rachunek lambda jest logiczny, a zatem zdefiniowane za jego pomocą funkcje będą jednolite w odniesieniu do typów bazowych. Nie mogą „zobaczyć” permutacji, jakie moglibyśmy zastosować do wartości typów podstawowych. Patrząc w ten sposób, to, co Gordon i Plotkin rozumieli jako „logiczny”, jest zasadniczo takie samo, jak to, co Reynolds nazywa „parametrycznym”.

Jednak termin „relacja logiczna” nie pojawia się w opublikowanej wersji artykułu. Możliwe, że sędziowie mogliby sprzeciwić się, że termin był mylący, a Plotkin mógł zdecydować, że najlepiej będzie go unikać. Ale Statman wrócił do starej terminologii i termin ten powrócił do popularnego języka.

Plotkin użył relacji logicznych w swoim nieopublikowanym, ale mimo to szeroko rozpowszechnionym i wpływowym artykule z 1973 r. „Definicja lambda i relacje logiczne”. Mam kopię tej notatki na mojej stronie internetowej.

Kiedyś myślałem, że stąd pochodzi nazwa, ale kiedy zapytałem o to Ricka Statmana, powiedział mi, że Mike Gordon ukuł termin logiczny, aby opisać metodę Tait, i że on i Gordon Plotkin to od niego wzięli. Myślę, że w ten sposób wszedł do żargonu języka programowania, choć można to sprawdzić, pytając Plotkina.