定義二元指數運算符CARAT.in lambda微積分CARAT

Question

我想在lambda微積分中定義二元指數運算符，例如運算符CARAT。例如，這個運算符可能帶有兩個參數，第2個lambda編碼和第4個lambda編碼，並計算第16個lambda編碼。我的答案並不對，但它花了我一天的時間這樣做。我使用教堂數字的定義。這是我的答案。如果我的回答錯誤，請諒解我。我不知道如何正確地做到這一點。如果有人知道，那麼請幫我找出簡短的答案。

繼任功能，接下來，它增加了一個，可以在零條款和下一定義自然數：

1 = (next 0)  
2 = (next 1) 
    = (next (next 0))  
3 = (next 2) 
    = (next (next (next 0))) 

從上面的結論，我們可以下一個定義的功能如下：

next = λ n. λ f. λ x.(f ((n f) x)) 
one = (next zero) 
    => (λ n. λ f. λ x.(f ((n f) x)) zero) 
    => λ f. λ x.(f ((zero f) x)) 
    => λ f. λ x.(f ((λ g. λ y.y f) x)) -----> (* alpha conversion avoids clash *) 
    => λ f. λ x.(f (λ y.y x)) 
    => λ f. λ x.(f x) 

因此，我們可以安全地證明......。

zero = λ f. λ x.x 
one = λ f. λ x.(f x) 
two = λ f. λ x.(f (f x)) 
three = λ f. λ x.(f (f (f x))) 
four = λ f. λ x.(f (f (f (f x)))) 
: 
: 
: 
Sixteen = λ f. λ x.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))) 

增加只是後繼的迭代。我們現在是在一個位置來定義另外在明年方面：

m next n => λx.(nextm x) n => nextm n => m+n 
add = λ m. λ n. λ f. λ x.((((m next) n) f) x) 
four = ((add two) two) 
    => ((λ m. λ n. λ f. λ x.((((m next) n) f) x) two) two) 
    => (λ n. λ f. λ x.((((two next) n) f) x)two) 
    => λ f. λ x.((((two next) two) f x) 
    => λ f. λ x.((((λ g. λ y.(g (g y)) next) two) f x) 
    => λ f. λ x.(((λ y.(next (next y)) two) f) x) 
    => λ f. λ x.(((next (next two)) f) x) 
    => λ f. λ x.(((next (λ n. λ f. λ x.(f ((n f) x)) two)) f) x) 

用於替代值後「下一步」，然後「二」，我們可以進一步降低上述形式

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

即四。

同樣，乘法是一個迭代的迭代。因此，乘法被定義爲如下：

mul = λ m. λ n. λ x.(m (add n) x) 
six = ((mul two) three) 
=> ((λ m. λ n. λ x.(m (add n) x) two) three) 
=> (λ n. λ x.(two (add n) x) three) 
=> λ x.(two (add three) x 
=> (λf. λx.(f(fx)) add three) 
=>(λx.(add(add x)) three) 
=> (add(add 3)) 
=> (λ m. λ n. λ f. λ x.((((m next) n) f) x)add three) 
=> (λ n. λ f. λ x.(((three next)n)f)x)add) 
=> (λ f. λ x.((three next)add)f)x) 

用於替代值後「三」，「下」，並且隨後的「添加」，然後再次對「下一步」，上面的形式將減少

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

ie六。

最後，求冪可以通過迭代乘法被定義

假設冪函數的調用CARAT

CARAT = λm.λn.(m (mul n)) 
sixteen => ((CARAT four) two) 
=> (λ m. λ n.(m (mul n) four) two) 
=> (λ n.(two (mul n)four 
=> (two (mul four)) 
=> ((λ f. λ x.(f (f x))))mul)four) 
=> (λ x. (mul(mul x))four) 
=> (mul(mul four)))) 
=> (((((λ m. λ n. λ x.(m (add n) x)mul)four) 
=> ((((λ n. λ x.(mul(add n) x)four) 
=> (λ x.(mul(add four) x)) 
=> (λ x (λ m. λ n. λ x.(m (add n) x add)four) x 
=> (λ x (λ n. λ x. (add(add n) x)four)x 
=> (λ x (λ x (add (add four) x) x) 
=> (λ x (λ x (λ m. λ n. λ f. λ x((((m next) n) f) x)add)four) x) x) 
=> (λ x (λ x (λ n. λ f. λ x(((add next)n)f)x)four)x)x) 
=> (λ x (λ x (λ f. λ x((add next)four)f)x)x)x) 
=> (λ x (λ x (λ f. λ x((λ m. λ n. λ f. λ x((((m next) n) f) x)next)four)f)x)x)x) 
=> (λ x (λ x (λ f. λ x((λ n. λ f. λ x.(((next next)n)f)x)four)f)x)x)x) 
=> (λ x (λ x (λ f. λ x((λ f. λ x ((next next)four)f)x)f)x)x)x) 
=> (λ x (λ x (λ f. λ x((λ f. λ x(((λ n. λ f. λ x.(f ((n f) x))next)four)f)x)f)x)x)x) 

現在，減少上述表達式和替換爲「下一個」和「4」，並進一步降低，我們得到以下表格

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

即十六。

Answer 1

首先，重新寫​​作爲

next = λ num. λ succ. λ zero. succ (num succ zero) 

在拉姆達演算括號只是用於分組;通過並置術語來表示申請，即僅通過將一個術語相鄰並且與左邊相關聯。

我們如何閱讀以上內容？這是一個lambda術語。當它應用於其他lambda術語時，如NUM，它將減少到lambda術語λ succ. λ zero. succ (NUM succ zero)。這將是直接結果，表示由NUM表示的給定號碼的下一個號碼。我們可以讀它對我們說，「我不知道如何計算後繼者，或者它是什麼意思是零，但如果兩者都提供給我，我會根據他們產生一些結果，並且根據用於創建我的lambda項NUM，將這些計算方法提供給NUM，然後再將其結果應用於後續函數，如給我的「」。

這當然假設NUM尊重相同的假設，並以一致的方式運行。特別是，ZERO，當應用於s和z，必須返回z：

ZERO = λ s. λ z. z ; == λ a. λ b. b == ... 

其他的一切，從這個如下。