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

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

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

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

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

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

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

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

Animals = {cat, duck, fish}

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

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

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

• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$
• $\stackrel{{\large\frown}}{{\small\smile}}$

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

Observations$\stackrel{{\large\frown}}{{\small\smile}}$Observations$\stackrel{{\large\frown}}{{\small\smile}}$

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

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

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

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