シャドーイングは、現実的には頭の痛い問題で、認める／認めないの判断（決断）が必要だ。が、理論的には特に問題ない。シャドーイングは入れ子スコープで起こるが、「入れ子にすること」を指標のマージだと解釈する。マージは余ファイバー和と解釈する。余…

モノグサはプログラマの美徳と呼ばれる。モノグサ精神は進化の原動力となるが、同時に理論的整合性を崩したり、混乱と錯誤の元凶ともなる。モノグサ精神は： 記述量を減らしたい、略記したい オーバーロードしたい 名前を考えたくない、名前を付けたくない …

相対指標とパラメータ化指標は同じ概念である。が、相対指標は原理的で、パラメータ化指標は実用的。Σが指標のとき、指標に出現するすべての名前の集合を全名前集合〈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〉に分けて考えたほうがいいようだ。基本射は、コンピュータッドとしての射。拡張…

入門的ではない型クラスの話：Haskellの型クラスがぁ (´^｀;) オーバーロードは何故にかくも難しいのか：Haskellの成功と失敗 Haskellの型クラスに関わるワークアラウンド JavaScriptで説明するオーバーロード解決

弱2-圏 モナド論をヒントに圏論をする（弱2-圏の割と詳しい説明付き） 弱2-圏内のモナドに関する補足：モナドが作る2-圏の多様性 米田 困った時の米田頼み、ご利益ツールズ 「確率変数」の一般論は可能か 2次元の圏における米田の補題がわからない ラックス…

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

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

nに対して、n-指標はn-セル＝n-項までを持つコンピュータッドとして定義される。n-指標はn-コンピュータッドだから、n-圏を生成する。このn-圏に、(n+1)-射の族を追加する役割が(n+1)-表明。n-指標と(n+1)-表明の組み合わせがn-仕様（(n+1)-仕様ではない）。…

今までのレイヤー0 → レイヤー1 今までのレイヤー1 → レイヤー2 レイヤー1の論理とレイヤー2の論理に変更する。 レイヤー1 レイヤー2 論理代数 構造付き集合 構造付き圏 議論域 単なる集合 単なる圏 論理代数のレパートリ 具象圏 具象2圏 n 議論域の圏 集合…

変数宣言 vars {x:real, y:real} 代入系 subst :vars {x:real, y:real}->>vars{s, t:real} {s := x + y, t := x - y} インターフェイス interface { ... } アダプター adapter : List ->> Stack { ... } 用語： 構文形式として、まとめて記述するためのレコ…

構文 レコード ::= '{' 文並び '}' 文並び ::= 空 | 文並び ';' 文 文 ::= 空文 | 宣言文 | 定義文 宣言文 ::= 種 名前 プロファイル 定義文 ::= 種 名前 ':=' 項種付きレコードは、 種付きレコード ::= 種 レコード種〈区分 | division〉を列挙： type func…

value x:X を function x:->X の略記とするなら、type X:Set を functor X:->Set の略記と考えることが出来るな。 Cat in Doctrines functor F:C->D in Cat functor X:->C 略記⇒ type X:C トランスフォーを使うと： 1Cat in 2Cat(Doctrines) 1transfor F:C->…

ゴグエンが、指標の圏にはインクルージョン構造が必要だといっていた。ΔからΣへのインクルージョンはあってもひとつだから、Δ⊆Σ という記法が意味を持つ。Δ⊆Σのとき、引き算Σ＼Δが意味を持ち（持たせて）、Σ Σ＼Δ # Δ が成立するようにする。そうすれば、変…

最初に与えられるハイパードクトリンとエルブランモデルで作られるインスティチューションをレイヤー0（L0）と言うことにする。L0の上にレイヤー1インスティチューションを構成するのが問題なのだが、結局、レイヤー1はレイヤー0と同型である、という事だと…

データ型と型シノニム - 檜山正幸のキマイラ飼育記 メモ編 で、コンプリヘンションとコンビネーションと言ったが、 コンプリヘンション（了解） コンストラクション（構成） にする。定義を、 了解〈コンプリヘンション〉による定義 構成〈コンストラクショ…

nomenclatureはだいたい「ノメンクラチャー」 -- 学名命名法、専門語、学名、術語 といった意味で、ここでは「術語法」といった意味。おバカ風は： キモい パねぇ キョドる カミ（神）ってる ググる KY（空気読めない）、YDK（やれば出来る子）、BBA（ばばあ…

システムボキャブラリーは、2つの構成要素からなる。 ディヴィジョンに付けるラベルの集合 パーザーに変更を加える構文マクロの集合 キーワード（予約語）のほとんどは、ディヴィジョンのラベル。したがって、ディヴィジョンのラベルを変えると雰囲気がガラ…

HaskellやMLで、データ型と型シノニムの違いがある。この違いは、関数定義において、“再帰スキーマやイプシロン式で定義する”のと、“通常の関数定義する”のとの違いと類似だろう。スキーマとは、「これこれの性質を持つモノ」という性質記述をすると、その存…

ハイパーインスティチューションの構文論のために、名前の理論とディヴィジョニング／プロファイリングの理論が必要。名前と記号は同義語。名前に対する概念： 有意名： 意味＝意味的割り当てが決っている名前。これは意味論的概念。 ディヴィジョン付き名：…

変換子〈substitutor | 代入子〉は、指標射〈signature morphism | base morphism〉と同義語だが、射の向きは違う。つまり、変換子はSigopの射になっている。 ML用語 インスティチューション用語 ストラクチャ S 指標 S SからTへのファンクタ TからSへの指標…

ダメさ 困ったバンドリング→ 分離分割する。 困ったエンタングルメント →絡み合い・もつれ合いをほどく。 Coqの場合は、名前が漏出する。 骨絡みの欠陥なので、修復不可能。再設計、再実装。名前管理・オーバーロード機能と構造記述機能を別に持つ。MLの型ク…

ハイパーインスティチューションの目指すところは、an overall framework for computing and logic だ。主要な道具は indexed/fibred/parametrized computads だ。アイディアの源泉は、hyperdoctrineとinstitution。

プログラミングとの対応 プログラミング ハイパーインスティチューション インターフェイス 指標 インターフェイスのハード実装 モデル インターフェイスのソフト実装 指標への射 インターフェイス上のプログラム 指標からの射 インターフェイスのアダプター…