lambda - 教会数字:ラムダ計算でゼロをエンコードする方法は?

Question

ラムダ計算を学んでいますが、数値 0 のエンコーディングを理解できないようです。

「関数と2番目の値を取り、引数に関数をゼロ回適用する関数」はどのようにゼロですか? ゼロをエンコードする他の方法はありますか? ここで誰かが0をエンコードするのを手伝ってくれますか?

Answer 1

A "function that takes in a function and a second value and applies the function zero times on the argument" is, of course, not zero. It's an encoding of zero. When you deal with plain lambda calculus, you have to encode numbers (as well as other primitive types) in some way, and there are a few requirements dictated for each of these types. For example, one requirement for natural numbers is to be able to add 1 to a given number, and another is to be able to distinguish zero from bigger numbers (if you want to know more, look for "Peano Arithmetic"). The popular encoding that Dario quoted gives you these two things, and it is also representing an integer N by a function that does something (encoded as the f argument) N times -- which is a kind of a natural way to use naturals.

There are other encodings that are possible -- for example, once you can represent lists, you can represent N as a list of N items. These encodings have their pros and cons, but the one above is by far the most popular one.

Answer 2

ウィキペディアを参照してください：

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

ラムダ計算を学べば、λxy.y arg1 *arg2* がarg2に還元されることをおそらくすでに知っているでしょう。なぜなら、x は何も置き換えられず、残り (λy.y) が恒等関数だからです。

他の多くの方法でゼロを書くことができます (つまり、別の慣例を考え出す) が、λxy.y を使用する正当な理由があります。たとえば、0 を最初の自然数にしたい場合、後継関数を適用すると 1、2、3 などになります。関数 λabc.b(abc) を使用すると、λxy.x(y )、λxy.x(x(y))、λxy.x(x(x(y))) など、言い換えれば、整数システムを取得します。

さらに、加算に関してゼロを中立要素にする必要があります。後継関数 S := λabc.b(abc) を使用すると、 n +*m* をn S mとして定義できます。つまり、mへの後継関数の適用のn倍です。ゼロ λxy.y はこれを満たし、0 S mとm S 0 の両方がmに還元されます。