クエリーにboolean値を割り当にラムダ計算

Question

このラムダ計算の表現は、オペレーター:

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

誰でもできるので助けてくれを理解する表記?

Answer 1

「その後、他のC Bが」

はラムダ計算にブール値を表現する方法を理解するために、それは、IF式を考えるのに役立ちます。それが偽である場合、これは、それが本当であれば、最初の分岐、Bを選択表現、そして第二に、Cです。ラムダ式は非常に簡単に行うことができます：

lambda(x).lambda(y).x

あなた自身の最初の引数を与え、かつます。

lambda(x).lambda(y).y

あなたに第二を与えます。だから、それらの式のいずれかである場合は、

a b c

我々はIFがやりたいだけで何である、のいずれかbまたはcを与えます。だから、定義

 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とm両方がnであり、そうでなければtrueする場合bこの発現評価します。 aはあなたの関数とbの第一引数が第二であり、そしてtrueは2つの引数の最初を与える関数として定義されているのでmとnは両方trueであれば、その後、その式全体です。それ以外の場合はfalseです。そして、それはandの単なる定義です！

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

Answer 2

のラムダ計算には、Booleanに代表されると二つの引数、成功と失敗。の引数と呼ばれる continuations, でも、残りの計算のboolean Trueの成功に続き、Boolean Falseの場合電話の故障続など。この符号化するという教会のエンコーディング、という考え方ですBooleanはい"の場合、その他の機能"を搭載しました。

と言えるでしょう

true  = \s.\f.s
false = \s.\f.f

場所 s いて成功 f 立不全のバックスラッシュはASCII lambda.

今私の指導が受けられます。どうしてコード and?でも、Cまで

n && m = n ? m : false

これだけでは、

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f

しかし、三元系を構築し、コードのラムダ計算をかけることができ機能を適用しておりますので

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f

と、いうまに到着

&& = \n . \m . \s . \f . n (m s f) f

お名前の変更の成功と失敗continuationsる a や b 戻しているオリジナル

&& = \n . \m . \a . \b . n (m a b) b

他の計算にはラムダ計算、使用時の教会のエンコーディング, あることがよくありますの作業においては、代数法 と等式推論に変換すlambdasします。

Answer 3

実際にはもう少しだけAND演算子よりもです。それはif m and n then a else bのラムダ計算バージョンです。ここに説明があります：

ラムダ計算で

真は、関数*二つの引数を取り、最初のを返すように表されます。偽関数は*二つの引数を取り、二を返すように表されます。

あなたは上記の示した機能は、* 4つの引数を取ります。その様子から、MとNブール値とすることが、いくつかの他の値をbになっています。 mがtrueの場合、それはn a bある最初の引数に評価します。 nがあれば真であり、B nは偽である場合、これは順番にと評価されます。 mがfalseの場合、それは2番目の引数bに評価されます。

mおよびnの両方が、そうでなければ真とBであるのであれば、基本的機能を返す。

（*）「二つの引数を取る」手段「の引数を取り、別の引数を取る関数を返す」。

あなたのコメントに応じて編集します：

はwikiページ上で見られるようにand true falseは、このように動作します

は最初のステップは、その定義、すなわち(λm.λn. m n m) (λa.λb. a) (λa.λb. b)と各識別子を交換するだけです。今すぐ関数(λm.λn. m n m)が適用されます。 m n mにおけるmのすべての発生が最初の引数（(λa.λb. a)）およびnのすべての出現で置換されていることを、この手段は、第二引数（(λa.λb. b)）で置換されています。だから我々は(λa.λb. a) (λa.λb. b) (λa.λb. a)を取得します。今、私たちは、単に機能(λa.λb. a)を適用します。この関数の本体は、即ち、第1引数、(λa.λb. b)この評価さは、単純であるため、すなわちfalse（λx.λy. y手段のfalseなど）。