У меня на самом деле есть два вопроса:
Кто первым использовал логические отношения, чтобы связать семантику?
Я проследил их до Рейнольда « О связи между прямой и семантикой продолжения », но я не могу утверждать, что провел исчерпывающий поиск.
Я нашел ссылки на логические отношения, датирующиеся ранее (Tait, '67), но не относящиеся к семантике.
Какое настоящее лучшее введение для логических отношений?
Я знаю о « Системах типов для языков программирования » Митчелла из Справочника TCS. Какие еще есть экспозиции?
Ответы:
Во втором абзаце Меморандума Плоткина 1973 года о лямбда-определимости и логических отношениях говорится следующее:
Это не говорит явно, что термин был придуман Гордоном. Но, учитывая, что меморандум озаглавлен «Лямбда-определимость и логические отношения», как будто «логическое отношение» является уже известной идеей, а второй абзац говорит «построить определенные, так называемые , логические отношения», я думаю, что это очень вероятно что Гордон придумал термин, а Плоткин использовал его отсюда. (Плоткин подтвердил мне, что все, что он написал в записке, является правильным.)
Гордон снова зачислен в верхней части р. 12,
В опубликованной версии статьи («Лямбда-определимость в полной иерархии типов» в To HB Curry: очерки о комбинаторной логике, лямбда-исчислении и формализме ) есть это замечание. Он также имеет замечание, которое может быть истолковано как объяснение термина «логическое отношение»:
На мой взгляд, это чрезвычайно удовлетворительное объяснение того, почему логические отношения являются «логическими». Лямбда-исчисление является логичным, и поэтому функции, определенные с его помощью, будут однородными по отношению к базовым типам. Они не могут «видеть» те перестановки, которые мы могли бы сделать со значениями базовых типов. Таким образом, то, что Гордон и Плоткин подразумевали под «логическим», по существу совпадает с тем, что Рейнольдс называет «параметрическим».
Однако термин «логическое отношение» не фигурирует в опубликованной версии статьи. Вполне возможно, что судьи могли возразить, что термин был запутанным, и Плоткин мог бы решить, что лучше избегать этого термина. Но Статман вернулся к старой терминологии, и этот термин снова стал популярным.
источник
Плоткин использовал логические отношения в своей неопубликованной, но, тем не менее, широко распространенной и влиятельной статье 1973 года «Лямбда-определимость и логические отношения». У меня есть копия этой заметки на моей веб-странице.
Раньше я думал, что именно отсюда и произошло название, но когда я спросил об этом Рика Стэтмана, он сказал мне, что Майк Гордон придумал термин логическое отношение, чтобы описать метод Тейта, и что он и Гордон Плоткин взяли его у него. Я думаю, что именно так он вошел в язык программирования жаргон, хотя вы можете убедиться, спросив Плоткина.
источник