日記 (2018 年 2 月 2 日)
最近は、 解析的関手や正規関手とかを用いてラムダ計算のモデルを作ることについて勉強していたりしていなかったりしている。 せっかくなので、 ちょっとずつまとめていこうと思う。
圏
有限の代わりにコンパクトと呼ぶこともある (nLab ではこちらの名称で記事がある) が、 このサイトでは一貫して有限と呼ぶことにする。
集合
圏
- 任意の
に対してa ∈ A は有限集合である。X a - 有限個の
を除いてa ∈ A である。X a = 0
がともに成り立つことである。
これにより、
さて、 これでメインの解析的関手が定義できる。
関手
この解析的関手と密接な関わりがあるのが、 次に定義する弱正規形である。
圏
- 任意の対象
に対してT 。Hom ( S , T ) ≠ 0 - 任意の対象
への射T に対して、 ある同型射f , g : S → T が存在してp : S → S が成り立つ。g = f ∘ p
がともに成り立っているとき、
圏
これらの定義により、
関手
は解析的である。F はフィルター余極限と広義弱引き戻しを保つ。F の任意の対象El ( F ) に対し、 その弱正規形( X , x ) が存在し、f : ( U , u ) → ( X , x ) は有限である。U
は同値である。
Hasegawa†1 を参照。 もしかしたらここにも書くかもしれない。
解析的関手の特殊な場合として、 正規関手というものがある。 ラムダ計算のモデルを作る場合は、 こちらの方が重要になる。
関手
正規関手は、 解析的関手の定義における
解析的関手と弱正規形の間に密接な関係があったように、 正規関手と密接に関係する概念として、 以下に定義する正規形がある。
圏
そして、 以下の定理が知られている。
関手
は正規である。F はフィルター余極限と広義引き戻しを保つ。F の任意の対象El ( F ) に対し、 その正規形( X , x ) が存在し、f : ( U , u ) → ( X , x ) は有限である。U
は同値である。
Hasegawa†1 を参照。
参考文献
- R. Hasegawa (2006) 「Two applications of analytic functors」 『Theoretical Computer Science』 272:113–175