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

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

指標と仕様と等式的と述語的

指標とコンピュータッドはまったく同義語だとする。指標の理論とはコンピュータッドの理論。

  • (具体)指標=コンピュータッド=ポリグラフ=(高次)箙

コンピュータッドは、背景としている形状により定義が変わるが、ここでは常に球体形状〈globular shape〉。

仕様と指標の本質的な違いはない。仕様は指標の一種であり、高次元部分を表明〈assertion〉と呼ぶと、それは仕様になる。何を表明と呼ぶかの基準はないので、仕様と指標の区別も基準はない。

最も重要な仕様は、n-圏の(n + 1)-指標である。n-圏の(n + 1)-射は等式しかないので、必然的に、指標の(n + 1)部分〈(n + 1)-part | (n + 1)-section〉は、n-射の等式の集まりになる。この形の指標を等式仕様(等式的仕様)と呼ぶ。等式は無限個あってもよい。

述語とは、特定の基準対象〈criterion object〉への射である。0-基準対象はブール集合、1-基準対象は集合圏である。各次元の基準対象は持ち上げ〈lift〉と落とし込み〈drop〉ができる。

真射〈truth morphis〉とは、任意の対象から基準対象への射で、自然変換として決っている。τX:X→B 。トポスではサブオブジェクト・クラシファイアだが、一般的な特徴付け=公理化はよく分からない。

真射以外に、X上のブール値定数関数に相当する命題射(または真偽値)が定義できる。X上の命題射は、基礎対象からの命題射=真偽値を、基礎対象=終対象への唯一射〈bang〉で引き戻したもの。

述語射と命題射の組を表明のフォーマットに採用した仕様を述語仕様(述語的仕様)と呼ぶ。

n-圏に対する述語仕様は、形式上はn-指標である。n-射までしか登場しないから。しかし、実際は等式仕様になる。述語と真偽値の組を、等式とみなして、(n + 1)-セルとして追加すれば、対応する等式仕様ができる。

  • 述語仕様は、等式仕様の略記である。


コンピュータッドと圏の関係を考える上で、等式仕様は重要である。圏Cに対して、どのような指標を作るかは自明ではない。特に高次圏では難しい。

n = 1のケースでは、1-圏Cに、2-指標(1-等式仕様)Σを対応させる。

  1. Σ0 = |C|0 = Obj(C)
  2. Σ1 = |C|1 = Mor(C)
  3. Σ2 = (別記)

Σ2 は次のようにする。1-指標 (Σ0, Σ1)の上にグラフの圏を作る。グラフの辺は、[A, f1, ... , B] の形。次の等式をすべてΣ2に入れる。

  • [A, f, g, C] = [A, f;g, B]
  • [A, idA, A] = [A, A]

2-指標Σから生成される1-圏は、Σ0, Σ1から生成されるグラフに、Σ2の等式達から生成される最小の同値関係による商となる。

こうして作った圏をΣとする。圏から等式仕様を作る操作を C! とすると、C! \stackrel{\sim}{=} C が成立する。

自由生成モナドと、モナドの代数による定式化と若干違う。この違いを分析する必要はある。