日記 (2021 年 2 月 1 日)
整合空間は、 線型論理の創始者でもある Girard によって、 線型論理の表示的意味論を与えるために導入されたものである。 この日記シリーズでは、 整合空間とその間の射である安定写像について軽く議論しつつ、 整合空間が成す圏について考察し、 最終的に線型論理との関係について触れるつもりである。
まず、 整合空間を定義する。
集合から成る集合
- 任意の
に対し、a ∈ A ならばa ⊆ a が成り立つ。a ∈ A - 任意に部分集合
をとり、 任意の 2 元S ⊆ A がa , a ∈ S を常に満たすとする。 このとき、a ∪ a ∈ A が成り立つ。⋃ S ∈ A
を満たすとする。
このとき、
Girard の慣習に従って、 整合空間の元は小文字で書く。 しかし、 整合空間の元は集合なのでそこからさらに元をとることもできるし、 整合空間の元同士で合併などを計算することもできることには注意すること (数学が基礎としているところの集合論では全ては集合なので当たり前なのだが)。
整合空間の定義に関していくつか注意を述べておく。
まず、 2 つ目の項目で部分集合
整合空間は、 反射的無向グラフとも見なすことができる。 ここで、 反射的無向グラフとは、 グラフ理論における (2 頂点の間の辺が高々 1 本である) 無向グラフであって、 全ての頂点に対して自分自身から自分自身への辺が存在するものである。 すなわち、 頂点が成す集合と、 頂点が辺で結ばれていることを表す反射的かつ対称な二項関係の組である。 以降はこの見方をし、 反射的無向グラフと言ったら、 何らかの集合とその上の反射的かつ対称な二項関係の組を表すものとする。
整合空間
整合空間からその網を得る操作は可逆である。 この逆の操作は、 反射的無向グラフのクリーク全体をとることで実現される。
反射的無向グラフ
整合空間からその網を得る操作と、 反射的無向グラフからそのクリーク全体の集合をとる操作は、 互いに逆である。
すなわち、 全単射
容易である。
以上のことから、 整合空間を定義するには、 定義 1.1 の 2 条件を満たす集合を与えるか、 反射的無向グラフを与えるかすれば良い。 また、 与えられた整合空間の元を 1 つ与えるのと、 その整合空間の網のクリークを 1 つ与えるのは同じことである。 以降、 整合空間とその網は断りなく同一視する。
いくつか用語を定義しておこう。
整合空間
の元を| A | のトークン (token) という。A - トークン
に対し、 上で定まる関係x , x ∈ | A | について が成り立つとき、x x とx は整合的 (coherent) であるという。x - 部分集合
に対し、a ⊆ | A | の任意の 2 元が整合的であるとき、a 自身も整合的 (coherent) であるという。a
さらに、
この用語を用いれば、 整合空間の網のクリークとは、 その整合空間のトークンから成る整合的な集合のことである。 したがって、 整合空間の元を 1 つ与えることは、 トークンから成る整合的な集合を 1 つ与えることだと言い換えることもできる。
次に、 整合空間の間の射となる安定写像を定義する。
整合空間
- 任意の
に対し、a , a ∈ A ならばa ⊆ a が成り立つ。f ( a ) ⊆ f ( a ) - 任意の有向部分集合
に対し、S ⊆ A が成り立つ。f ( ⋃ a ∈ S a ) = ⋃ a ∈ S f ( a ) - 任意の
に対し、a , a ∈ A ならばa ∪ a ∈ A が成り立つ。f ( a ∩ a ) = f ( a ) ∩ f ( a )
を満たすとき、
単調性と連続性は、 Scott 領域の間の射を定義するときも使われているよく知られた条件である。 整合空間の安定写像の定義には安定性が追加で課されているが、 この安定性が整合空間の理論において非常に重要な役割を果たすことが知られている。
なお、 有向部分集合
すでに述べたように、 任意の整合空間には
安定写像についてまず分かることととして、 これは合成に関して閉じている。
整合空間
次に、
これにより、 整合空間と安定写像は圏を成すので、 以降これを
次回から何回かに分けて、
参考文献
- J. Y. Girard (1987) 「Linear logic」 『Theoretical Computer Science』 50:1–101
- J. Y. Girard, Y. Lafont, P. Taylor (1989) 『Proofs and Types』 Cambridge University Press