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

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

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

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

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

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

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

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

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

基本的な概念と用語： まだ曖昧な所があるが、 区分〈くぶん | 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） | 型クラス・インスタンス | セオリー} プロファイリング ： ストラクチャのメンバーの一部 バインディング ： ストラクチャのメンバー…

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)…

計算解釈 論理解釈 項 証明 項ブロック 証明ブロック ユニット型 真 エンプティ型 偽 型 命題 型構成子 論理結合子 依存型構成子 限量子 定数 公理 関数 定理 関数の定義項 定理の証明 関数のヘッダ 定理のヘッダ 定数・関数名 公理・定理ラベル 関数コンビ…

ドクトリンは、CCCのような、Cat上の具象圏だとする。ハイパードクトリンは拡張されたドクトリンくらいの意味だが、 ベース圏（論域の圏）の上のインデックス付き圏であり、余域はCCCのようなドクトリンになる。 ベース圏の射に対して、ΣΔΠ随伴性がある。Σは…

ハイパードクトリン インスティチューション ベース対象 型コンテキスト 指標 ベース射 コンテキスト拡張／置換 指標射 ファイバー 命題の圏 モデルの圏 誘導関手 引き戻し リダクト関手 随伴関手 限量子 - 妥当性 - 充足関係 こうして見ると、限量子随伴性…

カリー／ハワード対応を信じるなら、関数の記述と定理の証明はまったく同じはず。だったら同じ書き方ができるはず。 // f:X×Y→Z function f given x:X, y:Y ensures Z begin ... end // t:A∧B→C theorem t given a:A, b:B ensures C begin ... end関数定義に…

管理・配布のメカニズム パッケージ バージョン（パッケージに付く） スクリプト（物理的にはファイル、拡張子は.tenjinscript） モジュール（スクリプトに制限を付けたもの、拡張子は.tenjin） リポジトリ インターネット上でパッケージを保存している場所 …

定理記述 - 檜山正幸のキマイラ飼育記 メモ編の続き。少し変える。 theorem 定理の名前 import モジュール1, モジュール2 for 宣言1, 宣言2 given 命題1, 命題2 ensures 命題 begin 証明 end endproofという語は避けた。 圏論 論理 始対象 False 終対象 True…

名前空間の構造化に関連する概念 名前空間の親子関係 シャドーイング 入れ子名前空間（ブロックスコーピング） 上掛け（overlay）名前空間 大域名前空間 名前付き名前空間 無名名前空間 名前空間もオブジェクトと考えてツリー構造をなす。ルートノードの名前…

コマンドは、先頭が動詞原型または動詞過去分詞形、それに続いてキーワード目的語名詞が続いてもいい。apply, make conjunction, found inconsistency など。「命題 by 根拠名詞 引数並び」でも証明が書けるとする。以下、根拠名詞とコマンド動詞の対応表。 …

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。 公理 公理証明 ax_A : * -> A * ----[ax A] AAx⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、 a : X -> A X ---[a] Aつまり、Ax⊆Mor(C)。Axはどん…