Что такое народная модель линейной логики?

23

Вероятно, наиболее распространенным применением линейных типов в PL является использование их для предоставления языков, которые управляют псевдонимами (т. Е. Линейное значение имеет единственный указатель на него, более или менее).

Но есть небольшое несоответствие между этим использованием и типичными денотационными моделями линейной логики. IIRC, Бентон показал, что если декартова замкнутая категория имеет сильную коммутативную монаду, то ее категория алгебр будет симметричной моноидально замкнутой (т. Е. Модель линейной логики). Но эта теорема неприменима к использованию управления псевдонимами, поскольку монада состояния не является коммутативной. И действительно, в последние несколько лет Симпсон и его коллеги дали исчисления для общих сильных монад, которые не являются исчислениями термина для линейной логики.

Итак, мой вопрос: что такое денотационная семантика линейных языков с состоянием? Существует ли невырожденная (т. Е. Тензор не декартова произведение) симметричная моноидальная замкнутая категория, в которой можно моделировать распределение, чтение и линейное обновление?

Нил Кришнасвами
источник
6
Это тот вопрос, который я ожидаю, что вы ответите Нилу, а не зададите его. ;-)
Марк Хаманн
5
Если вы сможете привлечь к cstheory.stackoverflow.com исследователей, способных ответить на этот вопрос, тогда мир станет для этого лучшим местом.
Дэйв Кларк

Ответы:

9

Мне кажется, что направление, которое вы должны рассмотреть, вращается вокруг семантики игры для общих ссылок и связанной семантики для линейной логики, такой как основанная на играх Конвея . Алгебраическое изложение ссылок в семантике игры Пола-Андре Мельеса и Николя Табаро, вероятно, является лучшим местом для начала. В этой статье линейная логика смягчается так называемой тензорной логикой, чтобы заставить вещи работать, поэтому это не совсем тот параметр, который вам нужен. Но они полагаются на игры Конвея, поэтому, безусловно, существует связь с моделями линейной логики. Они также на самом деле не используют линейность, как в линейных типах, но, я полагаю, есть механизм для этого, если вы хотите.

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

Дэйв Кларк
источник
1
Просто любопытный Нил. Было ли это вам полезно, или вы уже знали обо всем этом?
Дейв Кларк
Я знаю это (но не очень хорошо), но семантика игры намного сложнее, чем я ищу. У большинства людей есть интуиция для линейного состояния, которая находится недалеко от старомодного представления Стрейчи об императивных вычислениях как элемент монадического типа , и я надеялся, что существует модель линейное состояние, которое будет напоминать это. По сути, я надеялся, что есть кое-что, что вы могли бы показать первокурснику, не испугав их. :)T(A)=SA×S
Нил Кришнасвами
1
Возможно, глобальное состояние Uday Reddy считается ненужным: введение в семантику на основе объектов, J. Lisp and Symbolic Computing, 9 (1996): 7-76.
Дэйв Кларк
Я читаю это сейчас, на самом деле!
Нил Кришнасвами
7

(Гоша, Нил, это был сложный вопрос.)

«Народная модель» линейной логики, безусловно, является моделью связного пространства, обсуждаемой в статье Жирара «Линейная логика» (а также в «Доказательствах и типах»). Это не вырожденный в том смысле, который вы описываете.

Я не уверен, что эта семантика проливает свет на то, как можно реализовать линейный функциональный язык. Когда вы говорите о распределении, чтении и линейном обновлении, вы действительно говорите о реализации. Так что, возможно, ваш вопрос можно сформулировать так: «Как мне доказать правильность реализации линейного функционального языка, использующего обновление состояния?» Я не знаю ответа на этот вопрос, но я думаю, что он должен существовать в статьях, предлагающих реализации линейного обновления.

Удай Редди
источник
На самом деле, доказать правильность реализаций линейного состояния слишком просто - линейность - это такое сильное структурное ограничение, что вам вряд ли понадобится какая-либо семантика для выполнения этих доказательств. В результате я не знаю простой денотационной семантики линейного состояния. Две самые близкие вещи к тому, что я хочу, - ваша работа над объектно-ориентированной семантикой и модель «пространств длины» Хофмана в его работе по неявной сложности.
Нил Кришнасвами
На самом деле, я бы не описал объектную семантику как моделирование «линейного состояния». Это скорее «последовательное состояние» и «линейные объекты», латте навязывается SCI. Модели игр Idealized Algol, которые также являются «объектно-ориентированными» в том же смысле, не имеют линейного представления.
Удай Редди
Можете ли вы дать некоторые ссылки, где можно найти такие доказательства правильности? (Извините, переворачиваю вопрос на вас!)
Uday Reddy
1
Самым простым доказательством правильности для линейного языка с состоянием, которое я знаю, является «L3: Линейный язык с локациями» Ахмеда, Флуэта и Морисетта. ( ttic.uchicago.edu/~amal/papers/linloc-fi07.pdf ) В статье они дают простое логическое соотношение, но упоминают, что синтаксическое доказательство прогресса и сохранения также проходит.
Нил Кришнасвами
Вот еще одна работа, которая только что привлекла мое внимание. Попробуйте citeseer для Стивена Купера, ссылка «О линейных типах и обязательном обновлении» . Я должен был знать об этом, но не знал.
Uday Reddy