ラムダ計算と教会数の基本を理解しようとしています。私は多くの読書と練習を行ってきましたが、いくつかの機能がどのように機能するかを確認しようとすることに行き詰まっているようです.
私が立ち往生している例は次のとおりです。おそらく、誰かが私が間違っている場所を説明できるでしょう。
1 の教会数は、次のように表すことができます。
λf. λx. f x
教会数 (m n )のべき乗関数は、次のように指定できます。
λm. λn. n m
私がやりたいのは、1 と 1 に累乗関数を適用すると、1 1 = 1 であるため、1 が返されることを示すことだけです。これを行っているので、これらの関数がどのように機能するかをよりよく理解できます。私の作業は次のとおりで、毎回行き詰まります：
// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)
そして、私は立ち往生しています。私は両方fの を失い、 だけが残り、x1 つも戻っていません。どこが間違っていますか？