ラムダ計算との関係
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2022/06/17 15:40 UTC 版)
「SKIコンビネータ計算」の記事における「ラムダ計算との関係」の解説
任意のコンビネータ項に対して、それと外延的に等価かつ同じ自由変数を持つラムダ項が存在する。これは、コンビネータ項に現れるすべての定数記号を、 S = λxyz.xz(yz) K = λxy.x I = λx.x と置き換えれば良いから明らかである。一方任意のラムダ項に対して、それと外延的に等価かつ同じ自由変数を持つコンビネータ項が存在する。これは、命題論理におけるヒルベルトスタイルと自然演繹スタイルの証明系が等価であることと対応する(演繹定理)。
※この「ラムダ計算との関係」の解説は、「SKIコンビネータ計算」の解説の一部です。
「ラムダ計算との関係」を含む「SKIコンビネータ計算」の記事については、「SKIコンビネータ計算」の概要を参照ください。
- ラムダ計算との関係のページへのリンク