一貫した空間

証明理論において、コヒーレント空間（コヒーレンス空間とも呼ばれる）は、線形論理の意味論的研究で導入された概念です。

集合 Cが与えられているとします。2 つの部分集合S、T ⊆ C は、 S ∩ Tが ∅ またはシングルトンである場合、S ⊥ Tと書かれて直交していると言われます。族F ⊆ ℘( C )の双対は、 Fのすべてのメンバーに直交するすべての部分集合S ⊆ Cの族F ^⊥です。つまり、すべてのT ∈ Fに対してS ⊥ Tです。C上のコヒーレント空間Fは、 F = ( F ^⊥ ) ^⊥となるC部分集合の族です。

『証明と型』では、コヒーレント空間はコヒーレンス空間と呼ばれています。脚注には、フランス語の原文では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}}\}}$

コヒーレンス空間は、（無向）グラフと 1 対 1 で対応します（コヒーレンス空間の集合から無向グラフの集合への一対一の意味で）。 に対応するグラフはのウェブと呼ばれ、 はのトークン空間上の反射的な対称関係を誘導するグラフで、は として定義されるコヒーレンス モジュロと呼ばれます。のウェブでは、ノードは からのトークンであり、 のとき、ノードとの間でエッジが共有されます（つまり、 ）。このグラフは各コヒーレンス空間に対して一意であり、特に の要素は のウェブのクリーク、つまり、要素がペアで隣接する（エッジ を共有する）ノードの集合とまったく同じです。 ${\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}).}$

   

安定しているとみなされるためには、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})}$$

は、2 つの引数の安定関数で保存されます。これにより、積空間上の安定な 2 項関数 (2 つの引数の関数) と安定な単項関数 (1 つの引数) の間の一対一関係を作成する積空間の定義が導かれます。積コヒーレンス空間は、カテゴリカルな意味での積です。つまり、積の普遍的性質を満たします。これは、次の式で定義されます。 ${\displaystyle {\mathcal {A}}\ \&\ {\mathcal {B}}}$

• ${\displaystyle |{\mathcal {A}}\ \&\ {\mathcal {B}}|=|{\mathcal {A}}|+|{\mathcal {B}}|=(\{1\}\times |{\mathcal {A}}|)\cup (\{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}}\ベータ '}$
  • ${\displaystyle (1,\alpha )\sim _{{\mathcal {A}}\ \&\ {\mathcal {B}}}(2,\beta ),\forall \alpha \in |{\mathcal { A}}|,\beta \in |{\mathcal {B}}|}$

• ジラール、J.-Y.、ラフォン、Y.、テイラー、P.（1989）、証明と型（PDF）、ケンブリッジ大学出版局。
• Girard, J.-Y. (2004)、「論理と量子の間: 小冊子」、Ehrhard、Girard、Ruet、他編『コンピュータ サイエンスにおける線形論理』(PDF)、ケンブリッジ大学出版局。