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

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

ローヴェル・フレームワーク

高次圏論 プログラム意味論 まとめ セオリー論

代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編 の続きで、ローヴェル・セオリーを可能とするフレームワークについて。

ローヴェル・セオリー

ローヴェル・セオリーの導入・説明では、有限集合の圏FinSetの骨格として、基数（それ自身集合）の集合アレフ0を取り、基数のあいだの写像からなるSet充満部分圏を考える。が、これは分かりにくい。次のfinを代わりに使う。

  • |fin| = N
  • fin(n, m) := Set([n], [m])

Nを対象類とする圏とidentity-on-objects関手の圏Cat[N]を考える。a:fin→A in Cat[N] が有限積を厳密に保存するとき、(A, a)をローヴェル・セオリーと呼ぶ。Aはセオリーの台圏、aはセオリーの構造射（関手）。

ローヴェル・セオリーは、単ソート有限積セオリーなので、アンビエントとして有限積圏〈category with finnite product〉の圏FPCatを考える。FPCatはCat上の具象2-圏で、

  1. 対象は有限積圏
  2. 射は、有限積をタイトに保存する関手（厳密でなくてもよい）
  3. 2-射は、自然変換

このケースでは、FPCatが1-アンビエント〈1-ドクトリン | 1-宇宙 | 1-レルム〉で、1-圏を対象に持ち、それ自身は2-圏。厳密に積を保存する関手からなる部分2-圏はFPCatstrとする。FPCatstrは、役割としては厳密アンビエント、またはファーム・アンビエント〈firm ambient〉。

finは、アンビエント内でのコア対象〈core object〉。コア対象は、アンビエントが2-モナドTのEM代数だとして、2-モナドTの単位対象1 = 1(2)0 による像。

  • fin = T(1)

単一の対象からなる自明な圏から、Tにより生成されるアンビエント内対象がfin。

アンビエントのコア対象からの関手で、ファーム（厳密）で対象を動かさない（identity-on-objects）射を構造射として持つアンビエント内対象（1-圏）がローヴェル・セオリー。

  • Law = fin/(FPCat[N])str

ローヴェル・セオリーは、0-射記号＝ソートを1つだけ持つ定義形式〈指標 | 仕様〉で定義される。この定義形式には、1-生成射も2-生成射（等式）も無限個（可算無限個）を許す。したがって、可算無限個までの0-生成射、1-生成射、2-生成射を許す代数的定義形式はセオリーと呼んでも問題ない。コア対象からのファーム相対対象（オーバー圏の対象）と単一ソートの定義形式が対応し、どちらもセオリーと呼んでよい。

  1. コア対象の下の相対圏としてのセオリー
  2. 単ソートで、可算無限の1, 2-構成素を持つ1-定義形式としてのセオリー

次の関係がある。

  1. セオリー指標からローヴェル・セオリー圏を作れる。
  2. すべてのローヴェル・セオリー圏は、適当な指標から作られる。ローヴェル・セオリー圏Aを生成する指標を（役割として）Aのプレゼンテーションと呼ぶ。

セオリーのモデル

ローヴェル・セオリー (A, a) があると、台圏Aは1-アンビエントであるFPCatの対象である。よって、同じFPCat内の対象である有限積圏Cへの射（有限積保存関手）M:A→C は定義できる。これが(A, a)のモデル。Cをセマンティック圏と呼ぶのは定義形式のモデルのときと同じ。

セマンティック圏を固定すると、セオリーとセオリー射の圏は、Law = fin/(Cat[N])str、この圏をベース圏〈インデキシング圏〉として、モデルの圏をファイバーとするインデックス付き圏が作れる。

さらにセマンティック圏も動かすと、セオリーの圏の対象と、アンビエント圏の対象をパラメータとする双加群ができる。これはセオリーの圏を底領域、アンビエント圏を指数領域とする指数演算だと思われる。底の役割を持つ対象（1-圏）をセマンティック圏と呼ぶことになる。指数（肩）の役割がセオリー。

モデルは指数なので、底であるセマンティック圏に関しては共変に動き、指数（肩）であるセオリーに関しては反変に動く。

ローヴェル・フレームワーク

ローヴェル・セオリーには次の登場者がいる。

  1. 1-アンビエントであるFPCat、有限積を持つ圏の圏（それ自体は2-圏）。
  2. 1-アンビエントは、とある2-モナドのアイレンベルグ／ムーア2-圏なので、1-アンビエントを生じさせる2-モナドT。TはCat上に働く2-モナドで、有限積を持つ圏を自由生成する。
  3. 1-アンビエント＝EM(Cat, T) 内のコア対象。コア対象は常にT(1)で定義される。
  4. コア対象（と呼ばれる圏）と同じ対象類を持つ圏と、ファーム関手を射とする圏。この圏の対象と射が、セオリーの構成素となる。

このなかで、一番の基本は2-モナドT、Tがあれば、次のようにして他のモノを作れる。

  1. EM(Cat, T)としてアンビエントを作る。
  2. T(1)としてコア対象を作る。
  3. コア対象を含む、アンビエントの部分圏であるファーム部分圏を作る。
  4. ファーム部分圏内で、コア対象のアンダー圏を作ることによりセオリーの圏を作る。

Cat上の2-モナドと、Set上の1-モナドの組み合わせで、構造を持つ圏内に作れる構造を持つ対象（集合）を定義することがローヴェル・セオリーの理論であり、それを可能とするセッティングをローヴェル・フレームワークと呼ぶ。

ローヴェル・セオリーのハイライト

セオリーの射（関手） T→T' は、反変的にCモデル圏の関手 [T', C]→[T, C] を導く。これは、（一般化された）忘却関手と考えてよい。

  • （一般化された）忘却関手には左随伴が存在して、（一般化された）自由生成関手となる。
  • 忘却・自由生成の随伴ペアからモナドとコモナドを作れる。
  • C = Set とすると、集合モデル [T, Set] から、Tを再現できる。

自然演繹とシーケント計算の解釈

論理 圏一般論

困った時の米田頼み、ご利益ツールズ - 檜山正幸のキマイラ飼育記 で述べたこと：

自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出来そうではありますが、バシッと決められないもどかしさを感じてました。

今まで米田頼みをしたことがなかったのですが、「ひょっとしたら」と思って米田埋め込みを探してみました。… ありましたね(ニコ)。これでたぶん、バシッと決められます。でも、今日この話はしません。まだ詰め切れてないので、もう少し考えてからにします。

これだけど、何の記録もないので忘れるかも、、、、ヤバイ。

Cが自然演繹のモデルとなっているデカルト閉圏だとする。これに対して、シーケント計算のモデルはどうなるかという話。端的に結論を言ってしまうと、（たぶん）自己プロ関手の圏Prof(C, C) = EndProf(C) だろう。以下、EndProf(C) を EndProf(C)と書く。

CをEndProf(C)に埋め込む方法は色々ある。H∈EndProf(C)を単位元に相当するCのホム双関手だとすると、H(-, T), H(-, ⊥), H(T, -), H(⊥, -) などが埋め込みの例。しかし、

  • CをEndProf(C)に埋め込む標準的な方法はない。

この事実が、自然演繹（C）とシーケント計算（EndProf(C)）の関係を分かりにくくしている。

しかし、EndFunc(C)を自己関手圏Cat(C, C)とすると、EndFunc(C)の非対称モノイド圏構造も含めて、EndProf(C)に埋め込める。

  • EndFunc(C)をEndProf(C)に埋め込む標準的な方法がある。

よって、Cの対象である命題や、Cの射である（自然演繹の）証明をそのままシーケント計算に持っていくのはうまくなくて、いったんEndFunc(C)で解釈してから、素直にEndProf(C)に入れる。例えば、命題＝対象ならば、直積によりスタンピング関手としてから、EndProf(C)で解釈する。

そもそも、自然演繹は、C内での解釈は（出来るが）不自然で、証明図は射ではなくて、自然変換の成分表示になっている、と解釈すべき。

  • Cの射は、証明のインスタンスである。
  • Cの自然変換は、証明のパターン＝テンプレートである。

自然演繹の推論図とは、EndFunc(C)の構成的部分圏を生成するための生成1-射〈generating 1-morphism〉である。1-射＝自然変換なので、結局、「推論図＝生成自然変換」となる。

現状の説明（僕自身の説明も含めて）だと、パターンとパターンのインスタンスの区別がついてない。

パターン インスタンス
対象 対象変数 実際の対象（個別具体的命題）
射 自然変換 自然変換の特定成分
射の結合 自然変換の縦横結合 射の結合（横のみ）
射の直積 自然変換の直積 射の直積

EndFunc(C)は、Cが直積を持つことから、関手の直積と自然変換の直積を持つモノイド2-圏となる。

EndProf(C)もモノイド2-圏となる。したがって、自然演繹からシーケント計算への埋め込みは、モノイド2-圏の構造を保つようなモノイド2-関手によって行われる。

EndProf(C)には、Cop×Cが両側加群として働くが、EndFunc(C)op×EndFunc(C)も働く。自己関手モノイド圏が自己プロ関手モノイド圏に左右から働くような構図。この両側加群構造があるので、自然演繹とシーケント計算を混ぜて使うことが出来る。

さらに証明図（パターン）の変形は自然変換のあいだの変更〈modification〉になるので、3-圏が必要になる。そればかりか、高次の複圏と多圏が必要になる。難しいわ。

いずれにしても、高次の構造が絶対に必要なのは確か。

同義語・多義語の例

論理 圏一般論 プログラム意味論 多義語 STEM 文言正規表現

ステイ／メリディスの次の論文、とても良い。

僕がふだん考えていることだから、問題意識が一致して分かりやすい。

本論じゃないところで、（連想で）考えたことも含めていくつかの記事にしようと思う。

まず（論旨じゃないけど）連想した多義語の話。

  • {関数 | 演算(子)?}{記号 | 名}?

これを展開すると：

  1. 関数記号
  2. 関数名
  3. 関数
  4. 演算子記号
  5. 演算子名
  6. 演算子
  7. 演算記号
  8. 演算名
  9. 演算

英語だと

  • {function | operation | operator}{symbol | name}?

型理論からの例だと、

  • (型)?{文脈 | コンテキスト | 環境 | 前提 | 仮定}
  • (型)?{判断 | シーケント}

愚痴は 型理論ってば - 檜山正幸のキマイラ飼育記 から辿れる。

さらに例をいくか。

  1. (formal)? {logical | proof | deduction | deductive | entailment} system
  2. {(term)? constructor | connective | {function | operation | operator | morphism | homomorphism | map | mapping}{symbol | name}? }
  3. (term)? {rewrite | rewriting} ({rule | scheme | schema})?
  4. {equation | axiom | condition | assertion | constraint | identity | relation}
  5. {exponential | function (space)? | arrow | implication | power} type, ただし、power typeは危険。
  6. 日本語では、exponentもexponentialも「指数」
  7. {finitary | algebraic}
  8. {type | sort | set -- when(セマンティクスが集合) | object | 0-morphism}
  9. {instance | implementation | model | algebra}
  10. {rewrite | invertible 2-morphism | track}
  11. {wire | string | arrow | edge | arc}
  12. {arithmetic | calculus}

同義語・多義語を扱った記事

多義語 STEM

愚痴：

こんなんも：