functional-programming - ラムダ計算でのブール値のクエリ

Question

これは、AND 演算子のラムダ計算表現です。

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b

この表現を理解するのを手伝ってくれる人はいますか?

Answer 1

ラムダ計算でブール値を表す方法を理解するには、「if a then b else c」という IF 式について考えると役立ちます。これは、最初の分岐 b が true の場合に選択し、2 番目の分岐 c が false の場合に選択する式です。ラムダ式はそれを非常に簡単に行うことができます:

lambda(x).lambda(y).x

その引数の最初のものをあなたに与えるでしょう、そして

lambda(x).lambda(y).y

あなたに2番目を与えます。したがって、a がこれらの式の 1 つである場合、

a b c

または のいずれbかcを返します。これは、IF に実行させたいことです。だから定義する

 true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y

のa b cように動作しますif a then b else c。

式の中を見ると(n a b)、それは を意味しif n then a else bます。次にm (n a b) b、

if m then (if n then a else b) else b

この式は、 と の両方aが である場合に評価され、そうでない場合に評価されます。は関数の最初の引数であり、は 2 番目の引数であり、2 つの引数の最初の引数を与える関数として定義されているため、 ifとare bothであるため、式全体も同様です。それ以外の場合はです。そして、それは!の定義です。mntruebabtruemntruefalseand

これはすべて、ラムダ計算を発明したアロンゾ・チャーチによって発明されました。

Answer 2

実際、これは単なる AND 演算子ではありません。のラムダ計算のバージョンですif m and n then a else b。説明は次のとおりです。

ラムダ計算では、true は 2 つの引数* を取り、最初の引数を返す関数として表されます。False は、2 つの引数* を取り、2 番目の引数を返す関数として表されます。

上記の関数は 4 つの引数を取ります*。見た目から、m と n はブール値で、a と b は他の値であると想定されます。m が true の場合、最初の引数である に評価されますn a b。これは、n が true の場合は a に評価され、n が false の場合は b に評価されます。m が false の場合、2 番目の引数 b に評価されます。

したがって、基本的に、関数は m と n の両方が true の場合は a を返し、そうでない場合は b を返します。

(*) ここで、「引数を 2 つ取る」とは、「引数を取り、別の引数を取る関数を返す」ことを意味します。

コメントに応じて編集します。

and true falsewikiページに見られるように、次のように機能します。

最初のステップは、各識別子をその定義に置き換えるだけ(λm.λn. m n m) (λa.λb. a) (λa.λb. b)です。これで関数(λm.λn. m n m)が適用されます。これは、 m inm n mが出現するたびに最初の引数 ( (λa.λb. a)) に置き換えられ、 n が出現するたびに 2 番目の引数 ( (λa.λb. b)) に置き換えられることを意味します。だから私たちは得(λa.λb. a) (λa.λb. b) (λa.λb. a)ます。次に、関数 を適用するだけです(λa.λb. a)。この関数の本体は単に a 、つまり最初の引数であるため、 this は に評価(λa.λb. b)さfalseれλx.λy. yますfalse。