指標の意味論
CafeOBJで、タイト意味論とルーズ意味論という言葉を使っていたが、いまいちハッキリしないので、次の3種に分ける。
- ホール〈whole | 全体〉意味論
- 始対象意味論
- 終対象意味論
Σが指標のとき、〚Σ〛をどうするか、という話。これをハッキリさせないで指標の話をしてもしょうがない。
- 〚Σ〛= Mod[Σ] = Σのモデル圏 = Σ-マグマの圏
- 〚Σ〛= Init(Mod[Σ]) = Σのモデル圏の始対象を選ぶ
- 〚Σ〛= Fin(Mod[Σ]) = Σのモデル圏の終対象を選ぶ
上から順に、ホール意味論、終対象意味論、終対象意味論となる。次の例：
signature nat := {
nat in Set,
0 : nat,
s : nat-> nat
}この指標を満たすモデル（マグマ）は付点離散力学系というべきもので、いくらでもある。Set上のnatのモデルの全体をMod[nat]とすると、この圏の始対象が自然数。
- Nat := Init(Mod[nat])
始対象意味論を使った対象の定義（記述的な定義で、up-to-isoで決まる）が代数データ型で、次のような略記（構文マクロ）である。
- 略記： data foo := Σ
- 意味： foo := Init(Mod[nat])
data Σ が Init(Mod[Σ]) のリテラル表記だと思ってよい。
終対象意味論は、余代数指標に対して使われる。オブジェクト指向の意味論。隠蔽ソート（隠蔽型記号）が1個あると、状態遷移系になるので、いちばん一般的な状態遷移系として、指標の意味が定まる。インターフェイスから理想的な実装が一意的に定まる状況になる。マイヒル／ネロード型の定理。
他に記述的な定義としては、不動点意味論がある。不動点スキーマから、そのスキーマを満たすパラメータ付き不動点が一意に決まることを利用して射をup-to-isoで確定する。
- initial または data
- final または codata
- fixpoint
くらいのキーワードがあれば、記述的な定義はだいたい出来るだろう。
