克萊尼無定著理

佇咧數學中，序理論的Kleene 無法度定理指出予定任何完全格 _ L _ 佮任何具有斯科特連續性的函數

$ f : L \ to L , $

$ $ f $ 的上細袂振動 $ fix ( f ) $ 存在，阮若用 $ \ bot $ 來表示 _ L _ 內底的上小元素，遐爾 $ fix ( f )=\ bigsqcup _ { i \ geq 零 } f ^ { i } ( \ bot ) $ $

證明

咱首先定義集合 $ M=\ { \ bot , f ( \ bot ) , f ^ { 二 } ( \ bot ) , \ ldots \ } $，為著方便表示，阮用 $ m $ 來表示集合 $ M $ 中上大的元素，即 $ m=\ bigsqcup M $。阮想欲證明講 $ m $ 為函數 $ f $ 的上細袂振動。

起先咱證明 $ m $ 為函數 $ f $ 的不動點。因為函數 $ f $ 是斯科特連紲的，所以阮有 $ f ( m )=f ( \ sqcup M )=\ sqcup ( f ( M ) \ cup \ bot )=\ bigsqcup M=m $。

紲落來阮證明 $ m $ 為函數 $ f $ 的上細袂振動。準備函數 $ f $ 儉佇咧另外一个不動點 $ x $，因為乎 $ \ bot \ sqsubseteq x $ , 而且函數 $ f $ 為單調函數（因為斯科特連紲性）， 所以乎 $ f ( \ bot ) \ sqsubseteq f ( x )=x $。準講 $ m=f ^ { k } ( \ bot ) , k \ in \ mathbb { N } $，根據數學歸納法，$ f ^ { k } ( \ bot ) \ sqsubseteq f ^ { k } ( x )=x $。即 $ m $ 為函數 $ f $ 的上細袂振動。

參見

• 克納斯特-塔斯基定理
• 其他不動點定理