Согласованное пространство

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

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

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

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

Определения

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

• Замыкание вниз: все подмножества множества в ${\mathcal {A}}$ оставаться в ${\mathcal {A}}$: $a'\subset a\in {\mathcal {A}}\implies a'\in {\mathcal {A}}$
• Бинарная полнота: для любого подмножества $M$ из ${\mathcal {A}}$, если попарное объединение любого из его элементов находится в ${\mathcal {A}}$, то таково и объединение всех элементов $M$: $\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)$

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

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

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

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

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

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

1. Он монотонен относительно порядка подмножества ( категорически относится к аппроксимации , является функтором над частично упорядоченным множеством ${\mathcal {A}}$): $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 }}$ это направленный союз над $I$, множество конечных аппроксимаций $a$.
3. Он стабилен : $a_{1}\cup a_{2}\in {\mathcal {A}}\implies F(a_{1}\cap a_{2})=F(a_{1})\cap F(a_{2}).$ Категорически это означает, что откат сохраняется :

   

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

Чтобы считаться стабильными, функции двух аргументов должны удовлетворять критерию 3, приведенному выше, в такой форме: $$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})$$что означало бы, что помимо стабильности каждого аргумента в отдельности, откат

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

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

Ссылки

• Жирар, Ж.-Ю. ; Лафон, Ю.; Тейлор, П. (1989), Доказательства и типы (PDF) , Cambridge University Press .
• Жирар, Ж.-Ю. (2004), «Между логикой и квантовой: трактат», Эрхард; Жирар; Руэт; и др. (ред.), Линейная логика в информатике (PDF) , Издательство Кембриджского университета .