Связное пространство - Coherent space

Для когерентных пространств в топологии см. спектральное пространство.

В теория доказательств, а связное пространство (также пространство когерентности) - это понятие, введенное при семантическом исследовании линейная логика.

Пусть набор C быть данным. Два подмножества S,Т ⊆ C как говорят ортогональный, написано S ⊥ Т, если S ∩ Т или одиночка. В двойной семьи F ⊆ ℘(C) это семья F ^⊥ всех подмножеств S ⊆ C ортогонален каждому члену F, т.е. такие, что S ⊥ Т для всех Т ∈ F. А связное пространство F над C это семья C-подмножества, для которых F = (F ^⊥) ^⊥.-

В Доказательства и типы когерентные пространства называются пространствами когерентности. В сноске поясняется, что, хотя во французском оригинале они были espaces cohérents, перевод пространства когерентности использовался, потому что спектральные пространства иногда называют связными пространствами.

Определения

Как определено Жан-Ив Жирар, а пространство когерентности ${\displaystyle {\mathcal {A}}}$ это собрание наборы удовлетворяющие закрытию вниз и бинарной полноте в следующем смысле:

• Закрытие вниз: все подмножества набора в ${\displaystyle {\mathcal {A}}}$ оставаться в ${\displaystyle {\mathcal {A}}}$: ${\displaystyle a'\subset a\in {\mathcal {A}}\implies a'\in {\mathcal {A}}}$
• Бинарная полнота: для любого подмножества ${\displaystyle M}$ из ${\displaystyle {\mathcal {A}}}$, если попарное объединение любого из его элементов находится в ${\displaystyle {\mathcal {A}}}$, то объединение всех элементов ${\displaystyle M}$: ${\displaystyle \forall M\subset {\mathcal {A}},\left(\forall a_{1},a_{2}\in M,(a_{1}\cup a_{2}\in {\mathcal {A}})\implies \bigcup M\in {\mathcal {A}}\right)}$

Элементы подмножеств ${\displaystyle {\mathcal {A}}}$ известны как жетоны, и они являются элементами множества ${\displaystyle |{\mathcal {A}}|=\bigcup {\mathcal {A}}=\{\alpha |\{\alpha \}\in {\mathcal {A}}\}}$.

Пространства когерентности взаимно однозначно соответствуют (неориентированные) графики (в смысле биекция от множества пространств когерентности к неориентированным графам). График, соответствующий ${\displaystyle {\mathcal {A}}}$ называется сеть из ${\displaystyle {\mathcal {A}}}$ и является ли граф индуцированным рефлексивный, симметричное отношение ${\displaystyle \sim }$ над пространством токенов ${\displaystyle |{\mathcal {A}}|}$ из ${\displaystyle {\mathcal {A}}}$ известный как согласованность по модулю ${\displaystyle {\mathcal {A}}}$ определяется как:

$${\displaystyle a\sim b\iff \{a,b\}\in {\mathcal {A}}}$$

В сети ${\displaystyle {\mathcal {A}}}$, узлы - это токены из ${\displaystyle |{\mathcal {A}}|}$ и край распределяется между узлами ${\displaystyle a}$ и ${\displaystyle b}$ когда ${\displaystyle a\sim b}$ (т.е. ${\displaystyle \{a,b\}\in {\mathcal {A}}}$.) Этот граф уникален для каждого пространства когерентности и, в частности, элементов ${\displaystyle {\mathcal {A}}}$ точно клики сети ${\displaystyle {\mathcal {A}}}$ то есть наборы узлов, элементы которых попарно смежны (разделяют край.)

Пространства когерентности как типы

Пространства когерентности могут действовать как интерпретация типов в теория типов где точки типа ${\displaystyle {\mathcal {A}}}$ точки пространства когерентности ${\displaystyle {\mathcal {A}}}$. Это позволяет обсудить некоторую структуру типов. Например, каждый термин ${\displaystyle a}$ типа ${\displaystyle {\mathcal {A}}}$ может быть дан набор конечных приближений ${\displaystyle I}$ что на самом деле направленный набор с отношением подмножества. С ${\displaystyle a}$ являясь согласованным подмножеством пространства токенов ${\displaystyle |{\mathcal {A}}|}$ (т.е. элемент ${\displaystyle {\mathcal {A}}}$), любой элемент ${\displaystyle I}$ конечное подмножество ${\displaystyle a}$ и, следовательно, также связны, и мы имеем ${\displaystyle a=\bigcup a_{i},a_{i}\in I.}$

Стабильные функции

Функции между типами ${\displaystyle {\mathcal {A}}\to {\mathcal {B}}}$ рассматриваются как стабильный функции между пространствами когерентности. Стабильная функция определяется как функция, которая уважает аппроксимации и удовлетворяет определенной аксиоме устойчивости. Формально, ${\displaystyle F:{\mathcal {A}}\to {\mathcal {B}}}$ стабильная функция, когда

1. это монотонный относительно порядка подмножества (соблюдает приближение, категорически, это функтор над посеть ${\displaystyle {\mathcal {A}}}$): ${\displaystyle a'\subset a\in {\mathcal {A}}\implies F(a')\subset F(a).}$
2. это непрерывный (категорически сохраняет отфильтрованные копределы ): ${\textstyle F(\bigcup _{i\in I}^{\uparrow }a_{i})=\bigcup _{i\in I}^{\uparrow }F(a_{i})}$ куда ${\textstyle \bigcup _{i\in I}^{\uparrow }}$ это направленный союз над ${\displaystyle I}$, множество конечных аппроксимаций ${\displaystyle a}$.
3. это стабильный: ${\displaystyle a_{1}\cup a_{2}\in {\mathcal {A}}\implies F(a_{1}\cap a_{2})=F(a_{1})\cap F(a_{2}).}$ Категорически это означает, что он сохраняет откат:
   

Пространство продукта

Чтобы считаться стабильными, функции двух аргументов должны удовлетворять критерию 3 выше в следующей форме:

$${\displaystyle a_{1}\cup a_{2}\in {\mathcal {A}}\land b_{1}\cup b_{2}\in {\mathcal {B}}\implies F(a_{1}\cap a_{2},b_{1}\cap b_{2})=F(a_{1},b_{1})\cap F(a_{2},b_{2})}$$

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

сохраняется с устойчивыми функциями двух аргументов. Это приводит к определению пространства продукта. ${\displaystyle {\mathcal {A}}\ \&\ {\mathcal {B}}}$ который делает взаимно однозначное соответствие между стабильными бинарными функциями (функциями двух аргументов) и стабильными унарными функциями (одним аргументом) в пространстве произведения. Пространство когерентности продукта - это продукт в категориальном смысле т.е. удовлетворяет универсальная собственность для продуктов. Он определяется уравнениями:

• ${\displaystyle |{\mathcal {A}}\ \&\ {\mathcal {B}}|=|{\mathcal {A}}|+|{\mathcal {B}}|=\{1\}\times |{\mathcal {A}}|+\{2\}\times |{\mathcal {B}}|}$ (т.е. набор жетонов ${\displaystyle {\mathcal {A}}\ \&\ {\mathcal {B}}}$ является побочным продуктом (или несвязный союз ) наборов токенов ${\displaystyle {\mathcal {A}}}$ и ${\displaystyle {\mathcal {B}}}$.
• Токены из разных наборов всегда согласованы, а токены из одного набора согласованы именно тогда, когда они согласованы в этом наборе.
  • ${\displaystyle (1,\alpha )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(1,\alpha ')\iff \alpha \sim _{\mathcal {A}}\alpha '}$
  • ${\displaystyle (2,\beta )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(2,\beta ')\iff \beta \sim _{\mathcal {B}}\beta '}$
  • ${\displaystyle (1,\alpha )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(2,\beta ),\forall \alpha \in |{\mathcal {A}}|,\beta \in |{\mathcal {B}}|}$

Рекомендации

• Жирар, Ж.-Й.; Lafont, Y .; Тейлор, П. (1989), Доказательства и типы (PDF), Издательство Кембриджского университета.
• Жирар, Ж.-Й. (2004), «Между логикой и квантичностью: трактат», в Эрхарде; Жирар; Рует; и другие. (ред.), Линейная логика в информатике (PDF), Издательство Кембриджского университета.
• Джонстон, Питер (1982), «II.3 Связанные места», Каменные Пространства, Cambridge University Press, стр. 62–69, ISBN  978-0-521-33779-3.