自然数の教会数字コード化は不必要に複雑ですか？

Question

構造と解釈コンピュータプログラムの私が読んでいる本はゼロを定義することによって、教会の数字を提示し、インクリメント機能

zero: λf. λx. x 
increment: λf. λx. f ((n f) x) 

これは私にはかなり複雑なようで、それが数字に私には本当に長い時間がかかりましたそれを取り出して1つ（λf.λx. f x）と2つ（λf.λx. f (f x)）を得ます。

空のラムダがゼロで、このように数字をこのようにエンコードするのはずっと簡単ではないでしょうか？

zero: λ 
increment: λf. λ. f 

は、今では1（λ. λ）および2（λ. λ. λ）などを導き出すために些細です。

これは、ラムダで数値を表現する方がはるかに直感的で直感的な方法のようです。このアプローチにはいくつかの問題があり、教会の数字が彼らのやり方で働く理由がありますか？このアプローチはすでに証明されていますか？

Answer 1

あなたのエンコーディング（ゼロ：λx.x、1：λx.λx.x、2：λx.λx.λx.x、など）は、それが簡単にインクリメントとデクリメントを定義することが、それを超えて、それはあなたのエンコーディングのためのコンビネータを開発するためにかなりトリッキーになります。たとえば、isZeroをどのように定義しますか？

チャーチのコード化について考えてみると直感的には、nの数字はn回の繰り返しで表されます。これにより、番号に符号化された繰り返しを使用するだけで、plusのようなコンビネータを簡単に開発できます。再帰のための派手なコンビネータの必要はありません。

教会のエンコーディングでは、各数字は同じインターフェースを持ちます.2つの引数をとります。あなたのエンコーディングでは、各数字は引数の数によって定義されます。これは、一様に動作するのは本当に面倒です。

数字をエンコードする別の方法は、数値をn = 0と考えることです。 S n、およびバニラエンコーディングを使用してユニオンを作成します。

Answer 2

数字の提案構文はラムダ計算では有効ではありませんが、教会数字は実際にラムダ計算の有効な構造です。それで、教会の数字が彼らのやり方である理由の可能性があります。数字の符号化は、ラムダ計算（例えば、インクリメント）で定義されたさらなる操作が、符号化された数字に対しても動作することを許可する方法で、ラムダ計算 'definition 。