Каково происхождение логических отношений?

15

У меня на самом деле есть два вопроса:

  1. Кто первым использовал логические отношения, чтобы связать семантику?

    Я проследил их до Рейнольда « О связи между прямой и семантикой продолжения », но я не могу утверждать, что провел исчерпывающий поиск.

    Я нашел ссылки на логические отношения, датирующиеся ранее (Tait, '67), но не относящиеся к семантике.

  2. Какое настоящее лучшее введение для логических отношений?

Я знаю о « Системах типов для языков программирования » Митчелла из Справочника TCS. Какие еще есть экспозиции?

Охад Каммар
источник
2
В Основах Митчелла для языков программирования есть глава о логических отношениях . Внизу первой страницы дается краткий исторический обзор со ссылкой на основные статьи. Я мог бы напечатать их, если вы не можете достать книгу Митчелла.
Дейв Кларк,
Я могу достать это, спасибо! Я посмотрю, когда доберусь до офиса.
Охад Каммар
Хорошо, книга гораздо более сложна, чем глава из справочника, хотя они охватывают примерно один и тот же материал (к сожалению, без Sconing). Исторические заметки почти идентичны, за исключением того упоминания, которое в книге упоминается в техническом отчете Плоткина NeelK ниже.
Охад Каммар

Ответы:

6

Во втором абзаце Меморандума Плоткина 1973 года о лямбда-определимости и логических отношениях говорится следующее:

«Определение логического [отношения] получено из соответствующего определения М. Гордона для типизированного λ-исчисления».

Это не говорит явно, что термин был придуман Гордоном. Но, учитывая, что меморандум озаглавлен «Лямбда-определимость и логические отношения», как будто «логическое отношение» является уже известной идеей, а второй абзац говорит «построить определенные, так называемые , логические отношения», я думаю, что это очень вероятно что Гордон придумал термин, а Плоткин использовал его отсюда. (Плоткин подтвердил мне, что все, что он написал в записке, является правильным.)

Гордон снова зачислен в верхней части р. 12,

«М. Гордон предложил в качестве возможного средства, что отношения ... должны быть расширены, а не просто перестановки».

В опубликованной версии статьи («Лямбда-определимость в полной иерархии типов» в To HB Curry: очерки о комбинаторной логике, лямбда-исчислении и формализме ) есть это замечание. Он также имеет замечание, которое может быть истолковано как объяснение термина «логическое отношение»:

Из-за «логической» природы -определимых элементов, они должны быть инвариантны относительно перестановок .λD

На мой взгляд, это чрезвычайно удовлетворительное объяснение того, почему логические отношения являются «логическими». Лямбда-исчисление является логичным, и поэтому функции, определенные с его помощью, будут однородными по отношению к базовым типам. Они не могут «видеть» те перестановки, которые мы могли бы сделать со значениями базовых типов. Таким образом, то, что Гордон и Плоткин подразумевали под «логическим», по существу совпадает с тем, что Рейнольдс называет «параметрическим».

Однако термин «логическое отношение» не фигурирует в опубликованной версии статьи. Вполне возможно, что судьи могли возразить, что термин был запутанным, и Плоткин мог бы решить, что лучше избегать этого термина. Но Статман вернулся к старой терминологии, и этот термин снова стал популярным.

Удай Редди
источник
14

Плоткин использовал логические отношения в своей неопубликованной, но, тем не менее, широко распространенной и влиятельной статье 1973 года «Лямбда-определимость и логические отношения». У меня есть копия этой заметки на моей веб-странице.

Раньше я думал, что именно отсюда и произошло название, но когда я спросил об этом Рика Стэтмана, он сказал мне, что Майк Гордон придумал термин логическое отношение, чтобы описать метод Тейта, и что он и Гордон Плоткин взяли его у него. Я думаю, что именно так он вошел в язык программирования жаргон, хотя вы можете убедиться, спросив Плоткина.

Нил Кришнасвами
источник
1
Это почти звучит как сочная сплетня TCS.
Дэйв Кларк
5
Не проси Гордона, просто заставь его участвовать на этом сайте, как я сделал с Даной.
Андрей Бауэр
1
Хорошо, я спросил и Гордона Плоткина, и Майка Гордона. Оба согласны с тем, что Гордон Плоткин придумал термин «логические отношения», и каждый утверждал, что идея использовать отношения пришла от другого.
Охад Каммар
1
Тезис Ганди теперь свободно доступен онлайн: repository.cam.ac.uk/handle/1810/245090
Охад Каммар
2
@OhadKammar: «Лямбда-определимость в полной иерархии типов» Плоткина отдает должное Говарду, говоря, что идея использования отношений, а не перестановок «также использовалась Говардом для определения его наследственно мажорируемых функционалов [Tro]». Цитата в книге, но только глава Говарда является аппендикс «наследственно majorisable функционалы конечного типа»: download.springer.com/static/pdf/314/... (от link.springer.com/book/10.1007 % 2FBFb0066739 ).
Blaisorblade