檜山正幸のキマイラ飼育記 メモ編 このページをアンテナに追加 RSSフィード

キマイラ・サイト
キマイラ飼育記 本編
メモ編のアーカイブ
檜山の公開プライベート(なんじゃそりゃ?)メモ
檜山本人以外の読者を考慮しておりません。あしからず。

hiyama{at}chimaira{dot}org

2018-01-18(木)

Monoidal Topology

| 13:58

"Monoidal Topology, A Categorical Approach to Order, Metric and Topology" 508ページのPDF

モノイド概念がトポロジーにも使える、と。ほーーー。

米田モナド、図式平坦化モナド、ペースティングモナド

| 13:58

本編で書いた米田モナドだが、

次の論文にほとんど書いてある。

上記本文では、単に前層モナドと言っている。台が前層関手だから。前層モナド=米田モナドは、PSh:CatCATではなくて、PSh:CatCoCOMP という関手のプロファイルとしている。CoCOMPは余完備で局所小な圏の圏。確かに、PSh(C)が単に局所小では漠然とし過ぎている。カン拡張を作る場合でも、余完備性がいるから、CATに入ります、は条件が弱い。

次に図式平坦化モナド、まずは簡単な例から。

Sを1-箙の圏の部分圏だとする。とりあえず、有限離散箙の圏をSとする。S∈|S| にたいして、関手圏と同じ要領で図式の圏 [S, C]が作れる。φ:S→T という箙射があると、引き戻し φ*:[T, C]→[S, C] が定義できるので、S|→[S, C] はインデックス付き圏となる。余前層の圏の構成と同じ。

上記のインデックス付き圏のグロタンディーク平坦化を図式の圏と呼び DiagS(C) と書く。単に、Diag(C)とも書く。

1∈|S| とすれば、[1, C] ¥stackrel{¥sim}{=} C なので、C→Diag(C) の埋め込みは作れる。この埋め込みを ηC:C→Diag(C) と書く。

あとはモナド乗法。Diag(Diag(C)) → Diag(C) は面倒だが、グロタンディーク平坦化と同じように作れるだろう。

Diagモナドは、圏の圏CATに働く。アイレンベルク/ムーア圏EM(CAT, Diag)は、最初に選んだSにより変わるが、離散有限の形状(Sの対象を形状と呼ぶ)を選ぶと、そのアイレンベルク/ムーア代数は、デカルト圏だと思う。

CATは2-圏なので、Diagは実際は2-モナドだと思うが、2-モナドがよく分かってない。

形状の圏SアンビエントCに対するDiagS(C) は、Cに値を持つモデル(意味論)の圏になる。Sが指標の圏で、Cが計算の圏。

次にペースティングモナド。これは普通の図式計算法をモナドの形にしたもの。そもそも圏の定義が、特殊なペースティングモナド(リスト連接モナド)のアイレンベルク/ムーア代数になっている。

n-箙Aを考え、Aのセルの集合に貼り合わせデータを一緒に考えたものをペースティング図と呼ぶ。ペースティング図のペースティング図をペースティング・スキーマと呼ぶ(確か?)。ペースティングスキーマをペースティング図に落とす操作をモナド乗法とするモナドが存在するだろう。

少なくとも1-箙に関しては構成できる。

1-箙 n-箙
頂点 0セル
アロー 1セル
- i-セル
隣接条件 貼り合わせデータ
パス ペースティング図
パスのパス ペースティングスキーマ
連接 ペースティング

ペースティングモナドがn-圏を定義するモナドで、平坦化モナドが極限を定義するモナド

コンピュータッドと相対コンピュータッドの話を入れないとダメだが、後で考えよう。

n-圏の深さと変換手

| 15:22

n-圏Cがあるとして、この対象が何であるによって扱いが変わると思う。

  • |C|∈0-Cat であるとき、Cの深さは0。このとき、対象類=0-モーシングは集合。
  • |C|∈1-Cat であるとき、Cの深さは1。このとき、対象類=0-モーシングは圏。圏を対象とするn-圏。
  • |C|∈2-Cat であるとき、Cの深さは2。このとき、対象類=0-モーシングは2-圏。2-圏を対象とするn-圏。
  • |C|∈(-1)-Cat であるとき、Cの深さは-1。対象類=0-モーシングはTrueまたはFalse。深さ-1の圏は、単一の真偽値(真偽値の集合ではない)。

深さと次元が一致する必要はない。深さ1の1-圏は、対象が圏である圏。深さ1の2-圏は、対象が圏である2-圏。これにより、Catが圏か2-圏かの問題も解決する。

  • Cat1:対象が圏だが、関手しか考えないので、全体として1-圏
  • Cat2:対象が圏だが、関手と自然変換を考えるので、全体として2-圏

深さがdのn-圏において、k-変換手(トランスフォー)を考えることができる。d, n, k の関係はどうなってる?

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180118

2018-01-17(水)

網羅性のチェック

| 18:17

本編の追記に書いたが、

網羅性のチェックにnever変数への代入というトリッキーな方法がある。この方法は、次のページにあった。

指標のモデル圏のあいだの関手

| 18:18

Standard MLではモロに関手(functor)と呼んでいるのだが、やり過ぎだと思うので:

  1. トランスフォーマー: 現状、これを使っている。問題は、自然変換のトランスフォーメーションと似ていること。
  2. リダクト: インスティチューションではリダクト関手(reduct functor)と呼ぶ。が、一般的な言葉ではない。
  3. アダプター: アダプター・パターンにちなむので、悪くないと思うが、インパクトが弱い。
  4. ブリッジ: 一般的過ぎるような。
  5. ミューテーター: 生物の突然変異だから語感がどうだろ? 日本語にすると、変更手か、それはモディフィケーションと似てる。
トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180117

2018-01-13(土)

スクラッチバッファ

| 08:53

だいぶ昔、スクラッチバッファに書いてあった重要なメモがなくなって困ったことがあって、スクラッチバッファを保存するスクリプトを入れていたんだが、いつのまにかその設定とかELispファイルとかなくなっていた。

ごく最近、同じくスクラッチバッファを失って、すごいショック。2時間くらいかけた作業の結果を失った。ハアーーーーーー。こういうときは、普通のファイルに書くべきだ!!

悪いことには、2時間かけたらもう一度できるものではない。リアルタイムの音声・映像の要点をメモったものだから。もう再現はどうやっても出来ない。

なんてバカなことを! なんでファイルに書かなかった、と酷く後悔。

TypeScriptモード

| 10:13

割とVSCode使ってるが、emacsの場合:

  • c-indent-level, c-basic-offsetは効かない。
  • tab-widthは効く。がそもそもタブは使いたくない。
  • indent-tabs-modeをnilにすると、タブは使わなくなる。
  • c-tab-always-indentという変数もある。たぶん効かないが、これは僕は設定しなくもいい(デフォルト)
  • typescript-indent-levelでやっとインデント設定できた。
トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180113

2018-01-10(水)

ミクスチャ=ごった煮

| 12:24

宣言(名前のプロファイリング)と定義(束縛、名前のアタッチング)をゴッチャに混ぜて書いた形式をミクスチャと呼ぶことにする。

mixture Succ := {
 type X;
 X := int;
 value e: X;
 function succ : X->X
}

これはミクスチャの例。同じ名前に対して、「宣言が先で、定義は後」というルールさえ守れば、適当に混ぜて書いてよい。

ミクスチャに引数(argument、パラメータとは区別する!)を付けてもよい。引数を仮インスタンスとして使ってよい。

mixture OneFun (S of signature {type X}) := {
  type X;
  X := S.X;
  type Y;
  function f:X ->Y
}

引数なしミクスチャも引数ありミクスチャも、部分インスタンスを定義する。部分インスタンスは特殊なトランスフォーマーなので、結局、ミクスチャはトランスフォーマーの記述形式に過ぎない。

ミクスチャのメリットは、書き方の制約がゆるいので、楽に書けることである。いいかげんに書けることである。人間はいいかげんでモノグサだから、人間が使う記述形式としてはミクスチャが必須だと思う。

指標 ≠ コンピュータッド

| 12:47

今まで、指標はコンピュータッドの同義語としてきたが、どうも違う。その違いは指標は名前(ラベル)があること。単なるグラフとラベル付きグラフの違い。

2つの指標をとると、まったく無関係とは限らない。ラベリングによって、必然的にスパン構造=貼り合わせデータが付随する。名前構造によって定義されるベースコンピュータッドがあって、指標はベースコンピュータッドへのラベリングを一緒に考えたものだ。

指標の和(マージ)が、絶対的な直和ではなくて、余ファイバー和になってしまうのは、最初からラベリングから定義される貼り合わせデータを伴うからだ。ただし、相対コンピュータッドの圏=特定の名前構造のオーバー圏においては、余ファイバー和が直和になる。

多引数のトランスフォーマーを考えるとき、複数の引数が独立な直和としてマージされうのではなくて、余ファイバー和で合成される。これも、指標が常に貼り合わせ構造を伴うからだ。

指標のマージと貼り合わせ構造を明示するために、次のような表現を使えば良いかもしれない。

signature S := {type X}
signature T := {value e:X, function f:X->X}

// S と T をマージすると

signature {
  type S.X;
  tyep T.X;
  value T.e: T.X;
  function T.f: T.X -> T.X;
  synonym S.X = T.X
}

とりあえず、指標名で修飾(接頭辞付け)して直和を作る。synonym宣言が貼り合わせデータを与える。結果的に、

signature {
  tyep T.X;
  value T.e: T.X;
  function T.f: T.X -> T.X;
}

となる。修飾子(接頭辞)Tは無意味なので取ってもよい。

トランスフォーマーの操作

| 13:18

第一級オブジェクトとしてのトランスフォーマーを考えると:

  1. トランスフォーマーに名前を付けられる。名前無しでも扱える。
  2. 概念的には、トランスフォーマーが等しいかどうかを判定できる。現実的には無理なこともある(つうか、たいていは無理だけど)。
  3. トランスフォーマーを結合できる。
  4. トランスフォーマーをマージできる。
  5. トランスフォーマーをパラメータ化できる。
  6. パラメータ化したトランスフォーマーに、もうひとつのトランスフォーマーを代入できる。

こんなところだろう。

相対指標とパラメータ化指標を同義語だとして、[Δ]Σ で表す。Δ⊆Σ の場合が扱いやすいが、実際は包含してなくてもよくて、

  • [Δ]Σ = [Δ](Δ∪Σ)

もともと包含がなくても、解釈の時点で包含を作ってしまう。

s:Δ'→Δ, t:Σ→Σ' が2つの指標だとして、[s]t : [Δ]Σ → [Δ']Σ' を作れる。これは2つのトランスフォーマーの指数で、Trfop×TrfTrf という反変・共変な二項関手となる。

トランスフォーマーの圏は、マージを対称モノイド積とするモノイド閉圏になる。

  1. モノイド単位対象は、空指標。
  2. 対象のモノイド積は、指標のマージ Γ∪Σ
  3. 射のモノイド積は、トランスフォーマーのマージ t∪su
  4. 対象の指数は、パラメータ化 [Δ]Σ
  5. 射の指数は、逆行ペア [s]t
  6. 評価射は、代入(置換)で与えられる。
  7. 圏と関手からなるデカルト閉圏への表現を持つ。

次の概念は同じ。

  • 部分指標、指標の包含関係、指標の制限、指標の拡張、指標の親子関係、指標の継承関係

指標の制限オペレータは、単に部分指標の包含写像、ただし引き戻しになっている。

トランスフォーマーにも同じことが言えて、次は同じ。

全部同じこと、言葉が違うだけ。

トランスフォーマーの圏は、トランスフォーマーのあいだの変換(何と呼ぶ)があって、実際には2-圏になっている。2-射として、包含だけを採用した場合、ホムセットがホム順序集合となり、順序豊饒圏となる。2-圏だと複雑だから、順序豊饒圏あたりが妥当かも知れない。

[追記]

そうか、ホムセットが、有限余完備圏で豊饒化されればいいのか。(さらに追記あり)

有限余完備は、非モノイド的余デカルトと同じだから、CoCarCatで小さい余デカルト圏の圏だとして、圏の直積をモノイド積として対称モノイド圏とする。CoCarCat-豊饒圏を考えると、だいたい2-圏のようなものができる。が、むしろ豊饒圏論のほうが自然かも。

ホム圏自体はモノイド閉じゃないけど、射のモノイド閉と射の余ファイバー和は作れる。2-射はホム圏の1-射だとすればよい。

2-射をなんて呼ぶかが大問題だ。単に「包含関係」として、サブトランスフォーマーとスーパートランスフォーマーが一番無難か。ただし、sub- と partial- の問題が出る。部分インスタンス=partial instance とサブインスタンス=subinstanceを区別しないと。サブインスタンスは、スーパーインスタンスがあってのこと。部分インスタンスにはスーパーインスタンスはない。

インスタンスは一切出さないで、ミクスチャで代用するか。すると:

[/追記]

[さらに追記]ん、あれ。豊饒圏じゃないのか。ダメだ、もっと考える![/さらに追記]

[さらにもっと追記]2-射が四角形になる、二重圏みたいだ。モノイド閉な二重圏? あんまり聞かない構造だなー。[/さらにもっと追記]

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180110

2018-01-09(火)

モノグサ精神のジレンマ

| 12:50

モノグサはプログラマの美徳と呼ばれる。モノグサ精神は進化の原動力となるが、同時に理論的整合性を崩したり、混乱と錯誤の元凶ともなる。

モノグサ精神は:

  1. 記述量を減らしたい、略記したい
  2. オーバーロードしたい
  3. 名前を考えたくない、名前を付けたくない

原理的な所がシッカリしない前にモノグサ精神を発揮すると、グチャグチャになってしまう。モノグサ精神は確かに大事なんだが、どうやってモノグサすべきかの方針がvalidでないと悲惨だ。

シャドーイングの問題

| 15:17

シャドーイングは、現実的には頭の痛い問題で、認める/認めないの判断(決断)が必要だ。が、理論的には特に問題ない。

シャドーイングは入れ子スコープで起こるが、「入れ子にすること」を指標のマージだと解釈する。マージは余ファイバー和と解釈する。余ファイバー和は、スパンに対して定義されるが、スパンは入れ子の可視性によって定義される。

Σ | Δ で、Σの内側に入った指標Δを意味するとき、シャドーイングがないなら、Σ←Σ→(Σ+Δ) というスパンが入れ子を表す。シャドーイングがあるとき、Σ'⊆Σ をシャドーで削られた指標とする。そして、Σ←Σ'→(Σ'+Δ) を作ればいいので、何の問題も起きない。

  • シャドーイングは現実的には難しい問題だが、理論的には何ら問題にならない。


で、現実的な話をする。

Σが外側のスコープで、Δが内側のスコープとする。外側のΣ自体に名前sがあるとき、Δ内からs.fooとすれば、Σ内のfooにアクセスできる。sは大域名で、sはシャドーされてないとする。Σに名前がなかったり、名前を使いたくないときは、ΣとΔの相対位置に注目して、Δ内から (upper foo)とする。upperは修飾子で、ひとつ外のスコープにいって見ることを意味する。(upper upper)foo とかしてもよい。

foo = (upper foo) のとき、fooはシャドーされてない。foo ≠ (upper foo) のときfooはシャドーされている。すべての名前fooに関して、foo = (upper foo) か foo ≠ (upper foo) かを決めると、それは貼り合わせデータとなるから、スパンになり、余ファイバー和を定義できる。

スパン(余ファイバー)と余ファイバー和が定義できれば、後はなんとでもなる。

入れ子とシャドーイングとモノスパンの圏

| 15:36

シャドーイングの問題 - 檜山正幸のキマイラ飼育記 メモ編の続き。

入れ子 Σ | Δ があるとき、シャドーイングがあろうとなかろうと、Σ←Σ'→(Σ' + Δ) ができる。この事実から、一段階の入れ子はスパンで表現できることがわかる。一般のスパンではなくて、両脚がモノになっている。よって、入れ子=モノスパン。モノスパンと貼り合わせデータはまったく同じ。

指標の圏をベースに、そのなかのモノスパンの圏を考える。対象は同じく指標で、射をモノスパンとする。入れ子の場合は自然に方向(親から子)が決まるので、モノスパンの方向(脚の左右または前後)も自然に決まる。

入れ子の平坦化がモノスパンの余ファイバー和だから、モノスパンの系(モノを辺とするグラフ)があるとき、それをダイヤグラムとみて余極限ができる。余極限だからup-to-isoで一意。

これは、任意の入れ子構造(ツリー状の階層)に対して、平坦化がup-to-isoで一意に存在することになる。up-to-isoはup-to-renameなので、名前の違いを除いて一意となる。

2018-01-08(月)

相対指標とパラメータ化指標

| 13:09

相対指標とパラメータ化指標は同じ概念である。が、相対指標は原理的で、パラメータ化指標は実用的。

Σが指標のとき、指標に出現するすべての名前の集合を全名前集合〈whole name set〉と呼ぶ。全名前集合の部分集合を単にΣの名前集合〈name set〉と呼ぶ。

指標やインスタンストランスフォーマーの記述レコードは、宣言/定義の集合ではない。順序依存性があるのでリストに近い。ただし、一部の順序は交換可能で、ようするにコンピュータッド(集合のリスト)だ。

相対指標〈relative signature〉は、指標とその部分指標のペアだが、形式上、指標を前半と後半に分けた形で書くことができる。部分指標をΔ、全体指標(親指標)をΣとすると、[Δ]Σ と書く。Δ#Σ' = ΣであるΣ'を使って、[Δ]Σ' でもよい。重複記述を避けるには、Σ'を最小に取る。Σ'からΣを再現するには、Δとマージ(#演算)すればよい。

指標演算とパラメータ化

最も重要な指標演算はマージで、'#'か'+'で表す。一般には直和ではなくて、余ファイバー和になる。余ファイバー和を作るには、スパンが必要だが、スパンは指標のラベリング(名前付け)に基づいて作れる。要するに、同じ名前は同一視するだけ。マージと余ファイバー和はまったく同じ

AをΣの名前集合とする。このとき、Aを含む最小の部分指標=グラフをAのハル〈hull | 外皮 | 外殻〉と呼び、Hull(A, Σ)と書く。

ハルを使うと、指標から名前を削除する“引き算”が定義できる。

  • Σ - A := Hall( (|Σ| \ A), Σ)

\は単なる集合差。|Σ| := Σ0∪Σ1。Aが部分指標Δであっても、Δの全名前集合をAとして、Σ - Δ = Σ - A として指標の差を定義できる。

  • Aが名前集合のとき、named param A Σ は、relative signature [Hull(A, Σ)]Σ と同じ。
  • Xが名前のタプル、AはXの順序を忘れたものだとして、ordered param X Σ は、relative signature [Hull(A, Σ)]Σ と同じ。

こうして見ると、順序パラメータは、相当に複雑なメカニズムを導入してしまっていることがわかる。順序と名前のあいだの対応関係を挟んでいるので、束縛を作る手間がかかる。

相対指標、部分インスタンス、半指標

相対指標 [Δ]Σ があるとき、ΔのインスタンスAを付けた (A, [Δ]Σ) を部分インスタンス〈partial instance〉と呼ぶ。部分インスタンスの表現として、[A]Σ も使う。部分インスタンスは実は指標でもあるので、半指標〈semi signature〉とも呼ぶ。

なぜ2つの名前を準備するか、というと、人は「名前の呪縛」=「名は体を表すものだという強い思い込み」を持つから。インスタンスと呼んでしまうとインスタンスだと思ってしまう。指標だと思いたいときに、半指標と呼ぶ。

[A]Σ が半指標のとき、instance of [A]Σ というインスタンスを考えることができる。これは、もともとあった全指標Σのインスタンスになる。

次の手順になる。

  1. 指標Σがある。
  2. 部分指標Δを選ぶ。Δ⊆Σ。
  3. 相対指標 [Δ]Σ を作る。Σ' を使って、[Δ]Σ' と書けるが、それは単なる略記
  4. ΔのインスタンスAを選ぶと、半指標 [A]Σ ができる。
  5. 半指標も指標なので、半指標のインスタンスBができる。instance B of [A]Σ := {...}
  6. Bは指標Σのインスタンスとなっている。

指標Σから一気にBを作る代わりに、ΔのインスタンスAをあいだに挟んで、二段階でインスタンスを作るような指示を含むのが相対指標である。相対指標のインスタンス化は、部分指標のインスタンス化と残った半指標のインスタンス化の二段階になる。

相対指標の解釈として、マージ演算#を対称モノイド積とするモノイド圏における閉構造として捉えることができる。大枠としては、

  • Cat(Mod[Δ#Γ], Mod[Σ]) ¥stackrel{¥sim}{=} Cat(Mod[Γ], [Mod[Δ], Mod[Σ]])

であり、

  • Mod[[Δ]Σ] ¥stackrel{¥sim}{=} [Mpd[Δ], Mod[Σ]]

Trfを次のように定義するとよいと思う。

  • Trf(Γ, Σ) := Cat(Mod[Γ], Mod[Σ])

実際には、Mod[]の定義がシステム (Ω, ω:Ω→Set)と相対的になる。また、ホントは、

  • Trf(Γ, Σ) ⊆ Cat(Mod[Γ], Mod[Σ])

であり、置換子〈サブスティテューター〉により実現できる関手だけがTrfに含まれる。トランスフォーマー〈変換子〉より、置換子のほうがより本質的な存在で、トランスフォーマーは、置換子の相対的な反変表現になっている。換言すれば、置換子の圏の相対化(+反対化)によりトランスフォーマーの圏が生まれる。

  1. 指標と置換子の作る圏がある。
  2. その圏は、クリーネ/ストリート相対モナドの相対クライスリ圏である。
  3. Ω-インスタンスの圏は置換子の圏に対するアンダー圏 Subst である。
  4. アンダー圏SubstCatへの反変表現を持つ。その反変関手がModω[]である。この場合のモデルは、タルスキーモデル(超越的モデル)ではなくてエルブランモデル(構文構成的モデル)なので、HModω[] と書いたほうがいいかも。
  5. Substは、局所モノイド閉構造を持つ。Mod[]は、局所モノイド閉構造の局所デカルト閉構造への表現を与える。
  6. 全体として、たぶん米田構造を持つだろう。
トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180108

2018-01-06(土)

モデルの概念と理論

| 18:47

システム全体もひとつの指標を持つから、それをシステム指標と呼び、Ωで表す。システム指標に含まれる名前はso-called大域名で、いつでもどこからでも自由に参照できる。

システム指標Ωの環境(文脈)下にあるトランスフォーマーtを次のように書く。

  • Ω| t:Σ→Γ

なにをシステム指標とみなすかは勝手なので、

   Ω| t:Σ, Σ'→Γ
  --------------------
   Ω, Σ| t':Σ'→Γ


   Ω, Ω'| t:Σ→Γ
  --------------------
   Ω| t':Ω',Σ→Γ

これは重要で、システムをライブラリで拡張したり、カーネル機能をユーザーランドで実装したりに相当する。システムとユーザープログラムの境界は動かしてよい

トランスフォーマーtに対して、それが定義する置換子をtと書く。次の関係がある。

   Ω| t:Σ→Γ
  ---------------
   t:Γ→(Ω,Σ)

(-)は、指標=コンピュータッドから圏を作る演算子。

トランスフォーマーと置換子〈サブスティテューター | substitutor〉の違いは:

  • トランスフォーマーはシステムに対して相対的だが、置換子は絶対的に記述する。
  • 向きが逆である。

よって、次のように考えればよい。

  1. まず、置換子の圏を考える。対象は指標。
  2. 指標の順次併置演算#をモノイド積と考えて、モノイド圏とする。
  3. Ωによるモノイダル・スタンピングモナド Ω#(-) を考える。
  4. さらに、(Ω#(-))* を考える。(-)*はクリーネ/ストリート・スター。クリーネ/ストリート・スターは、コムキャット随伴性から作られるモナドの台関手。
  5. Ωごとに、このモナドのクライスリ圏を生やす。
  6. クライスリ圏は反対圏を取る。
  7. インデックス付き圏が出来る。
  8. グロタンディーク射は、クロスプラットフォーム・シミュレーション


ここで、「同義語・類義語・多義語」の問題を述べる。

システム指標は次のように言っても同じ。

  1. 環境
  2. 文脈
  3. 組み込み指標
  4. コア指標
  5. カーネル指標
  6. ニュークリアス

システムとは、システム指標Ωと ω:Ω→Set(厳密には、忘却関手で移したSet)として定義したいが、ωのことは、

  1. 表示〈denotation〉
  2. モデル
  3. 代数(指標Σの代数)
  4. セマンティクス〈意味〉
  5. (抽象)実装
  6. 抽象機械
  7. 仮想機械
  8. (抽象)アーキテクチャ
  9. (抽象)仕様
  10. (抽象)ランタイムシステム
  11. (抽象)実行系
  12. (抽象)エンジン
  13. 実行環境
  14. プラットフォーム

などなど、山のような同義語・類義語。組み合わせも考えると

  • { | 抽象 | 仮想 | 概念}{ | ランタイム | 実行 | 実行時}{システム | 系 | 実装 | エンジン | 機械 | コンピュータ | ハードウェア | 環境 | 仕様 | アーキテクチャ}

ここでは「モデル」を使用する。システム指標とシステムモデルがシステム(プログラムの実行環境)を定義する。モデルに域・余域の概念は入っているから、「システム=Ωが域であるモデル」。

構文的なインスタンスとは、引数指標を持たない(空である)トランスフォーマーt

  • Ω| t:→Σ

tは、Σのインスタンス(instance of Σ)と呼ぶ。tの置換子は、

  • t:Σ→Ω* in Com

置換子は、コンピュータッド圏に働くクリーネ/ストリート・スターのクライスリ射と考える。システム指標Ωにはシステムモデル ω:Ω→Setがあったから、インスタンスの置換子とシステムモデルを結合すると、指標Σ上のモデル ω':Σ→Set が出来る。

  • [ω, ω']:Ω#Σ→Set

これは、システムをΣ-インスタンス(基礎ライブラリ)で拡張〈enhance〉したものになる。

別な見方として:

この見方から、

とも言える。しかし、インスタンスがモデルそのものではなくて、インスタンス(というトランスフォーマー)の置換子を通じて、システムモデル(決っている)が引き戻される。

ここで、システムモデルを色々と動かしてみると、インスタンスtは、

  • Ωのモデルの圏[Ω, Set]からΣのモデルの圏[Σ, Set]への関手を定義する。

この事実により、Standard MLではトランスフォーマーを関手と呼ぶ。

次のモノの相互関係を調べることが大事。

  • 指標
  • システム指標(ただし、色々と動かす)
  • トランスフォーマー(システム指標に相対的)
  • システムモデル
  • 一般のモデル
  • モデル圏(可能なモデルをすべて考える)
  • インスタンストランスフォーマーの一種、モデルとは区別)
  • 指標のスタンピングモナド
  • 指標のクリーネ/ストリート(・スター)・モナド
  • 指標(コンピュータッド)と置換子の圏に働くモナドと、モナドを利用した初等関手。
  • 特殊な射としての値と述語の概念

指標と置換子/トランスフォーマーの理論は、(0,1)-論理のような気がしている。

(-1, 0)-論理 (0, 1)-論理
集合 指標(圏 and/or コンピュータッド)
単元集合 自明な指標
空集合 空な指標
Xの値=要素=点 Σのインスタンス
関数 変換子 and/or トランスフォーマー
関数の大域環境 トランスフォーマーの環境
ブール集合 集合圏
述語 モデル
述語集合 モデル圏
直和スタンピング マージスタンピング
ベキ集合モナド モデル圏モナド
部分集合ファイブレーション モデル・ファイブレーション
ホーア論理 シミュレーションの理論
ラムダ計算 パラメータ化計算

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

| 18:52

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

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

コンピュータッドは、背景としている形状により定義が変わるが、ここでは常に球体形状〈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 が成立する。

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

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180106

2018-01-05(金)

カン拡張と米田拡張

| 16:10

まず、nLabのカン拡張項目:

Proposition 2.8. Let

  • C be a small category;
  • D have all small limits.

Then the right Kan extension of a functor F:CD of locally small categories along a functor p:CC' exists and its value on an object c'∈C' is given by the limit (極限公式)

あるいはMarina Christina Lehnerのテキスト

Theorem 3.1. Given K∶ CD, let F∶ DE be a functor such that ... (consider the left/right Kan extension of F along K) (極限公式)

Corollary 3.9. When C is small, right Kan extensions exist when E is complete, while left Kan extensions exist when E is cocomplete.

これで、基本関手 K:CE に関して、Cが小さい圏で、Eが余完備ならば、Kに沿った左カン拡張の存在が保証される。

次に、小さい圏の前層の圏に関して:

によると、Dの前層の圏PSh[D]はDの自由余完備化となっている。もちろん、PSh[D]は余完備。したがって、米田埋め込み yC:C→PSh[C] に沿った、F:C→PSh[D] の左カン拡張は存在する。

実際、そのような拡張を米田拡張と呼ぶ。

The Yoneda extension of a functor F:CD is extension along the Yoneda embedding Y:C→[Cop, Set] of its domain category to a functor F~:[Cop, Set] → D.

Yoneda extension F~ is the left Kan extension LanYF:[Cop, Set]→D F along the Yoneda embedding Y:

米田埋め込みと米田拡張があるので、これからマナ・スタイル(=拡張スタイル)のモナドを定義する。しかし、そのままではうまくいかない。

"Operads, clones, and distributive laws" by Pierre-Louis Curien(キュリア)の2012年論説、11p.からの"7 Profunctors as a Kleisli category"を参照。

これに対する対処は、

"Monads Need Not Be Endofunctors" Thorsten Altenkirch, James Chapman, Tarmo Uustalu が参考になる。

サイズの問題は、

フレイド/ストリート(PETER FREYD AND ROSS STREET)のサイズ定理で、ある程度は解決できる。複数の宇宙を使う方法は、

"An introduction to Yoneda structures" Paul-André Melliès に書いてある。

クライスリ・コンピュータッド圏n-Kom

| 18:58

n-Comをn-コンピュータッドの圏だとする。Fn -| Vn : n-Com ←→ n-Cat をn次元のコムキャット随伴性だとする。この随伴性から導かれるn-Com上のモナドの台関手を Sn とする。コンピュータッドΣに対してSn(Σ)をS*と書く。上付きの星印をクリーネ/ストリート・スターと呼ぶことにする。

記号の乱用で、記号Sを、台関手だけではなくてモナド全体を表すために使う、S = (S, η, μ)。Kl(n-Com, Sn)を、クリーネ/ストリート・スター・モナドSnに対するクライスリ圏とする。

  • n-Kom := Kl(n-Com, Sn)

圏(むしろ2-圏だと思う)n-Komの対象はコンピュータッド、射はコンピュータッドのトランスフォーマーn-Komの米田埋め込みは次のように記述できる。

  • Ω |→ n-Kom(-, Ω)

Ωはシステム指標〈コア指標 | 組み込み指標〉と考えると、システム指標を決めるごとにエルブラン・モデル関手が決まることに対応する。エルブラン・モデル関手またはタルスキー・モデル関手は、インスティチューション(エルブラン・インスティチューション、またはタルスキー・インスティチューション)を決める。Ω→Σ in n-Kom があると、インスティチューションのあいだの準同型が決まる。

こんな感じだと思う。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20180105

2017-12-31(日)

コムキャット随伴性

| 16:12

ComCat随伴性。Comはコンピュータッド、Catは圏で、

  • n-Compd(Σ, V(D)) ¥stackrel{¥sim}{=} n-Cat(F(Σ), D)

という自由・忘却スタイルの随伴性。これがメチャクチャ重要だと思う。

コムキャット随伴性から誘導されるモナドをコムキャットモナドとする。このモナドももちろんメチャクチャ重要。

キャット⊆コム

| 19:22

コンピュータッドの圏を単にCom(コム)と書くことにする。n-圏のn-構造を忘れて、(n-1)-構造をそのままにして忘却関手 V:n-Catn-Com が定義できる。この忘却関手を使うと、

  • n-Catn-Com

とみなせる。これは、モデル論も含めてすべてコムのなかで出来ることを意味する。

課題は、コンピュータッド、構文モナド(のクライスリ圏)、インスティチューション(のグロタンディーク平坦化)との関係だろう。

それと、指標の圏=コンピュータッドの圏でいいだろうが、指標射は写像ではなくてコボルディズムだと思う。多様体コボルディズムなんかとは比べ物にならないほどの柔軟で、すべてのコンピュータッドは一点(自明なコンピュータッド)へのコボルディズム=錐体を持つ。コボルディズムという言葉が適切かはあやしいけど。

部分インスタンスと相対指標

| 19:46

Σが指標、ΔをΣの部分指標とする。Σに対して、Δ部分だけをインスタンス化したものをΣの部分インスタンスと呼ぶ。これはまーいい。

ΔとΣの組 (Δ, Σ) を相対指標と呼ぶ、ただし、Δ⊆Σ。次のように考える。

相対指標(Δ, Σ)は、Δに対する実装責務を主張しているとする。別言すれば、Σ\Δに対しては責務を課してない。

相対指標(Σ, Σ)は、絶対指標Σと同じである。全体に対する実装責務を課しているから。(∅, Σ)は何の責務も課してない。

  • 完全インスタンスは、(Σ, Σ)に対する責務履行〈fullfillment〉である。
  • インスタンス(1個だけある)は、(∅, Σ)に対する責務履行である。

相対インスタンスは、包含射 i:Δ→Σ に伴う射影リダクト関手 Πi:Mod[Σ]→Mod[Δ] を持つ。部分インスタンスはMod[Δ]の対象Aを決めるので、射影リダクト関手のファイバー Πi-1[A]を決める。

部分インスタンスの意味は、Σのモデル圏を、ファイバー Πi-1[A] にまで狭めることだろう。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20171231

2017-12-30(土)

指標の圏

| 18:28

具体的な指標=コンピュータッドの圏は面白い。単純そうだが実際は色々と複雑で、ジャングルを探検する気分。

指標の射は基本射〈basic morphism〉と拡張射〈extended morphism〉に分けて考えたほうがいいようだ。基本射は、コンピュータッドとしての射。拡張射は項モナド(構文モナド)のクライスリ射。

で、射の方向が実に紛らわしい。どっちを順方向にするかを決めておいたほうがいいな。基準となるのは、部分指標の包含射 Δ⊆Γ をΔ→Γとみるか、Γ→Δとみるかだろう。仮に、Δ→Γを順方向とみると、包含に対応する制限子はΓ→Δだから反対になる。制限子は特殊な変換子〈トランスフォーマー〉とみなせるから、変換子も逆方向の射となる。

変換子はリダクト関手と同じ方向になるから、これはやはり指標射の反対射とみるのがよさそうだ。つまり、順方向の指標射は変換子の反対射。

改名子は同型射(可逆射)だから、方向はどうでもいいが、変換子の方向と揃えておいたほうがいいだろう。

 rename{ top to peek} signature {type S, V; top : S -> V; push : S*V -> S; pop : S -> S|eror}
=
 signature {type S, V; peek : S -> V; push : S*V -> S; pop : S -> S|eror}

次と同じ、

transformer (instance St of Stack) to (instance of ?)
{
  S := St.S;
  V := St.V;
  ppk := St.top
  push := St.push;
  pop := St.push;
}

方向は、リネーム前の指標 → リネーム後の指標、旧名 =: 新名 または、新名 := 旧名。

インスタンスは特殊な変換子になる。

instance of ToggleSwitch {
  S := bool;
  isOn := (s:S):bool => s == true;
  isOff := (s:S):bool => s == false;
  toggle := (s:S): S => s? false : true;
}

transformer (instance _ of Empty) to (instance of ToggleSwitch)
{
  S := bool;
  isOn := (s:S):bool => s == true;
  isOff := (s:S):bool => s == false;
  toggle := (s:S): S => s? false : true;
}

次に部分インスタンス

partial instance of Counter {
  C := int;
}

transformer (instance X of singnature {init: -> int; up : int -> int})
          to  (instance of Counter)
{
 C := int;
 init := X.init;
 up := X.up;
}

インスタンス化(具体性が増す)の方向と変換子の方向は逆。

あとはパラメータ化。パラメータ化は指標に対する操作で、おそらく指数対象を作ることになる。もし、指数対象がパラメータ化指標なら、射=変換子の逆に対して、射の指数は Sig×Sigop→Sig という反変共変の二項関手になるので、取り扱い注意。

指標をワイヤー、変換子をノードにした絵を描くといいと思う。

トラックバック - http://d.hatena.ne.jp/m-hiyama-memo/20171230