このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

自然演繹のための構成法

  1. Cは一般的なモノイド圏、X = (X, δ, ε)がC内の余モノイド(余モノイド構造、余モノイド対象)のとき、Xのスタンピング関手(域側に掛け算する)から余モナドが定義できる。
  2. 上記の余モナドの余クライスリ圏を作れる。これは一般的な構成。
  3. モナドテンソル強度(余テンソル強度)を持つとき、余クライスリ圏がプレモノイド圏になる。特に可換余モナドなら余クライスリ圏はモノイド圏となる。
  4. Cデカルト圏なら、すべての対象が余モノイドになる。したがって、余クライスリ圏が作れる。
  5. それだけではなくて、スタンピング余モナドが可換余モナドとなるので、余クライスリ圏はモノイド圏となる。
  6. さらに、そのモノイド積はデカルト・モノイド積なので、出来た余クライスリ圏はデカルト圏となる。
  7. 与えられたデカルト圏から余クライスリ・デカルト圏を作る構成法は、CartCatCartCatという関手になる。この構成に特に名前がないのでB-構成と呼ぶことにする。
  8. B-構成は、{環境 | 文脈 | 背景}付き計算の定式化になっている。
  9. B-構成で使うXを動かすと、C上のCartCat値のインデックス付き圏が出来る。これはインデックス付きB-構成〈indexed B-construction〉。
  10. そのグロタンディーク平坦化も出来る。