S-K basisの完全性
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2021/09/10 14:50 UTC 版)
「コンビネータ論理」の記事における「S-K basisの完全性」の解説
SとKが外延的にすべてのラムダ項と同値なものに合成されうるのは、おそらく驚くべき事実である。したがって、チャーチのテーゼによれば、それはあらゆる計算可能な関数に合成されうる。その証明は、T[ ]という任意のラムダ項を同値なコンビネータにする変換を示すことで与えられる。T[ ]は以下のように定義する。 T[x] => x T[(E₁ E₂)] => (T[E₁] T[E₂]) T[λx.E] => (K T[E]) (if x does not occur free in E) T[λx.x] => I T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E) T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) これはabstraction eliminationとして知られている。
※この「S-K basisの完全性」の解説は、「コンビネータ論理」の解説の一部です。
「S-K basisの完全性」を含む「コンビネータ論理」の記事については、「コンビネータ論理」の概要を参照ください。
- S-K basisの完全性のページへのリンク