…。 リテラチャーは、インスティチューション用語の指標圏と同義。高次セオリー構造からインスティチューションを作るときは、リテラチャーを指標圏として使う。 「アンビエントと特定されたインスタンス」の関係は「リテラチャーと特定された指標」の関係と似ている。意味論側が「アンビエント／特定インスタンス」で、構文側が「リテラチャー／特定された指標」である。 セオリーを指定・特定・定義するとは、すべての次元＝レイヤーに渡って、リテラチャーから指標を特定し、アンビエントからインスタンスを特定…

… 20120426 インスティチューションとホーア論理 20111110 これにフビニの定理への期待が書いてある。 インデックス付き圏のフビニ／グロタンディーク同値 20111102 入れ子になったインデックス付き圏 インデックス付き圏を使ってオブジェクト指向風計算を定式化してみる 20110318 インスティチューションと Categories-as-Types 20110208 デカルト圏の掛け算から作るインデックス付き圏の例 20110201 ホーア論理の圏論的な定式化…

…単項セマンティクス（インスティチューション） Lit -- リテラチャー生成子（謎） Expr -- 式生成子（随伴の片割れ） ほんとに重要なのは、ΣkとIk、レイヤー(k+1)があると、Σkを選ぶことが出来て、選んだΣkからインスタンスIkを選べて、レイヤーkが完成する。無限タワーとしてのセオリーを構成可能な背景をセオリー・フレームワークと呼ぶ。セオリー・フレームワークΨ上で構成された全てのセオリーからなる類をTheory(Ψ)と書く。Theory(Ψ)は少なくとも1-圏に…

…-セオリーから自然にインスティチューションが出てくる。n-セオリーまず、n-セオリーのk-段階（k-階層、次元k）の定義： (At dimension k): Σk∈0k-Spef[Σk+1], Ak∈0k-Mod[Σk+1](Σk, Ak+1) Ck := k-Mod[Σk+1](Σk, Ak+1) k-Mod[Σk+1]:k-Spef[Σk+1]×Ck→Ck k-Mod[Σk+1](σ, X) := Ck+1↑[Freek(σ), X] ここで、C↑[X, Y] は、Cが…

…のに向いている構造がインスティチューションだが、そのインスティチューションでも、とこかしっくり来ないことがある。インスティチューションをJとして、ModJ(Σ) をモデル圏とする。モデル圏は単項引数で決まるが、これは、ModJ(Σ, C) と二項であるべきだ。二項にすることによって、説明できることが拡がる。例えば、F:C→D で誘導されるセマンティック圏Cの切り替えが説明できる。 ModJ(Σ, C)→ModJ(Σ, D) 例えば、Set→Boolに基づくセマンティック圏の切…

…ぎだと思うので： トランスフォーマー： 現状、これを使っている。問題は、自然変換のトランスフォーメーションと似ていること。 リダクト： インスティチューションではリダクト関手（reduct functor）と呼ぶ。が、一般的な言葉ではない。 アダプター： アダプター・パターンにちなむので、悪くないと思うが、インパクトが弱い。 ブリッジ： 一般的過ぎるような。 ミューテーター： 生物の突然変異だから語感がどうだろ？ 日本語にすると、変更手か、それはモディフィケーションと似てる。

…Komの米田埋め込みは次のように記述できる。 Ω |→ n-Kom(-, Ω) Ωはシステム指標〈コア指標 | 組み込み指標〉と考えると、システム指標を決めるごとにエルブラン・モデル関手が決まることに対応する。エルブラン・モデル関手またはタルスキー・モデル関手は、インスティチューション（エルブラン・インスティチューション、またはタルスキー・インスティチューション）を決める。Ω→Σ in n-Kom があると、インスティチューションのあいだの準同型が決まる。こんな感じだと思う。

…は、モデル論も含めてすべてコムのなかで出来ることを意味する。課題は、コンピュータッド、構文モナド（のクライスリ圏）、インスティチューション（のグロタンディーク平坦化）との関係だろう。それと、指標の圏＝コンピュータッドの圏でいいだろうが、指標射は写像ではなくてコボルディズムだと思う。多様体のコボルディズムなんかとは比べ物にならないほどの柔軟で、すべてのコンピュータッドは一点（自明なコンピュータッド）へのコボルディズム＝錐体を持つ。コボルディズムという言葉が適切かはあやしいけど。

…間の宣言空間」となる。モジュール名は、意味領域にはなくて、構文領域にあるから。構文領域側の名前空間が「名前空間の宣言空間」の実体になるだろう。インスティチューションを持ち出さないと解釈できないと思う。代数的データ型、余代数的データ型とかもそうだけど、インスティチューションとそのモデル圏、モデル圏のなかでの構成（極限や余極限）がないとうまく説明できない。[追記]entityのcontainerという概念も面白い。TypeScriptは割とマジメに名前構造を考えている。[/追記]

…を考えてないせいだと思う。指標の圏を境界付き高次箙の圏とみなして、それが生成する高次圏をモデルと考える必要がある。インスティチューションの意味でのモデル関手は、指標圏からドクトリン（構造付き圏の2-圏）への関手となるが、余デカルト閉構造をデカルト閉構造に写す。およそ、 〚Σ # Γ 〛 = 〚Σ〛×〚Γ〛 〚Σ ∸ Γ〛 = 〚Σ〛〚Γ〛 スローガンとしては、 足し算が掛け算に、引き算が指数ベキに写る 足し算／引き算は指標の工作であり、モデル側の指数ベキは関手圏で与えられる。

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

…ランモデルで作られるインスティチューションをレイヤー0（L0）と言うことにする。L0の上にレイヤー1インスティチューションを構成するのが問題なのだが、結局、レイヤー1はレイヤー0と同型である、という事だと思う。ただし、レイヤー1はレイヤー0よりはるかに使いやすいので、人はレイヤー1を使う。 上昇埋め込み定理： レイヤー0はレイヤー1にインスティチューションとして埋め込める。 下降レイフィケーション定理： レイヤー1はレイヤー0にインスティチューションとして埋め込める。 レイヤ…

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

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

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

…ている。 ML用語 インスティチューション用語 ストラクチャ S 指標 S SからTへのファンクタ TからSへの指標射 SからTへのストラクチャ変換 SからTへのリダクト関手 インスティチューションでは、リダクト関手が指標射に対して反変（インデックス付き圏の定義）となるが、変換子＝MLファンクタでは最初から反対圏で定義しているので、変換子とリダクト関手は共変になる。この事実が、変換子を関手（ファンクタ）と呼ぶ所以〈ゆえん〉。 MLファンクタは変換子だが、変換子はリダクト関手と…

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

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

…ータ圏の基礎射 計算インスティチューション〈compute institution〉： 指標をベースに作られるインスティチューション セオリー・インスティチューション〈theory institution〉：仕様〈セオリー対象〉とセオリー射により作られる圏を指標圏として、エルブランモデルをモデルとするインスティチューション。 望まれる定理： ゲーデル／カリー／ハワードの定理： ゲーデル／カリー／ハワード・レイフィケーションにより、セオリー・インスティチューションは計算インステ…

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

…シングを組み合わせてインスティチューションを作れるだろう。このインスティチューションを非制約インスティチューション〈unconstrained institution〉と呼ぶ。非制約インスティチューションのなかでは、論理式〈formula〉と定理・公理・証明と推論規則がハイパードクトリンとして備わっているが、指標圏＝インデキシングのベース圏では、プロファイリングしかしてなくて、論理的制約はまったく使われてない。論理的制約を指標の命題部〈命題セクション〉と規則部〈規則セクション…

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

…ー／インスタンスは、インスティチューションのモデルになる。モデル射は、ひとつのシグニチャ／仕様の自己トランスフォーマーの特殊なもの。一般のトランスフォーマーにより、モデル圏のリダクト関手が定義される。リダクト関手は、指標射＝トランスフォーマーで誘導される。仕様の指標部で、定数名、関数名、述語名（基本命題名）が定めるから、対応する論理言語の論理式としてSen[Σ]が決まる。仕様の命題部でSen(Σ)は既に使っている。Mod[Σ]の作り方から言って、X∈|Mode[Σ]| は仕様…

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

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

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

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

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

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

…識する必要がある。インデックス付き圏のベース圏（インデクシング圏）は論域の圏から指標（型文脈）の圏に拡張して、各指標の上に乗っかる命題と定理（＝証明）の圏を論理圏と呼ぶことにしよう。指標Σの論理圏をLogic[Σ]とする。|Logic[Σ]| = Sen[Σ] としてインスティチューションと関係が付く。充足関係を |Mod[Σ]|×Sen[Σ]→{true, false} から拡張して、Mod[Σ]×Logic[Σ]→Ω としたい。Ωは、Logic[1]から作った真理値の圏。