日記 (2021 年 2 月 1 日)

整合空間は、 線型論理の創始者でもある Girard によって、 線型論理の表示的意味論を与えるために導入されたものである。 この日記シリーズでは、 整合空間とその間の射である安定写像について軽く議論しつつ、 整合空間が成す圏について考察し、 最終的に線型論理との関係について触れるつもりである。

まず、 整合空間を定義する。

定義 1.1.

集合から成る集合 A が、 2 条件

  1. 任意の aA に対し、 a󰎘a ならば a󰎘A が成り立つ。
  2. 任意に部分集合 SA をとり、 任意の 2 元 a,a󰎘Saa󰎘A を常に満たすとする。 このとき、 SA が成り立つ。

を満たすとする。 このとき、 A整合空間 (coherence space) という。

Girard の慣習に従って、 整合空間の元は小文字で書く。 しかし、 整合空間の元は集合なのでそこからさらに元をとることもできるし、 整合空間の元同士で合併などを計算することもできることには注意すること (数学が基礎としているところの集合論では全ては集合なので当たり前なのだが)。

整合空間の定義に関していくつか注意を述べておく。 まず、 2 つ目の項目で部分集合 SA に課された条件は、 任意の 2 元 a,a󰎘S に対して aa󰎘A に属していれば良く S に属する必要はないので、 単に S が有向であるということよりも強い条件である。 また、 この項目において S= とおくことで、 A であることが分かる。

整合空間は、 反射的無向グラフとも見なすことができる。 ここで、 反射的無向グラフとは、 グラフ理論における (2 頂点の間の辺が高々 1 本である) 無向グラフであって、 全ての頂点に対して自分自身から自分自身への辺が存在するものである。 すなわち、 頂点が成す集合と、 頂点が辺で結ばれていることを表す反射的かつ対称な二項関係の組である。 以降はこの見方をし、 反射的無向グラフと言ったら、 何らかの集合とその上の反射的かつ対称な二項関係の組を表すものとする。

定義 1.2.

整合空間 A に対し、 |A|:={x{x}A} と定義し、 |A| 上の二項関係 󰖬 を、 x󰖬x󰎘:⟺{x,x󰎘}A で定める。 このとき、 反射的無向グラフ (|A|,󰖬)A (web) といい、 web(A) で表す。

整合空間からその網を得る操作は可逆である。 この逆の操作は、 反射的無向グラフのクリーク全体をとることで実現される。

定義 1.3.

反射的無向グラフ (G,󰖬) の頂点から成る集合 aG を考える。 任意の 2 頂点 x,x󰎘a に対して x󰖬x󰎘 が成り立つとき、 aGクリーク (clique) という。 G のクリーク全体の集合を clique(G) で表す。

命題 1.4.

整合空間からその網を得る操作と、 反射的無向グラフからそのクリーク全体の集合をとる操作は、 互いに逆である。 すなわち、 全単射 {整合空間} {反射的無向グラフ} A web(A) clique(G) G が存在する。

証明.

容易である。

以上のことから、 整合空間を定義するには、 定義 1.1 の 2 条件を満たす集合を与えるか、 反射的無向グラフを与えるかすれば良い。 また、 与えられた整合空間の元を 1 つ与えるのと、 その整合空間の網のクリークを 1 つ与えるのは同じことである。 以降、 整合空間とその網は断りなく同一視する。

いくつか用語を定義しておこう。

定義 1.5.

整合空間 A に対し、 以下のように用語を定める。

さらに、 |A| 上の関係 󰖫,󰖪, を、 x󰖫x󰎘 :⟺ x󰖬x󰎘ANDxx󰎘 x󰖪x󰎘 :⟺ x󰖬̸x󰎘 xx󰎘 :⟺ x󰖬̸x󰎘ORx=x󰎘 で定め、 これらを満たすトークンをそれぞれ狭義整合的 (strictly coherent), 狭義非整合的 (strictly incoherent), 非整合的 (incoherent) であるという。

この用語を用いれば、 整合空間の網のクリークとは、 その整合空間のトークンから成る整合的な集合のことである。 したがって、 整合空間の元を 1 つ与えることは、 トークンから成る整合的な集合を 1 つ与えることだと言い換えることもできる。

次に、 整合空間の間の射となる安定写像を定義する。

定義 1.6.

整合空間 A,B の間の写像 f:AB が、 3 条件

  1. 任意の a,a󰎘A に対し、 aa󰎘 ならば f(a)f(a󰎘) が成り立つ。
  2. 任意の有向部分集合 SA に対し、 f(aSa)=aSf(a) が成り立つ。
  3. 任意の a,a󰎘A に対し、 aa󰎘A ならば f(aa󰎘)=f(a)f(a󰎘) が成り立つ。

を満たすとき、 f安定 (stable) であるという。 また、 これらの条件をそれぞれ単調性 (monotonicity), 連続性 (continuity), 安定性 (stability) という。

単調性と連続性は、 Scott 領域の間の射を定義するときも使われているよく知られた条件である。 整合空間の安定写像の定義には安定性が追加で課されているが、 この安定性が整合空間の理論において非常に重要な役割を果たすことが知られている。

なお、 有向部分集合 SA に対して、 f(aSa)=aSf(a) が成り立つことが aSf(a)B であることを含意していることを踏まえると、 連続性から単調性が従うことが分かる。 したがって、 写像が安定であることの定義に単調性と連続性を両方課すのは冗長である。 しかし、 ある写像が安定であることを示す際、 たいていの場合で単調性が自明で、 連続性を示すときに単調性を使うことが多いため、 ここでは単調性と連続性を両方を条件として書いた。

すでに述べたように、 任意の整合空間には が元として属するが、 安定写像が を保存する必要はない。 これを条件として課さないのは、 領域理論において Scott 連続関数に最小元の保存を課さないのと同じ理由で、 不動点を考える際に不都合が生じるからである。

安定写像についてまず分かることととして、 これは合成に関して閉じている。

命題 1.7.

整合空間 A,B,C および写像 f:AB,g:BC をとる。 fg がともに安定ならば、 gf も安定である。

証明.

gf が上記の 3 条件を満たすことを示せば良いが、 単調性は明らかなので、 連続性と安定性を示す。

gf の連続性を示す。 任意の有向部分集合 SA に対し、 まず f が安定だから f(aSa)=aSf(a) が成り立つ。 ここで、 T:={f(a)aS} が有向であることが示されれば、 g が安定であることから、 g(aSf(a))=g(bTb)=bTg(b)=aSg(f(a)) が成り立つので、 最初の式と合わせて g(f(aSa))=aSg(f(a)) が得られる。 したがって、 T が有向であることを示せば良い。 任意の a,a󰎘S に対し、 S の有向性によって a󰔄a かつ a󰎘󰔄a を満たすような 󰔄aS が存在する。 このとき、 f の単調性から f(a)f(󰔄a) かつ f(a󰎘)f(󰔄a) が成り立つ。 したがって、 T は有向である。

次に、 gf の安定性を示す。 任意の a,a󰎘A であって aa󰎘A を満たすものをとる。 f の安定性から f(aa󰎘)=f(a)f(a󰎘) が成り立つ。 また、 f の単調性から f(a)f(aa󰎘) および f(a󰎘)f(aa󰎘) が成り立つから、 f(a)f(a󰎘)f(aa󰎘) が得られる。 ここで、 B は整合空間であって f(aa󰎘)B だから、 f(a)f(a󰎘)B が分かる。 したがって、 g の安定性から g(f(a)f(a󰎘))=g(f(a))g(f(a󰎘)) が成り立つ。 最初に得られた式と合わせて、 g(f(aa󰎘))=g(f(a))g(f(a󰎘)) を得る。

これにより、 整合空間と安定写像は圏を成すので、 以降これを Coh で表す。

次回から何回かに分けて、 Coh の積と冪の具体的な形を与えることで Coh がカルテシアン閉であることを示す。 さらに、 積とは異なる演算を与えて、 その演算に関して Coh がモノイダル閉であることも示す。

参考文献

  1. J. Y. Girard (1987) 「Linear logic」 『Theoretical Computer Science』 50:1–101
  2. J. Y. Girard, Y. Lafont, P. Taylor (1989) 『Proofs and Types』 Cambridge University Press