不動点
不動点(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と呼んでた。