ベキッチの定理

計算可能性理論において、ベキッチの定理またはベキッチの補題は、相互再帰を一度に 1 つの変数に関する再帰に分割することを可能にする不動点に関する定理です。 ^{[ 1 ] [ 2 ] [ 3 ]}これは、オーストリアのハンス・ベキッチ (1936-1982) によって 1969 年に作成され、^{[ 4 ]} 1984 年にクリフ・ジョーンズの著書で死後に出版されました。^{[ 5 ]}

定理は次のように定式化される。^{[ 1 ] [ 4 ]} 2つの演算子を考える${\displaystyle f:P\times Q\to P}$そして${\displaystyle g:P\times Q\to Q}$有向完全半順序について${\displaystyle P}$そして${\displaystyle Q}$各成分において連続である。次に演算子を定義する。${\displaystyle (f,g)(x,y)=(f(x,y),g(x,y))}$これは積の順序（成分ごとの順序）に関して単調です。クリーネの不動点定理により、最小不動点を持ちます。${\displaystyle \mu (x,y).(f,g)(x,y)}$ペア${\displaystyle (x_{0},y_{0})}$で${\displaystyle P\times Q}$そのため${\displaystyle f(x_{0},y_{0})=x_{0}}$そして${\displaystyle g(x_{0},y_{0})=y_{0}}$。

ベキッチの定理（彼のノートでは「二分補題」と呼ばれている）^{[ 4 ]}は、同時最小固定点が${\displaystyle \mu (x,y).(f,g)(x,y)}$最小固定点の系列に分割できる${\displaystyle P}$そして${\displaystyle Q}$特に、固定点は${\displaystyle (x_{0},y_{0})}$次のように：

$${\displaystyle {\begin{aligned}x_{0}&=\mu xf(x,\mu yg(x,y))\\y_{0}&=\mu yg(x_{0},y)\end{aligned}}}$$

このプレゼンテーションでは${\displaystyle y_{0}}$は、${\displaystyle x_{0}}$代わりに、対称的な表現で定義することもできます。^{[ 1 ] [ 6 ] [ 7 ]}

$${\displaystyle {\begin{aligned}x_{0}&=\mu x.f(x,\mu y.g(x,y))\\y_{0}&=\mu y.g(\mu x.f(x,y),y)\end{aligned}}}$$

証明（ベキッチ）：^{[ 4 ]}

取${\displaystyle y_{0}=\mu y.g(x_{0},y)}$明らかに、${\displaystyle y_{0}=g(x_{0},y_{0})}$以来${\displaystyle y_{0}}$は不動点である。同様に、${\displaystyle x_{0}=\mu x.f(x,\mu y.g(x,y))}$、 我々は持っています${\displaystyle x_{0}=f(x_{0},\mu y.g(x_{0},y))=f(x_{0},y_{0})}$したがって${\displaystyle (x_{0},y_{0})}$は固定点である${\displaystyle (f,g)}$。

さらに、あらかじめ定められた点がある場合${\displaystyle (x_{1},y_{1})}$と${\displaystyle (x_{1},y_{1})\geq (f(x_{1},y_{1}),g(x_{1},y_{1}))}$、 それから${\displaystyle x_{1}\geq f(x_{1},\mu y.g(x_{1},y))\geq x_{0}}$そして${\displaystyle y_{1}\geq \mu y.g(x_{1},y)\geq \mu y.g(x_{0},y)=y_{0}}$;したがって${\displaystyle (x_{1},y_{1})\geq (x_{0},y_{0})}$そして結論として${\displaystyle (x_{0},y_{0})}$は最小の不動点である。

ベキッチの定理を繰り返し適用することで、タプルの最小不動点を単一変数の最小不動点の観点から求めることができます。結果として得られる式はかなり複雑になるかもしれませんが、自動定理証明器を設計する際には、単一変数の不動点について推論する方が容易になる場合があります。^{[ 9 ]}