ラムダの計算と教会の数字の混乱

Question

私はラムダ計算と教会の数字の基礎を理解しようとしています。私は多くの読書と練習をしてきましたが、私はいくつかの機能がどのように機能するか見てみようとしていました。

私が執着している例は次のとおりです。おそらく誰かが私が間違っている場所を説明することができます。

1教会数字として表すことができる。

λm. λn. n m 

私がしたいすべての：教会数字（M ^N）に指数関数として与えることができる

λf. λx. f x 

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の両方を失ってしまった、xと一緒に残っていて、私は1つも戻っていない。どこが間違っていますか？

Answer 1

どこが間違っていますか？

Nowhere！あなたは終わった。変数名は重要ではないことを覚えておいてください。それは重要な構造です。 fまたはx2の名前は意味がありません。どのように使用されるかだけが重要です。 1のための教会の数字は

λf. λx. f x 

であり、あなたがx出来上がりにfからx2とx1の名前を変更し

λx2. (λx1. x2 x1) 

を持っています！あなたは

λf. (λx. f x) 
= λf. λx. f x