Можете ли вы объяснить интуицию за когерентными пространствами?

13

Линейная логика интерпретируется с использованием когерентных пространств , и они выделяются в работах Жирара. Я знаю все три основных способа их формального определения, и они на самом деле не представляют проблемы для использования и доказательства чего-либо, но я просто не могу понять, что они имеют в виду .

Такое ощущение, что есть какой-то способ понять их. Прежде всего, есть несколько примеров, которые используют функции на логических значениях (как где-то в вики ). И это намекает на что-то интересное и значимое за формальным определением. Тем не менее, boolэто очень простое связное пространство, без клики размера > 1. Может кто-нибудь уточнить?

Еще одна вещь, где Жирар говорит где-то, что каждая точка связного пространства представляет определенную «последовательность вопросов / ответов», причем две точки являются связными, если они «раздвоены отрицательно (то есть, по разным вопросам)», и несвязными, если они раздвоены при разных ответах [1]. Это кажется легкой для понимания идеей, но я просто не могу придумать пример, так что это означает, что я на самом деле не понимаю ...

Может ли кто-нибудь помочь мне с этим?

[1] JY Girard, Призрак прозрачности . URL: http://iml.univ-mrs.fr/~girard/longo1.pdf

Валя
источник
Вы проверили оригинальную бумагу Girard Linear Logic ?
Каве
@Kaveh Я пролистал (быстро) через него, но, похоже, он не предлагает ничего, чего нет у «Слепого пятна» (которое я читаю) ... У него есть определение, но нет метафоры / интерпретации / объяснения.
Валя
2
Прошло много времени с тех пор, как я смотрел на них, но я думаю, что если вы действительно хотите понять, откуда они берутся, вы должны вернуться к завершению алгебры Хейтинга и семантики Скотта в области интуиционистской логики. Домены (dcpo) обычно используются для выражения частичной информации, два элемента x и y совместимы, если их информация может быть объединена, то есть {x, y} имеет sup. Согласованность - это как раз такая совместимость информации. (Я думаю, что статью «Линейная логика» стоит прочитать, чтобы понять, откуда берутся идеи Жирара.)
Каве
Это звучит о том, что я должен делать с доменами, да ... Спасибо! Я пойду побродить в этом направлении, а затем, если никто не ответит, возможно, однажды я сам напишу ответ.
валя
(И я тоже внимательно посмотрю на бумаге, спасибо - оказывается, я просмотрел не тот)
Валя

Ответы:

10

Интуиция позади пространств когерентности состоит в том, что элементы пространства когерентности представляют наблюдения некоторых базовых данных, а отношение когерентности говорит вам, могли ли два наблюдения поступить из одного и того же фрагмента данных.

Конкретно, предположим, у нас есть набор животных

Animals = {cat, duck, fish}

Теперь мы можем иметь ряд наблюдений:

Observations = {warm-blooded, swims, water-breathing, furry}

Допустим, два наблюдения совместимы, если их можно было бы сделать из одного и того же животного. Каждое наблюдение совместимо с самим собой, а также:

Мы знаем, что теплокровность совместима с плаванием, потому что утки теплокровны и плавают. Но быть теплокровными и дышащими водой несовместимы, так как у нас нет животных, которые были бы теплокровными и дышащими водой.

ObservationsObservations

Нил Кришнасвами
источник
но, как я понимаю, значение типа Observationsбудет кликой, то есть не наблюдением, а набором из них. так это больше похоже [Observation], верно? то же самое с Animals(клики были бы одиночными, но все же) ...
Валя
конечно, даже не совсем [Observation], но все же ... У меня возникли проблемы с поиском примера, в котором не-одиночная клика имела бы смысл
валя
6

У меня всегда были проблемы с формированием интуиции для пространств когерентности, пока я не стал более знакомым с теорией предметной области и не прочитал «Систему F переменных типов Жирара, пятнадцать лет спустя». Пространства когерентности - это просто особый вид области, и я понял, что гораздо проще понять, что означает когерентность, начиная с этого момента. Я постараюсь дать объяснение, которое более или менее имело для меня смысл.

Представьте, что вы хотите изучать программы, которые принимают целочисленные входные значения для целочисленных выходных данных. В общем, эти программы могут работать в цикле навсегда, поэтому имеет смысл математически моделировать их как частичные функции от целых чисел до целых чисел: если программа зацикливается, соответствующая частичная функция на этом входе не определена. Мы можем рассматривать такую ​​частичную функцию fкак граф : набор пар целых чисел, (n, m)таких, которые fопределены nи равны m. Это позволяет нам представлять эти функции как пространство когерентности:

  • Сеть пространства когерентности - это множество пар целых чисел (n, m).
  • Две пары (n, m)и (n', m')когерентны , если и только если nи n'отличаются, или mи m'равны.

Распаковывая определения, мы видим, что каждая клика этого пространства когерентности является графом частичных функций, и наоборот. Мы можем интерпретировать отношение когерентности как следующее: если на входе определена частичная функция, то для этого входа будет получен только один результат. Если вы привыкли к другим видам теоретико-доменной семантики, включение клик соответствует обычному порядку Скотта для частичных функций на целых числах.

Артур Азеведо Де Аморим
источник