最小固定点

数学の一分野である順序論では、半順序集合(略して「poset」)からそれ自体への関数の最小不動点( lfpまたはLFP、最小不動点とも呼ばれる)は、poset の順序に従って、他の各不動点よりも小さい不動点です。関数は必ずしも最小不動点を持つ必要はありませんが、もし持つ場合は、最小不動点は一意です。

実数の通常の順序では、実関数f ( x ) =  x ²の最小の不動点はx = 0です (他の唯一の不動点は 1 で、0 < 1 であるため)。対照的に、f ( x ) =  x  + 1 には不動点がまったくないため、最小の 1 つはありません。また、f ( x ) =  xには無限個の不動点がありますが、最小の 1 つはありません。

を有向グラフ、を頂点とします。からアクセス可能な頂点の集合は、関数 の最小不動点として定義でき、次のように定義されます。 から共アクセス可能な頂点の集合は、同様の最小不動点によって定義されます。の強連結成分は、これら 2 つの最小不動点の 交点です。${\displaystyle G=(V,A)}$${\displaystyle v}$${\displaystyle v}$${\displaystyle f:\wp (V)\to \wp (V)}$${\displaystyle f(X)=\{v\}\cup \{x\in V:{\text{ for some }}w\in X{\text{ there is an arc from }}w{\text{ to }}x\}.}$${\displaystyle v}$${\displaystyle v}$

を文脈自由文法とします。空の文字列を生成する記号の集合は、 と定義される関数 の最小の不動点として取得できます。ここで、 は のべき集合を表します。 ${\displaystyle G=(V,\Sigma ,R,S_{0})}$${\displaystyle E}$ ${\displaystyle \varepsilon }$${\displaystyle f:\wp (V)\to \wp (V)}$${\displaystyle f(X)=\{S\in V:\;S\in X{\text{ or }}(S\to \varepsilon )\in R{\text{ or }}(S\to S^{1}\dots S^{n})\in R{\text{ and }}S^{i}\in X{\text{, for all }}i\}}$${\displaystyle \wp (V)}$${\displaystyle V}$

多くの不動点定理は、最小不動点を見つけるためのアルゴリズムを生み出します。最小不動点は、多くの場合、任意の不動点にはない望ましい特性を持っています。

コンピュータサイエンスにおける表示的意味論アプローチでは、最小不動点を使用して、特定のプログラムテキストから、その意味論と呼ばれる対応する数学関数を取得します。この目的のために、例外的な値「未定義」を表す人工的な数学的オブジェクト が導入されます。たとえば、プログラムデータ型 が与えられた場合、その数学的対応物は、それぞれ について を定義し、任意の 2 つの異なるメンバーをに関して比較できないようにすることで、 半順序集合にすると定義されます(図を参照)。 ${\displaystyle \bot }$int${\displaystyle \mathbb {Z} _{\bot }=\mathbb {Z} \cup \{\bot \};}$${\displaystyle \bot \sqsubset n}$${\displaystyle n\in \mathbb {Z} }$${\displaystyle n,m\in \mathbb {Z} }$${\displaystyle \sqsubset }$

プログラム定義のセマンティクスはint f(int n){...}、何らかの数学関数です。プログラム定義が何らかの入力 に対して終了しない場合、これは数学的に次のように表現できます。すべての数学関数の集合は、各 に対して関係が成り立つ場合、つまり がより定義されていないか に等しい場合、を定義することによって部分的に順序付けされます。たとえば、式 のセマンティクスは のセマンティクスよりも定義されていません。これは、前者は にマッピングされますが、後者はにマッピングされないためです。それ以外では、これらは一致します。 ${\displaystyle f:\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }.}$fn${\displaystyle f(n)=\bot .}$${\displaystyle f\sqsubseteq g}$${\displaystyle n,}$${\displaystyle f(n)\sqsubseteq g(n)}$${\displaystyle f(n)}$${\displaystyle g(n).}$x+x/xx+1${\displaystyle 0}$${\displaystyle \bot ,}$

あるプログラムテキストが与えられた場合f、その数学的対応物は、関数から関数への写像の最小不動点として得られ、これは「翻訳」によって得られるf。例えば、Cの定義

int fact ( int n ) { if ( n == 0 ) return 1 ; else return n * fact ( n -1 ); }               

マッピングに変換されます

${\displaystyle F:(\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot })\to (\mathbb {Z} _{\bot }\to \mathbb {Z} _{\bot }),}$定義${\displaystyle (F(f))(n)={\begin{cases}1&{\text{if }}n=0,\\n\cdot f(n-1)&{\text{if }}n\neq \bot {\text{ and }}n\neq 0,\\\bot &{\text{if }}n=\bot .\\\end{cases}}}$

写像は非再帰的に定義されるが、再帰的に定義される。例で満たされている特定の制約（クリーネの不動点定理を参照）の下では、必ず最小の不動点 、すなわちすべての に対してが存在する。^[1]で あることを示すことが可能である 。${\displaystyle F}$fact${\displaystyle F}$${\displaystyle \operatorname {fact} }$${\displaystyle (F(\operatorname {fact} ))(n)=\operatorname {fact} (n)}$${\displaystyle n\in \mathbb {Z} _{\bot }}$

${\displaystyle \operatorname {fact} (n)={\begin{cases}n!&{\text{if }}n\geq 0,\\\bot &{\text{if }}n<0{\text{ or }}n=\bot .\end{cases}}}$

のより大きな不動点は、例えば次のように定義される 関数である。${\displaystyle F}$${\displaystyle \operatorname {fact} _{0},}$

${\displaystyle \operatorname {fact} _{0}(n)={\begin{cases}n!&{\text{if }}n\geq 0,\\0&{\text{if }}n<0,\\\bot &{\text{if }}n=\bot ,\end{cases}}}$

ただし、この関数は、負の値の場合、上記のプログラム テキストの動作を正しく反映しません。つまり、呼び出しは終了せず、 を返すこともありません。数学的なプログラム セマンティクスとして合理的に使用できるのは 、最小の固定点だけです。${\displaystyle n;}$fact(-1)0${\displaystyle \operatorname {fact} ,}$

Immerman ^{[2] [3]} とVardi ^{[4] は} 独立に、線形順序構造の多項式時間計算可能特性がFO(LFP)、すなわち最小不動点演算子を持つ一階述語論理で定義可能であるという記述的複雑性の結果を示した。しかし、 FO(LFP) は、順序付けられていない構造のすべての多項式時間特性（例えば、構造が偶数サイズであるなど）を表現するには弱すぎる。

関数の最大不動点は、最小不動点と同様に、半集合の順序に従って他のどの不動点よりも大きい不動点として定義できます。コンピュータサイエンスでは、最大不動点は最小不動点よりもあまり一般的に使用されません。 具体的には、ドメイン理論で見つかる半集合には通常、最大元がないため、特定の関数に対して、相互に比較できない複数の最大不動点が存在する可能性があり、その関数の最大不動点は存在しない可能性があります。 この問題に対処するために、最適不動点は、他のすべての不動点と互換性のある最も定義された不動点として定義されています。 最適不動点は常に存在し、最大不動点が存在する場合は最大不動点です。 最適不動点により、最小不動点に収束しない再帰関数と共帰関数の正式な研究が可能になります。[ 5 ]^残念ながら、クリーネの再帰定理は、最小不動点が効果的に計算可能であることを示していますが、計算可能な関数の最適不動点は計算不可能な関数である可能性があります。^[6]

• クナスター・タルスキー定理
• 固定小数点ロジック

• イマーマン、ニール. 記述的複雑性、1999年、Springer-Verlag.
• Libkin, Leonid .有限モデル理論の要素、2004年、Springer。