Woher stammen logische Beziehungen?

Ich habe eigentlich zwei Fragen:

1. Wer benutzte zuerst logische Beziehungen, um die Semantik in Beziehung zu setzen?

   Ich habe sie auf Reynolds " Über die Beziehung zwischen direkter und Fortsetzungssemantik " zurückgeführt, aber ich kann nicht behaupten, eine erschöpfende Suche durchgeführt zu haben.

   Ich habe Hinweise auf frühere logische Beziehungen gefunden (Tait, '67), aber nicht für semantische Beziehungen.

2. Was ist die beste aktuelle Einführung für logische Beziehungen?

Ich kenne Mitchells " Typensysteme für Programmiersprachen " aus dem Handbuch von TCS. Welche anderen Ausstellungen gibt es?

Der zweite Absatz von Plotkins Memo über Lambda-Definierbarkeit und logische Beziehungen von 1973 lautet wie folgt :

"Die Definition der logischen [Relation] leitet sich aus einer entsprechenden Definition von M. Gordon für die typisierte λ-Rechnung ab."

Dies besagt nicht ausdrücklich, dass der Begriff von Gordon geprägt wurde. Angesichts der Tatsache, dass das Memo den Titel "Lambda-Definierbarkeit und logische Beziehungen" trägt, als ob "logische Beziehung" eine bereits bekannte Idee ist, und im zweiten Absatz heißt es "konstruiere bestimmte, sogenannte logische Beziehungen", halte ich dies für sehr wahrscheinlich dass Gordon den Begriff geprägt und Plotkin ihn daher verwendete. (Plotkin hat mir bestätigt, dass alles, was er in das Memo geschrieben hat, korrekt ist.)

Gordon wird erneut am oberen Rand von p gutgeschrieben. 12,

"M. Gordon schlug als mögliche Abhilfe vor, die Beziehungen ... zu erweitern - nicht nur die Permutationen."

Die veröffentlichte Version der Arbeit ("Lambda-Definierbarkeit in der vollständigen Typenhierarchie" in To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism ) enthält diese Bemerkung. Es gibt auch eine Bemerkung, die als Erklärung des Begriffs "logische Beziehung" ausgelegt werden könnte:

$\lambda$$D$

Meiner Ansicht nach ist dies eine äußerst befriedigende Erklärung dafür, warum logische Beziehungen "logisch" sind. Die Lambda-Rechnung ist logisch und daher sind die damit definierten Funktionen in Bezug auf die Basistypen einheitlich. Sie können die Permutationen, die wir mit den Werten der Basistypen machen, nicht "sehen". So gesehen ist das, was Gordon und Plotkin mit "logisch" meinten, im Wesentlichen dasselbe wie das, was Reynolds "parametrisch" nennt.

Der Begriff "logische Beziehung" erscheint jedoch nicht in der veröffentlichten Version des Papiers. Möglicherweise haben die Schiedsrichter beanstandet, dass der Begriff verwirrend war, und Plotkin hat möglicherweise entschieden, den Begriff am besten zu meiden. Aber Statman kehrte zu der alten Terminologie zurück und der Begriff ist wieder in die Volkssprache zurückgekehrt.

Plotkin verwendete logische Beziehungen in seiner unveröffentlichten, aber dennoch weit verbreiteten und einflussreichen Arbeit "Lambda Definability and Logical Relations" von 1973. Ich habe eine Kopie dieser Notiz auf meiner Webseite.

Früher dachte ich, dass hier der Name herkommt, aber als ich Rick Statman danach fragte, erzählte er mir, dass Mike Gordon den Begriff logische Beziehung zur Beschreibung von Taits Methode geprägt habe und dass er und Gordon Plotkin ihn von ihm aufgegriffen hätten. Ich denke, so wurde der Jargon der Programmiersprache eingegeben, obwohl Sie dies sicherstellen können, indem Sie Plotkin fragen.