B,Cコンビネータ

ウィキペディア小見出し辞書

B,Cコンビネータ

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/09/10 14:50 UTC 版)

「コンビネータ論理」の記事における「B,Cコンビネータ」の解説

SとKに加え、モイセイ・シェインフィンケリ（ロシア語版、英語版）の論文ではBとCと呼ばれる、以下のような簡約をするコンビネータを含めた。 (C f x y) = (f y x) (B f g x) = (f (g x)) 彼は、どのようにしてSとKだけを用いてこれらを表現できるかを説明した。これらのコンビネータは述語論理やラムダ計算をコンビネータ式にする際に非常に有用である。これらはハスケル・カリーと、だいぶ後に計算機における用法と関連付けたデビッド・ターナーによって使われた。これらを使って、以下のように変換のルールを拡張できる。 T[x] => x T[(E₁ E₂)] => (T[E₁] T[E₂]) T[λx.E] => (K T[E]) (if x is not free in E) T[λx.x] => I T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E) T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂]) (if x is free in both E₁ and E₂) T[λx.(E₁ E₂)] => (C T[λx.E₁] T[E₂]) (if x is free in E₁ but not E₂) T[λx.(E₁ E₂)] => (B T[E₁] T[λx.E₂]) (if x is free in E₂ but not E₁) BとCコンビネータを使うと、λx.λy.(y x)の変換はこのようになる。 T[λx.λy.(y x)] = T[λx.T[λy.(y x)]] = T[λx.(C T[λy.y] x)] (by rule 7) = T[λx.(C I x)] = (C I) (η-reduction) = C*(traditional canonical notation : X* = X I) = I'(traditional canonical notation: X' = C X) 確かに、(C I x y)は(y x)に簡約される。 (C I x y) = (I y x) = (y x) その動機は、BとCは限定されたSであるということである。Sは値を取り両方のアプリカンドを置き換えて適用を行う一方。Cはアプリカンドのみ、Bは引数のみを置き換える。そのコンビネータのための近代的な名前は、ハスケル・カリーの1930年の博士論文による(B,C,K,Wシステムを参照)。モイセイ・シェインフィンケリ（ロシア語版、英語版）のもとの論文では、今S, K, I, B,Cと呼んでいるものはそれぞれS, C, I, Z, Tと呼ばれていた。新しい変換の規則によるコンビネータのサイズの短縮はBとCを用いなくても、この論文の節3.2のように達成できる。