私は本から、Church Numerals の後継者は (\lambda nf x. f (nfx) ) の形式であることを読みました。
昨夜、私はこれを思いついた: (\lambda ab c. (ab) (bc) )
後継機能としての機能も果たしていると思います。ただし、削減が正しいと 100% 確信しているわけではありません。誰か調べて教えてくれませんか？
以下は私の要約です: 教会の数字を (\lambda f x. f^nx) とします。ここで、f^nx は実際には (f(f(f(f...(x)))) の短縮バージョンです。これは数値 n を表します。期待される結果は n+1、つまり (\lambda f x. f^{n+1} x) になるはずです。
(\lambda ab c. (ab) (bc) )(\lambda f x. f^nx)
= (\lambda b c. ( (\lambda f x. f^nx) b) (bc) ) // a 置換
= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // f を置換
= (\lambda b c. ( (\lambda x. b^nx) (bc) ) // 100% 確実ではありません。x を (bc) に置き換えることはできますか?
= (\lambda b c. ( b^n (bc) )
= (\lambda b c. ( b^(n+1) c )
特にステップ 3 から 4 へのこの削減は正しいですか? ありがとう！