…から、これは命題と伴意順序〈entailment order | 論理順序〉の圏と考えてよい。2-代数としてデカルト閉圏とかを使う。1-論理と2-論理が無関係にあるのではなくて、 1-論理から2-論理を作り出せる。 1-論理を、作った2-論理に埋め込める。 2-論理を、1-論理にレイフィケーション出来る。 こういう条件を満たす多レイヤー論理系をハイパーインスティチューションと呼ぶのだった。1-論理から2-論理をモデル圏も含めて作り出す手法をゴグエン／エルブラン構成と呼びたい。

…隠語、といった意味。ハイパーインスティチューションの場合、聞き慣れなく長ったらしい用語がたくさん出てしまうので、いっそのことおバカ風にする。 英語 動詞的名詞 日本語 value assignment 付値 term attachment 着項（造語） profiling プロファイリング divisioning 区わけ おバカ風： 動詞的名詞 語幹 動詞 受動形 付値 フチ フチる フチった 着項 チャコ チャコる チャコった プロファイリング プロフ プロフる プロフった…

システムボキャブラリーは、2つの構成要素からなる。 ディヴィジョンに付けるラベルの集合 パーザーに変更を加える構文マクロの集合 キーワード（予約語）のほとんどは、ディヴィジョンのラベル。したがって、ディヴィジョンのラベルを変えると雰囲気がガラッと変わる。ディヴィジョンは本来、圏名と次元だから、ラベルをどう変えても大丈夫。ディヴィジョン構文は、@Set@1 とか @Logic[unit]@0 とかの変な構文でもいいかも。ボキャブラリー定義は、 keyword type @Set…

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

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

…応 プログラミング ハイパーインスティチューション インターフェイス 指標 インターフェイスのハード実装 モデル インターフェイスのソフト実装 指標への射 インターフェイス上のプログラム 指標からの射 インターフェイスのアダプター 一般の射 インターフェイスのソフト実装は、「インターフェイス下の」のプログラミングと言える。指標射は、置換または代入ともいうが、あまりに普通の言葉なので、少し変えて 置換子／代入子〈substitutor〉と呼ぶ。代入子は、指標のあいだの射である。…

基本的な概念と用語： まだ曖昧な所があるが、 区分〈くぶん | division | ディヴィジョン〉： 特定の圏Cと次元数kのペア。Cのk-射の集合を意味する。 区分ラベル： 区分に付ける人間可読なテキスト。 区分け〈くわけ | divisioning | ディヴィジョニング〉 ： 名前に区分を割り当てること。 プロファイル： 高次圏のホムセットのこと。0-ホムセットは対象全体の集合とする。 プロファイリング： 名前にプロファイルを割り当てること。 接着〈attach〉： …

ハイパーインスティチューションは、3×3のマトリックスで整理できる。縦横どう書くかは自由だが、3ロール×3レイヤーと呼ぶ。 ロール： ベース（Base）ロール、論理（Logi）ロール、モデル（Mode）ロール レイヤー： アンビエント（Ambi）レイヤー、計算（Comp）レイヤー、セオリー（Theo）レイヤー マトリックスの成分（欄）には圏が入るが、圏の名前は、 レイヤー名ロール名 以下に列挙。 ↓レイヤー＼ロール→ Logi Base Mode Ambi AmbiLogi …

…ューション、あるいはハイパーインスティチューションと呼ぶ。ハイパーインスティチューションに関して、次の定理が欲しい。 エルブランの定理： ハイパーインスティチューションのモデル圏はエルブランモデルだが、同じ構文的インデキシングを持つ、どんなインスティチューションに対しても、そのインスティチューションにおける真概念は、エルブランモデルのインスティチューションで確認できる。したがて、エルブラン・インスティチューションだけを考えておけば良い。 ゲーデル／カリー／ハワードの定理： ハ…

…対象であると同時に、ハイパーインスティチューションのモデル圏のコンピュータッド＝生成系＝プレゼンテーションになっている。指標は、命題部分が自明な仕様なので、指標を仕様に埋め込める。仕様は、構造〈インスタンス | 絶対セオリー | 基礎セオリー〉に対する公理的規定〈axiomatic {regulation | standard | norm}〉（定義とは言わない！）を与える。仕様の命題部分から導出閉包（導出される命題の反射的推移的閉包）を作れる。導出閉包には証明（定理〈論理射…

…充足する保証はない。ハイパーインスティチューション（あるいはグロタンディーク／エルブラン・インスティチューション）のモデル圏は、エルブラン・モデルとして定義される（だからエルブランを冠している）。 ドクトリン → ベック（by Jon Beck） ハイパードクトリン → ローヴェル（Bill Lawvere） 平坦化／ファイバー化 → グロタンディーク（Alexander Grothendieck） 構文的項モデル → エルブラン（Jacques Herbrand） グロタン…

…が出来る。この貼り合わせが大局的プログラミングに相当する。もとのアンビエント圏、またはベース圏（アンビエント圏と名前から作った圏）における射（＝プログラム）の構成が小局プログラミング。グロタンディーク／エルブラン圏に対して余スライス構成をして作ったインスティチューションをハイパーインスティチューションと呼ぶ。Modの作り方は自明だが、Senがいまいち分からない。 ハイパーインスティチューション＝ハイパードクトリンのグロタンディーク／エルブラン圏上の余スライス・インデキシング。

当然にインスティチューション 当然に述語論理＝ハイパードクトリン 限量子随伴性 ＝ ΣΔΠ随伴性 否定があるなら、否定双対性。スター自律圏かな？ 継続との関連は？ 契約は仕様と関連するから、メイヤー先生のDbCとは関連する。 仕様モジュール、セオリー・モジュールを扱うので、モジュール計算＝大局的プログラミングと関係する。 仕様記述は仕様モジュールの書き方だろう。 モデル圏が余代数の圏ならば、模倣、双模倣と関係すると思う。 モデル圏のスペクトラムが作れるのでは？ リンデンバウム…

…ドクトリン（さらにはハイパーインスティチューション）から作られるセオリーの圏の構造を把握すれば、STEM記述フレームワークの基礎が固まるだろう。用語の比較： 論理 オブジェクト指向 関数型 指標 インターフェイス 型クラス 仕様 表明付きインターフェイス 表明付き型クラス 絶対セオリー クラス インスタンス 相対セオリー なし MLのファンクタ？ パッケージ／モジュールと、仕様／セオリーは独立な概念であるが、管理単位と論理単位を一致させるなら： 仕様（spec）モジュールで仕…

…定義項 定理の証明 関数のヘッダ 定理のヘッダ 定数・関数名 公理・定理ラベル 関数コンビネータ 定理コンビネータ＝手続き 原始コンビネータ 推論規則 ただし、ハイパーインスティチューションのなかでは、あまりカリー／ハワード対応を重要視するべきではない。対応が重要なのではなくて、ベースドクトリンと論理ドクトリンが同一の構造を持つというだけのこと。計算解釈はベース圏に対して使い、論理解釈は論理圏に対して使う。2つの解釈を同一視するのではなくて、共通性を意識しながらも使い分ける。

…徴ということになる。ハイパーインスティチューションを定義するには、 限量子随伴をインスティチューションに取り込む。 充足関係をハイパードクトリンに取り込む。 我々の目的は型クラスのセマンティクスなので、ハイパーインスティチューションのグロタンディーク平坦化がうまくできないと困る。 型クラス（＝対象）のインスタンシェーションがうまく定義できる。 型クラス（＝対象）のコンビネータがうまく定義できる。 トランスレーション（＝射）がうまく定義できる。 トランスレーションのコンビネータ…

…トリンのグロタンディーク平坦化）の対象。トランスレーションが射となっている。したがって、型クラス・コンビネータは圏TypeClass上の圏論的オペレーターとなる。やっぱり、ハイパードクトリンとインスティチューションを組み合わせたハイパードクトリン的インスティチューション＝ハイパーインスティチューションが必要そうだ。ハイパーインスティチューション＝述語論理とモデル理論。しかし、「ハイパードクトリン」、「ハイパーインスティチューション」なんて言葉は、無闇に壮大そうで厨二病的だな。