指標とモデルと意味論

昨日 代数的定義形式とアンビエント構造 - 檜山正幸のキマイラ飼育記 メモ編、次の用語を導入した。当たり前で自己説明的な言葉だと思う。

• (n-)?代数(的)?定義(形式)?
• (n-)?定義(形式)?

同義語が：

1. (n-)?指標
2. (n-)?仕様
3. (n-)?セオリー
4. (n-)?型クラス
5. (n-)?インターフェイス
6. (n-)?仕様モジュール
7. (n-)?モジュール仕様
8. (n-)?スキーマ
9. (n-)?プレゼンテーション
10. (n-)?表示
11. (n-)?表現
12. (n-)?生成系
13. (n-)?コンピュータッド
14. (n-)?ポリグラフ

定義形式＝コンピュータッドの構成素は、

1. (生成)?アロー〈(generating)? arrow〉
2. (生成)?セル
3. (生成)?射
4. 生成元〈generator〉
5. データ〈data〉

モデルについては、

1. モデル
2. 代数
3. インスタンス
4. セマンティクス
5. デノテーション
6. 表示

次も同義語または類語。

1. 宇宙
2. ユニバース
3. 世界
4. ワールド
5. 銀河（檜山使用）
6. アンビエント
7. 環境

アンビエントの実体は：

1. 具象n-圏
2. ドクトリン
3. レルム
4. ブランド

次もだいたい同義。

1. 射
2. 準同型(射)?
3. アロー
4. セル
5. 演算
6. オペレータ
7. オペレーション
8. 関数
9. 写像
10. マップ

計算システムは、システム指標とシステムモデルで決まるが、システムの同義語は

1. {計算 | コンピューティング}?{システム | モデル}
2. {仮想 | 抽象 | 概念}?{計算機 | マシン | 機械 | コンピュータ | システム}

システム指標は、

1. システム指標
2. コア指標
3. 組み込み指標
4. 基本指標
5. 基礎指標〈ground signature〉

システム指標とシステム・セマンティクス〈システム代数 | システム・モデル | システム意味論〉が決まっていると、Σからシステム指標Ωへのクライスリ射はΣのセマンティクス〈代数 | モデル | 意味論〉を誘導する。

システムとそのあいだの準同型の圏をシステムの圏Systemと呼ぶと、セマンティクスの圏SemanにSystemは埋め込める。ここで、圏Semanは、クライスリ射〈置換〉の圏から集合圏Setへの関手を対象として、自然変換を射とする関手圏。

S∈|System|に対して、Sが定義するセマンティクス〈意味論〉をSem_S、または〚-〛_S と書く。Sem_S = 〚-〛_S : Subst→Set

意味論関手 Sem:System→Seman はさらに2つのパラメータを含む。

1. プログラミング言語L
2. セマンティック圏C

プログラミング言語Lは、型システムを決める2-モナドT_Lと、値計算システムを決める1-モナドC_Lからなる。T_Lが型演算を決め、C_Lが値演算を決める。プログラミング言語（実体はモナドの組）とそのあいだの準同型は圏ProgLangを形成する。プログラミング言語のあいだの準同型は、モナドのあいだの準同型なので、2つのモナド準同型を組み合わせた形をしている。