様相μ計算
参考文献
鹿島 亮; "コンピュータサイエンスにおける様相論理"
Modal mu-calculi (HoML)
Handbook of Modal Logicのp721~756
Results on The Propositional μ-Calculus
大雑把なはじめに
論理式の不動点というのを次のように定める
論理式$ \varphi,\xi、命題記号$ pとして
$ \xi = \varphi\lbrack \xi/p \rbrackが恒真となるとき
$ \xiを$ \varphiの$ xに対する不動点とする
$ \xi = \eta x.\varphiと表す(不動点演算子)
例えば
$ \Box^* \varphi = \eta x.(\varphi \land \Box x)
$ \Box^* \varphi \equiv \varphi \land \Box \Box^* \varphiは恒真
$ \alpha \mathsf{AU} \beta = \eta x. \beta \land (\alpha \mathsf{AX} x)
$ \alpha \mathsf{AU} \beta \equiv \beta \land (\alpha \mathsf{AX} (\alpha \mathsf{AU} \beta))
これは$ \Box^*, \mathsf{AU}をそれぞれの論理で$ \Boxだけ($ \mathsf{AU}は$ \Boxと同等の意味)で再定義出来る
つまり正規様相論理Kに不動点演算子を加えた論理はかなり拡張性がある