日記 (2018 年 2 月 2 日)

最近は、 解析的関手や正規関手とかを用いてラムダ計算のモデルを作ることについて勉強していたりしていなかったりしている。 せっかくなので、 ちょっとずつまとめていこうと思う。

定義 1.1.

󰒚 の対象 S に対し、 表現可能関手 Hom󰒚(S,-):󰒚Set がフィルター余極限を保存するとき、 S有限 (finite) であるという。 圏 󰒚 の有限対象全体は Fin(󰒚) で表す。

有限の代わりにコンパクトと呼ぶこともある (nLab ではこちらの名称で記事がある) が、 このサイトでは一貫して有限と呼ぶことにする。

集合 A を離散圏だと見なして関手圏 SetA を考えれば、 これは A を添字集合とする集合族が成す圏になる。 この形の圏は、 解析的関手を用いてラムダ計算や論理のモデルを作るときにかなり重要になる。 SetA の有限対象については、 以下のことが知られている。

定理 1.2.

SetA の対象 X が有限であるための必要十分条件は、 2 条件

がともに成り立つことである。

これにより、 SetA の有限対象は A の元から成る有限多重集合と (同型の違いを除いて) 同一視することができる。 したがって、 今後は SetA の有限対象を {a1,a1,a2} のように表すことがある。 これは、 {a1,a1,a2}: A Set a { 2 (a=a1) 1 (a=a2) 0 (上記以外) のことである。

さて、 これでメインの解析的関手が定義できる。

定義 1.3.

関手 F:󰒚Set を考える。 ある添字集合 I が存在し、 各 iI に対して 󰒚 の有限対象 Si と部分群 KiAut󰒚(Si) が存在して、 X󰒚 に対し、 FX󰄘iIKi\Hom󰒚(Si,X) と表せるとする。 このとき、 F解析的 (analytic) であるという。 ここで、 Ki\Hom󰒚(Si,X) は左からの群作用 Ki×Hom󰒚(Si,X) Hom󰒚(Si,X) (p,f) fp1 による商集合である。

この解析的関手と密接な関わりがあるのが、 次に定義する弱正規形である。

定義 1.4.

󰒚 の対象 S が、 2 条件

がともに成り立っているとき、 S推移的 (transitive) であるという。

定義 1.5.

󰒚 の射 f:UX に対し、 f をスライス圏 󰒚/X の対象と見なすと推移的であるとき、 fX弱正規形 (weak normal form) という。

これらの定義により、 SetA からの解析的関手は以下のように特徴付けられる。 ここで、 広義引き戻しとは、 通常の引き戻しとは異なり、 極限をとる射が 2 本とは限らないものである。 また、 広義弱引き戻しとは、 通常の広義引き戻しでは一意に定まる普遍性から得られる分解射の、 一意性を仮定しないものである。

定理 1.6.

関手 F:SetASet について、 3 条件

は同値である。

証明.

Hasegawa†1 を参照。 もしかしたらここにも書くかもしれない。

解析的関手の特殊な場合として、 正規関手というものがある。 ラムダ計算のモデルを作る場合は、 こちらの方が重要になる。

定義 1.7.

関手 F:󰒚Set を考える。 ある添字集合 I が存在し、 各 iI に対して 󰒚 の有限対象 Si が存在して、 X󰒚 に対し、 FX󰄘iIHom󰒚(Si,X) と表せるとする。 このとき、 F正規 (normal) であるという。

正規関手は、 解析的関手の定義における Ki たちを全て単位群にしたものである。

解析的関手と弱正規形の間に密接な関係があったように、 正規関手と密接に関係する概念として、 以下に定義する正規形がある。

定義 1.8.

󰒚 の射 f:UX に対し、 f をスライス圏 󰒚/X の対象と見なすと始対象であるとき、 fX正規形 (normal form) という。

そして、 以下の定理が知られている。

定理 1.9.

関手 F:SetASet について、 3 条件

は同値である。

証明.

Hasegawa†1 を参照。

SetA という形の圏とその間の正規関手を考えることでカルテシアン閉圏を構成することができ、 カルテシアン閉ならいろいろなラムダ計算のモデルが作れるよねというのが今後の話である。 続きはまた後日に書きたい。

参考文献

  1. R. Hasegawa (2006) 「Two applications of analytic functors」 『Theoretical Computer Science』 272:113–175