Jack of All Trades, Master of None

器用貧乏系情報科学徒のメモ

クリプキフレーム Kripke frame

用語

クリプキフレーム Kripke frame

そう言えばクリプキフレームの話を書いていなかった事を思い出したり(クリプキフレームの話なんて素敵なpdf (http://www.is.titech.ac.jp/~kashima/manuscript/03Sept.pdf )がネット上に溢れているので、わざわざ書くようなことでもないような気もしますが………)

定義

クリプキフレーム $\mathfrak{K}$ は次の２つ組で定義される.

$\mathfrak{K}=(K, \mathfrak{m}_{\mathfrak{K}})$

ここで、 $K$ は状態と呼ばれる集合、 $\mathfrak{m}_{\mathfrak{K}}$ は意味付け関数(meaning function)と呼ばれる.

例えばこの定義のもとで動的命題論理の意味論を考えてみる. 命題 $p\in\Phi$ 、プログラム $a\in\Pi$ について意味付け関数 $\mathfrak{m}_{\mathfrak{K}}$ が次のように与えられる.

$\mathfrak{m}_{\mathfrak{K}}(p) \subseteq K, \mathfrak{m}_{\mathfrak{K}}(a) \subseteq K \times K$

このとき、意味付け関数の直感的な意味は、ある命題pを満たすような状態の集合、あるプログラムaの実行に相当する遷移関係の集合を与えているようなものであると考えることが出来る.

[そのうち加筆修正]

参考文献

amazonリンクで恐縮ですが

www.amazon.co.jp