今まで、指標はコンピュータッドの同義語としてきたが、どうも違う。その違いは指標は名前（ラベル）があること。単なるグラフとラベル付きグラフの違い。2つの指標をとると、まったく無関係とは限らない。ラベリングによって、必然的にスパン構造＝貼り合わ…

宣言（名前のプロファイリング）と定義（束縛、名前のアタッチング）をゴッチャに混ぜて書いた形式をミクスチャと呼ぶことにする。 mixture Succ := { type X; X := int; value e: X; function succ : X->X }これはミクスチャの例。同じ名前に対して、「宣言…

相対指標とパラメータ化指標は同じ概念である。が、相対指標は原理的で、パラメータ化指標は実用的。Σが指標のとき、指標に出現するすべての名前の集合を全名前集合〈whole name set〉と呼ぶ。全名前集合の部分集合を単にΣの名前集合〈name set〉と呼ぶ。指…

指標とコンピュータッドはまったく同義語だとする。指標の理論とはコンピュータッドの理論。 （具体）指標＝コンピュータッド＝ポリグラフ＝（高次）箙 コンピュータッドは、背景としている形状により定義が変わるが、ここでは常に球体形状〈globular shape…

システム全体もひとつの指標を持つから、それをシステム指標と呼び、Ωで表す。システム指標に含まれる名前はso-called大域名で、いつでもどこからでも自由に参照できる。システム指標Ωの環境（文脈）下にあるトランスフォーマーtを次のように書く。 Ω| t:Σ→Γ…

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

Σが指標、ΔをΣの部分指標とする。Σに対して、Δ部分だけをインスタンス化したものをΣの部分インスタンスと呼ぶ。これはまーいい。ΔとΣの組 (Δ, Σ) を相対指標と呼ぶ、ただし、Δ⊆Σ。次のように考える。 部分インスタンスは、相対指標のインスタンス 完全インス…

コンピュータッドの圏を単にCom（コム）と書くことにする。n-圏のn-構造を忘れて、(n-1)-構造をそのままにして忘却関手 V:n-Cat→n-Com が定義できる。この忘却関手を使うと、 n-Cat⊆n-Com とみなせる。これは、モデル論も含めてすべてコムのなかで出来ること…

ComCat随伴性。Comはコンピュータッド、Catは圏で、 n-Compd(Σ, V(D)) n-Cat(F(Σ), D) という自由・忘却スタイルの随伴性。これがメチャクチャ重要だと思う。コムキャット随伴性から誘導されるモナドをコムキャットモナドとする。このモナドももちろんメチャ…

具体的な指標＝コンピュータッドの圏は面白い。単純そうだが実際は色々と複雑で、ジャングルを探検する気分。指標の射は基本射〈basic morphism〉と拡張射〈extended morphism〉に分けて考えたほうがいいようだ。基本射は、コンピュータッドとしての射。拡張…

CafeOBJで、タイト意味論とルーズ意味論という言葉を使っていたが、いまいちハッキリしないので、次の3種に分ける。 ホール〈whole | 全体〉意味論 始対象意味論 終対象意味論 Σが指標のとき、〚Σ〛をどうするか、という話。これをハッキリさせないで指標の…

指標の圏が有限余完備であることが本質的。ただし、非モノイド的なので、モノイド積は定義できない。非モノイド的有限余完備圏。それと、ゴグエンのいうinclusiveで、やせた部分圏としてinclusionが定義されている。双対的にはprojectionだが、inclusioinと…

等値的圏と同値的的圏 k-等値的圏〈k-equational category〉は、k≦n であるn-射がすべて恒等になってしまう圏。 0-等値的圏： 0-射がすべて恒等？ 対象がすべて恒等？ うーん？？ 空集合か単元集合のことだ。よって、0-等値的圏の全体はブール集合になる。 1…

ユグドラシル・エクスプローラー - 檜山正幸のキマイラ飼育記 メモ編の続き。ワールドのなかにある項目を、ミクロ項目とマクロ項目に分けたほうがいい。 マクロ項目： 項目なので区分〈division〉、プロファイル、名前を持つが、名前だけでなくて、名前に関…

https://ncatlab.org/nlab/show/transfor トランスフォー〈変換手〉はワールドの項目として必要となる。nとkで、k≦n に対して (n, k)-トランスフォーが定義できる。 (0, 0)-トランスフォーは写像〈map〉 (1, 0)-トランスフォーは関手〈functor〉 (1, 1)-トラ…

ユグドラシル “ユグドラシル”は、Coqのuniverseの話を読んだ時連想した。 エクスプローラー ブラウザと言ってもいいんだけど、“エクスプローラー”のほうが探索・探検・究明の意味があるから。 我々が何かするときの文脈を世界〈world〉と呼んでしまおう。世…

だいたいの感じは掴めた。 概念 表現方法 ソフトウェア 圏 コンピュータッド データ（JSO形式？） ドクトリン 等式的仕様 拡張機能 圏はドクトリンに所属するが、プレーンドクトリン＝単なる圏は最初から入っている。システムコアには、銀河に相当する唯一の…

基本的な概念と用語： まだ曖昧な所があるが、 区分〈くぶん | division | ディヴィジョン〉： 特定の圏Cと次元数kのペア。Cのk-射の集合を意味する。 区分ラベル： 区分に付ける人間可読なテキスト。 区分け〈くわけ | divisioning | ディヴィジョニング〉 …

ハイパーインスティチューションは、3×3のマトリックスで整理できる。縦横どう書くかは自由だが、3ロール×3レイヤーと呼ぶ。 ロール： ベース（Base）ロール、論理（Logi）ロール、モデル（Mode）ロール レイヤー： アンビエント（Ambi）レイヤー、計算（Com…

圏論的な世界〈world〉を次のようなものだとする。 世界の構成素を領地〈dominion〉と呼ぶ。 領地は、高次の圏、複圏、多圏のいずれかである。 領地は有限個である。 それぞれの領地は小さいn-圏, n-複圏, n-多圏である。 領地の次元は有限で、最高次元nが領…

指標（"インデキシング・ベース圏”の対象）と命題（{インデキシング垂直圏 | ファイブレーションのファイバーである圏}の対象）のペアを仕様と呼ぶ。仕様はグロタンディーク／エルブラン圏＝ハイパーベース圏の対象であると同時に、ハイパーインスティチュー…

重要なのはグロタンディーク／エルブラン圏である。 MLの概念 グロタンディーク／エルブラン圏 別な言い方 シグニチャー 仕様 セオリー ストラクチャ 絶対セオリー インスタンス ファンクタ 相対セオリー トランスフォーマー シグニチャに属するストラクチャ…

素材： 名前の集合 Name アンビエントドクトリン アンビエント圏C： アンビエントドクトリンから1つ選ぶ 論理ドクトリンL 以上から、指標圏と指標射が作れて、指標圏を定義できる。この指標圏をベース圏として、論理ドクトリンLに値をとるインデックス付き圏…

ストラクチャ＝{構造体 | クラス | 型クラス | レコード | 指標 | オブジェクト} トランスフォーマ＝{ファンクタ（SML） | 型クラス・インスタンス | セオリー} プロファイリング ： ストラクチャのメンバーの一部 バインディング ： ストラクチャのメンバー…

用語法、表記法 オペレーター | オペレータ | 演算子 | 作用素 | コンビネータ | コンビネーター コンストラクタ | コンストラクター | 構成子 | 構築子 | 生成子 例 トレースオペレーター 不動点オペレーター CADGの微分オペレーター／微分コンビネータ デ…

Erlangにパーズトランスフォームってのがあったけど、あんな感じだろうな。プログラミング言語であれば、そのプログラミング言語でパーズトランスフォームを書けたらいいが、専用構文のほうが可搬性はあるかもしれない。いずれにしても、入力構文の適当なタ…

「型」と「型つけ」の概念が曖昧。型の代わりにプロファイルを導入して、型つけ〈タイピング〉の代わりにプロファイリングを使う。型は対象のことだとして、型付けは、基礎射のプロファイリングの意味に限定して使う。つまり、f:->A in C の形のプロファイリ…

当然にインスティチューション 当然に述語論理＝ハイパードクトリン 限量子随伴性 ＝ ΣΔΠ随伴性 否定があるなら、否定双対性。スター自律圏かな？ 継続との関連は？ 契約は仕様と関連するから、メイヤー先生のDbCとは関連する。 仕様モジュール、セオリー・…

name object 呼び名 圏論 変数名 型 型宣言 指標対象成分 関数名 項 関数 指標射成分 ラベル 命題 表明 論理対象 定理名 証明 定理 論理射 名前の宣言 name 宣言 名前のソート ソート式 変数名 var x:X 型 型項 関数名 function f:(x:X, y:Y)->Z プロファイ…

Sを指標圏、Lを論理ドクトリンとするハイパードクトリンH:S→Lがあるとする。Σ∈|S| に対してH[Σ]は指標Σ上の論理圏であり、その論理圏は論理ドクトリンLに所属する。ハイパードクトリンHをインデックス付き圏とみなして、そのグロタンディーク平坦化をTheo(H)…