演繹付きインスティチューション〈institution with deduction〉を定義する。普通のインスティチューションに、指標Σごとの演繹性判断〈deducibility judgement〉|-Σが付いている。 |-Σは、Pow(Sen[Σ])とSen[Σ]のあいだの（二項）関係 演繹性判断は、次の公理を満たす。 {a} |- a 反射性 A |- a, A⊆B ならば B |- a 単調性 Ai |- ai ならば、∪({ai}|i∈I) |- b ならば、∪(A…

…と同義語 指標 ： インスティチューションやGlobularでは指標と呼ぶ。 アルファベット ： 形式言語理論 スケッチ ： 極限・余極限が入るとスケッチ スキーマ ： スピヴァックの用語 シェイプ ： データ型の理論で使われることがある。 一般論はかなり難しい。次数（degree, rank, grade, dimensioin）付き集合Σ = (Σ0, Σ1) で、次数に沿って構成可能なもので、次数kまでで、Diagk(Σ) が出来るようなもの。このとき、Diagk(Σ)…

リレーショナルと言わずに形容詞もリレーションで済ませる。で、リレーションスキーマとリレーション指標（relational signature）は同義語。Sがリレーション指標とは、Sのインデックスセット|S|があり、ドメイン割り当て δS:|S|→|Set| があること。指標射 j:S→T は、|S|から|T|への単射で、ドメイン割り当てを保つもの。SとTの直和は、インデックスセットの直和として定義できる。空指標があり、直和の単位対象となっている。j, k:S→T に対して、余…

…型クラスがダメなのはインスティチューションを考慮してないから。 オーバロードや型強制のメカニズムがわけわからん。 パッケージマネージャー、ビルドシステム、アーカイブサイトなどを考慮してない。 計算機代数システム（CAS）との連携が不十分。 ドキュメント・システムとして不十分。 コミュニケーションや通知機能がないし、想定もされてない。 証明オブジェクトが人間にとっては難読過ぎてい無意味 フォワード証明かバックワード証明のどちらか一方しかサポートしてない。 論理資源の管理機構が整…

インスティチューションでは、指標Φに対してモデル圏Mod[Φ]が決まる。まーこれはいいのだが、指標圏が何であるか、Mod[Φ]をどう作るかは言及しない。公理的フレームワークだから、まー、そんなもんだ。しかし実際に出現するインスティチューションではもっと細かな構成をしなくてはならない。その構成の方法：基礎圏（ground category）が必要。多くの場合はSetが基礎圏。たくさんの圏が登場するが、それらはすべて基礎圏の上の具象圏、つまり唯一の忠実な忘却関手を持つ。基礎圏をB…

…る圏をモデル圏とするインスティチューションを構成することだ。インスティチューションの指標圏を忘れて、モデル圏の集まりを適当な大きなドクトリンのなかに埋め込むと宇宙（大きなドクトリンの部分ドクトリン）が出来る。一方で、グロタンディーク平坦化により単一の圏にすることもできる。Haskell風型クラスは、宇宙という圏（2-圏の圏骨格部分）にコアージョン構造＝コアージョングラフを導入する。問題点は： コアージョンが（個々のコアージョンもコアージョングラフも）、ユーザーから不可視である…

…ない。意味論的には、インスティチューションで言えば、Σ(Φ∈|Sig| : |Mod[Φ]| ) という集合（類）、Σは直和による総和。あるいはインデックス付き圏をグロタンディーク平坦化した圏の対象類とも言えるが、、、そこまで考えているとは思えない。複パラメータ型クラス（多ソート指標上のセオリーだろう）、so-call"多重継承"の解釈がひどい。 用語、記法 用語や記法が誤解を誘導するよう（ミスリーディング）になっている。 型クラスを単にクラスと呼ぶ。 メソッドとかメンバー関…

…んでさしつかえない。インスティチューションでは実際に「文」（sentence）だ。文を構成する文を、全体に対して相対的に「節」と呼ぶ。基本となる文は基本文とか単純文、接続詞（論理結合子のこと）で構成された文は複合文と呼ぶ。文法で聞いたことがあるような言葉使いだ。AND, OR, NOT, IF（conditional, implication）は特に問題ない。∀、∃の導入が問題。P(x)のような主語変数を含む文（文関数）を意外とスンナリ理解できるから、しばらくはP(x)を全称…

インスティチューションの指標の圏があって、Σ, Φが指標として、基本指標射 σ:Σ→Φ だけでんなくて、モナドFが働いた FΦ を考えて、クライスリ射 Σ→FΦ を使うことは非常に多い。つまり、最初の指標圏をクライスリ圏に拡張して使う。一方で、柱体とホモトピーとの類似から、コスパン Σ→Π←Φ を射とする圏を考えることもある。クライスリ射は、コスパンとみなせるが、結合がうまくない。より一般の結合を探して、クライスリ構成とコスパン構成を統合できないか？

…と。この圏を仮にLaGrand（labelled graphi with end-points）とでもする。ランはラベリングと境界を保存するグラフ写像だから、LaGrandの射となる。ということは、LaGrandの対象は構文的なプログラムコードともみなせるし、意味論的な実行系ともみなせることになる。プログラム変換も、模倣のような実行系のあいだの対応も、一様にLaGrandの射とみなせる。この一様な定式化からの含意（帰結すること）は何だろう？ インスティチューションとの関係は？

ラベル概念がクセモノ。ラベルは遷移グラフの辺に付くナニカだが、 入力となる記号、データ、イベント、メッセージ 出力となる記号、データ、イベント、メッセージ 命令、アクション、コマンドの名前 その他、コンストラクタやオブザーバーの名前 おおざっぱで重要な分類は、データとしての記号か名前としての記号かの別。データとしての記号は意味領域に属し、名前としての記号は構文領域に属する。やっかいなのは、データと名前が入れ替わったりすること。テキスト処理とか構文処理は、構文的存在をデータとし…

型の意味は関手で、項の意味は自然変換だと考える。型である関手の定義域は、「スキーマ、シェープ、指標」などと呼ばれる。型の定義域の全体はまた圏で、スキーマ圏、シェープ圏、指標圏などと呼ぶ。インスティチューションや導来子との類似性がある。 導来子の図式の圏 → スキーマ圏、シェープ圏、指標圏 導来子の値 → 指標に対するモデル圏 導来子の単位圏での値 → モデルのアンビエント圏 おそらく、総称（多相）の説明になるだろう。

Σ、Δが指標とする。Expr(Σ) がΣから構成される式の集合だとする。Exprはモナドになるので、指標圏をモナド付きの圏と考える。このモナドのクライスリ圏の反対圏を考えると、これは「定義の圏」となる。それで、定義の圏においては、指標の直和 Σ+Δ が直積を与える。これはなかなかに象徴的な事実だと思った。

…子の、あるいは多段のインスティチューション。いろいろな圏が出てくる。 Graph -- 有向グラフの圏。自己ループも多重辺も認める、まったく任意のグラフの圏。ただし小さい（たかだか加算で十分）なグラフが対象。 Syn -- 構文的対象（syntactic objects）の圏。対象は、頂点ラベルと辺ラベルが付いたグラフだが、ラベルを頂点そのもの、辺そのものと同一視して、SynはGraphの部分圏と考える。 Exp -- 構文モナド。ExpはSynの上のモナドで、乗法と単位は、…

「インスティチューションだのプロ関手だのなんだの」の「何が必要か」に書いたこと、だいたいの見当は付いたと思う。厳密性がないハナシで、その意味ではマダマダだけど。目的は多段階の設計実装プロセスをきちんと定式化すること。インスティチューション（指標圏からの関手）が値を取る圏が複雑になる。インスティチューションの値となる圏（関手の余域圏）は水平射と垂直射と2セルを持つ二重圏と考えられる。水平射は、豊饒化プロ関手。垂直射は関手のペアで、豊饒化プロ関手と協調するもの。豊饒化プロ関手（圏…

…が、メモしておこう。インスティチューションの定式化と例ボーッと考えていたのは、インスティチューション。 インスティチューションを、もっと使いやすいように変形や拡張ができないか？ インスティチューションの実例で、わかりやすいものはないか？ インスティチューションをバキバキに使いたいなー。 とか。階層付き圏まず、category with inclusions / inclusive category って言葉がどうもイヤだ。category with hierarchy / h…

…。 ホーアトリプルのインスティチューションによる一般化 -- あんまりわかってない。 ペトリネットのマーキングの一般化と双対の定式化 -- 単なる山勘、アヤシイ。 オートマトンの森田同値 -- 当初の目論見はダメだった。で、ほったらかしだが、なんかありそう。 形式言語系を相対モナドを使って定式化できないか？ モナドの作用乗法って何だったのか？ ハイパーリンクをちゃんと書いておいたほうがいい。 境界付きアルファベットって、結局よく分からないまま。なんとかしたい。 [追記]それと…

…オートマトン射、右加群射＝余オートマトン射、双加群射＝トランスデューサー射などを考えると、これはラベル付き遷移系の双模倣と同じ定義になるはずだ。多元環の定義で、「生成系＋関係」による定義があるが、生成系＝指標、関係＝制約、となる。指標＋制約＝仕様＝セオリーだから、仕様（セオリー）の圏は多元環の圏であり、それに対するモデルの圏は、多元環上の加群の圏となっていると思ってよい。インスティチューションがインデックス付き圏の形をしているのは、多元環上の加群の圏とも解釈できるからだろう。

…ンと呼ぶ。もちろん、インスティチューションになる。いつだか忘れたが、昔、IDLの構文に、when accept xxx とか issues Event, results NewState とか、そんなキーワードを入れてinterface構文を拡張しようとしていた。今にして思えば： ステージ遷移とステージ内の状態遷移を記述したかった。 外部からのメッセージ（刺激、イベント）を受け取って、それをきっかけにする動作（イベントハンドリング）を記述したかった。 状態遷移に伴って、外部に…

… sigってなに？（インスティチューションのsigと関係するのか） インスタンスってなに？（アトムとは全然違うが、語感がアトムっぽい） なんで、集合の直積に '->' を使う？ そのココロは？ なんで型システムがあるんだ？ 関係計算だけじゃダメ？ 整数ってなに？ なんで整数だけ付け足しっぽい？ 入れ子タプルは認めてないようだが、強調してないな。直積もフラットな直積になるよな。 一階の対象（タプルの集合）までしか認めてないのに高階論理風の論理式が出てくるけど、あれはなに？ 「+…

…e）と呼んでよい。（インスティチューションの用語法では。） この圏の射は指標射（signature morphism）と呼んでよい。 だが、この圏の射はモジュールであることは事実。 モジュールの英語"module"は加群の意味があるので、category of modules は使えない。 指標圏（category of signatures または signature category）なら使える。 だが、「指標圏」で分かる人はいない。 とりあえず、signatures a…

インスティチューションは概念を整理する枠組みとしては便利だが、中身がまったくないので、インスティチューションから出発してもラチがあかない。なんか実際のモノを作って、後から見たらそれはインスティチューションでした、ってことじゃないとダメだな。で、抽象的インスティチューションに欠けている実質は、指標が何であるか？ 指標の圏が何であるか、指標の圏とモデルの圏をごちゃ混ぜにできるメカニズムなど。構文論がモナドをベースにできることは、非常に確からしい気がする。ので、とりあえず、モナドか…

インスティチューションは、構文とモデルを区別する。もともとがモデル論だから当たり前だ。が、コンピュータでは、その構文領域もデータ領域としてモデルの世界に入り込む。ここが問題。インスティチューションの構造を残しながらも、構文（項）がモデルの世界に入り込むメカニズムが必要だ。モデルMod[Σ]を関手圏AΣとして定義するのがひとつの手かもしれない。圏Aは、定数係数のような外部環境のようなアーキテクチャのような、、、 | --------+-------- モデルの世界（Mod[Σ]…

…するにはどうする？ インスティチューションは必須だ。 プログラミング言語は、構文生成モナドTとプリミティブを与える指標Σとの組だ。 プログラムpは、モナドTのKleisli圏に射として存在するが、Σによるスライス圏の対象と考えたほうがよい。 よって、プログラムp:Σ→Δ は、スライス圏のあいだのプログラム変換関手も定義する。圏の対象でもあり同時に関手でもあるという二重性。 プログラムの生成（creation）、進化（evolution）、リファクタリングなども定義したい。 エ…

帰納的に自由な集合の件だが、有限な代数指標Σを決めて、Σの自由代数＝始対象のことだわな。Σを決めるごとに再帰関数（帰納関数）論ができるから、全体としてはインスティチューション。

…リク半環（n-パリク代数）と呼ぼう。nを固定してのn-パリク半環、またはすべてのnを同時に考えてパリク半環達はどんな圏論的構造を持つのだろう。それが定式化できればパリク圏と呼んでよいだろう。パリク・ベクトルをなんらかの関手とみなして、パリク関手と呼ぶ。パリク関手は、トレース付きモノイド圏、またはトレース付きモノイド圏の族（インスティチューション、インデックス圏）からパリク圏への関手となるべき。パリク圏とパリク関手の基本性質からパリクの定理が自動的に出るようにならないだろうか。

…og) の補足：簡易インスティチューションで定式化してみる。実は簡易インスティチューションにさえなってない略式インスティチューション。どのへんが略式かというと、指標Σに対してMod[Σ]は単なる集合。よって、指標射 Σ→Δ に対するMod[Δ]→Mod[Σ]は単なる写像。さらに、文関手Senは考えない。本編では、クラスという曖昧で直感的な概念を使ったが、ここではクラスを使わない。S={boolean, int double, string}を基本ソートの集合として固定（実はS…

…の例を出す。（多項式インスティチューションについては、多項式インスティチューション - 檜山正幸のキマイラ飼育記 メモ編参照。）まず全体的な対応。 形式言語系 ラベル付き遷移系 多項式 指標Σ ラベル集合Σ 変数集合x ={x1, ..., xn}（無限でもいい） 指標の射 ラベル集合間の写像 変数集合間の写像 Mod[Σ] Σラベル付き遷移系 X上のK付値=レコード=点 構文モナドT クリーネスター 多項式生成関手 Kleisli射 ラベルのマクロ定義 多項式による変数変換…

…イラ飼育記 メモ編 インスティチューションの枠内で、具体的な指標から具体的にモデルを作る話。 指標はグラフ、またはプレ圏。 グラフから自由生成された圏（道の圏）の合同がセオリーになる。 指標が前もってプレ圏（圏でもよい）なら、セオリーは一般化合同。 グラフに境界概念を入れると、隠蔽ソート＝内部ノードができる。 指標の圏には、直和、直積、境界でのグルーイングが入る。 グラフのファイバー和（貼り合わせ）が必要。上江州アタッチメントも貼り合わせ。 指標の圏に、構文生成モナドが働いて…

後で考える／調べる／書く - 檜山正幸のキマイラ飼育記 メモ編にて： 総称は必然なのか？ 必然だと思うが、型クラス、C++のコンセプト（という概念）、型制約、種、スラント圏、インデックスされた圏、インスティチューションなどを考慮して考えるべきだ。