不動点理論に悩む

研究 基礎理論

形式的手法のサーベイをおこなっていると、やはり不動点は避けて通れない。
前出のKripke構造のところであったが。まずは

  • least fixedpoint: $\mu Z.\tau(Z)=\cap\{Z|\tau(Z) \subseteq Z\}$
  • greatest fixedponit:$\nu Z.\tau(Z)=\cup\{Z|\tau(Z) \supseteq Z\}$

というのが難問だなあ。どうして\tau(Z) \subseteq Zになるものの下限（下のぎりぎり）が最小不動点になるかな？

>>と思ったが、絵を書けば一目瞭然だった。

さらにそれが、時相論理にからみかたも今一歩明確ではない。
そりゃ

EG f_1 = \nu Z.f_1 \wedge EX Zというふうに言われますけども

なんかよくわからん。

>>と思ったが、f1が成立しかつ次のパスがあることがずっとなりたつ。
>>と解釈すれば何となく納得。