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

本編では、けっこうTypeScriptについて書いているんだな。 随伴のニョロニョロ関係をTypeScriptで確認する - 檜山正幸のキマイラ飼育記 クロージャなんて貧乏人のオブジェクトだろ - 檜山正幸のキマイラ飼育記 お手軽で実用的なジェネリックスへの道は遠い -…

VSCodeを使う動機があんまりないから、VSCode上でTypeScriptを使うことにしようかと。TypeScriptでは、既存のJavaScriptライブラリにおける型を定義した *.d.tsって型定義ファイルが必要なのだが、 TypeScriptをインストールしたディレクトリのlib/に、lib.*…

必要なもの - 檜山正幸のキマイラ飼育記 メモ編の話。ボチボチ準備、年末年始には片付けたい。 Firefox 設定情報のバックアップhttps://support.mozilla.org/ja/kb/back-and-restore-information-firefox-profiles 同期→ https://support.mozilla.org/ja/kb/…

事情 - 檜山正幸のキマイラ飼育記 メモ編 以来。まず、自分にとって必要なもの。 とりあえず入れる Firefox Chrome Google日本語入力 Tera Term iTunes LINE PDF Reader EpsonScanドライバとマニュアル（自動で入ると思う） エディタ Emacsはやめようかと思…

サル、いやガキ（園児）でも使えるGUIとは - 檜山正幸のキマイラ飼育記

自然演繹系のUIをglobular風にする。 globular 自然演繹系 パレット パレット セル 項（ターム） ラベル ラベル（名前） 色 (なし) 次元 次元 ダイアグラム 式 キャンバス ノート キャンバスビュー ノートエリア コマンド コマンド コマンド Globularのコマ…

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

関数〈かんすう〉 関数〈function〉 関数〈写像〉 関数〈かんすう | function | 写像〉 写像〈mapping | map | 関数〉

変数宣言 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 { ... } 用語： 構文形式として、まとめて記述するためのレコ…

googleアカウントでログインしているなら、 https://drive.google.com/drive/my-drive というURLが自分のドライブを指す。 上部の[My Drive]のドロップダウンメニューから"New folder"でフォルダを作れる。 左ペインの[My Drive]はツリービューを提供する。 …

構文 レコード ::= '{' 文並び '}' 文並び ::= 空 | 文並び ';' 文 文 ::= 空文 | 宣言文 | 定義文 宣言文 ::= 種 名前 プロファイル 定義文 ::= 種 名前 ':=' 項種付きレコードは、 種付きレコード ::= 種 レコード種〈区分 | 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の型ク…

参考： MLソースを扱うとき - 檜山正幸のキマイラ飼育記 メモ編 デスクトップにIsabelle2016（少し古い）のアイコンがある。 このアイコンは C:\Installed\Isabelle2016\Isabelle2016.exe を指している。 Isabelle2016.exeの実体は、jEditをフロント、PolyML…

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

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

言語サーバープロトコル - 檜山正幸のキマイラ飼育記 メモ編 Isabelle風の継続的同期＆チェッキングだと、もっと細かく精密な通信が必要になる。 次のことが必要。 ソース完全保存性 テキスト編集可能性 構造編集可能性 構文解析木の豊かな情報を付加して、…

2015年に、「言語処理サーバーとそのプロトコル」という記事を書いたけど、Microsoftはこの方向を追求しているね。 https://langserver.org/ The Language Server protocol のページ 言語サーバープロトコルのドキュメントは、 https://github.com/Microsoft…

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

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

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