不動点

不動点(fixpoint)について。
(適当メモなので信用しないように。)

関数の不動点は、f(x)=xとなる点。
んでも、least fixpointとgreatest fixpointという単語がよく分からず調べてみた。
どうやら、両方とも論理学ヨリの単語らしい。
おぼろげながらに理解した部分は、

述語P(x)と、なんか適当な関数f(y)に対して、
再帰定義された述語の、D(x)=P(x)∨D(f(x))みたいなのがあったとする。
これを展開してゆくと

D(x), P(x)∨D(f(x)), P(x)∨P(f(x))∨D(f(f(x)),...

となって、無限の述語を記述できるっぽい。
これが述語のfixpointらしい。

んで、least fixpointというのは、

P(x1)∨P(x2)∨P(x3)∨P(x4)∨... → True

すなわち、あるiに対して、P(xi)が成り立つこと。

greatest fixpointというのは、

P(x1)∧P(x2)∧P(x3)∧P(x4)∧... → True

すなわち、全てのiに対して、P(xi)が成り立つこと。
と理解した。

別の資料では、上をFinally、下をGloballyと呼んでた。