私が読んでいるコンピュータープログラムの構造と解釈の本は、ゼロとインクリメント関数を定義することによって教会の数字を提示しています
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 つ( ) などを導出するのは簡単λ. λ. λです。
これは、ラムダで数値を表現するためのはるかに明白で直感的な方法のように思えます。このアプローチには何らかの問題があり、教会の数字がそのように機能する正当な理由がありますか? このアプローチはすでに証明されていますか?
エンコーディング ( zero: λx.x、 one: λx.λx.x、 two:λx.λx.λx.xなど) により、インクリメントとデクリメントを簡単に定義できますが、それを超えると、エンコーディング用のコンビネータを開発するのがかなり難しくなります。たとえば、どのように定義しますisZeroか?
教会の符号化について直感的に考える方法は、数字nが時間を繰り返す動作によって表されるということnです。これによりplus、数値にエンコードされた反復を使用するだけで、コンビネータを簡単に開発できます。再帰のための派手なコンビネータは必要ありません。
Church エンコーディングでは、各数値は同じインターフェイスを持ちます。2 つの引数を取ります。エンコーディングでは、各数値は引数の数によって定義されるため、均一に操作するのは非常に困難です。
数字をエンコードするもう 1 つの方法は、数字を n = 0 | S n であり、共用体にはバニラ エンコーディングを使用します。
数値の提案された構文はラムダ計算では有効ではありませんが、チャーチ数値はラムダ計算では実際に有効な構造です。これが、教会の数字がそのままである理由の 1 つです。数値エンコーディングは、ラムダ計算で定義されているさらなる操作 (たとえば、インクリメント) がエンコードされた数値を操作できるように、ラムダ計算の定義に準拠する必要があります。 .