質疑布爾在演算

Question

這是與運算的演算表示：

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b 

誰能幫助我理解這種表示？

Answer 1

要理解如何在lambda演算中表示布爾值，可以考慮IF表達式，「if a then b else c」。這是一個表達式，選擇第一個分支，b，如果它是真的，第二個，c，如果它是假的。 Lambda表達式可以做到這一點很容易：

lambda(x).lambda(y).x 

會給你第一個它的參數，並

lambda(x).lambda(y).y 

給你第二次。因此，如果是那些表現之一，那麼

a b c 

給出任何b或c，這正是我們想要的如果要做。所以定義

true = lambda(x).lambda(y).x 
false = lambda(x).lambda(y).y 

和a b c會像if a then b else c。

在(n a b)的內部查看錶達式，表示if n then a else b。 然後m (n a b) b裝置

if m then (if n then a else b) else b 

該表達式評估爲a如果兩個m和n是true，以及b否則。由於a是函數的第一個參數，b是第二個參數，true已被定義爲一個函數，它給出了兩個參數中的第一個參數，因此如果m和n都是true，那麼整個表達式也是如此。否則它是false。這就是and的定義！

所有這些都是由Alonzo Church發明的，他發明了lambda演算。

Answer 2

實際上它不僅僅是AND運算符。這是if m and n then a else b的lambda微積分版本。下面是解釋：

在lambda微積分中，true表示爲一個帶兩個參數*並返回第一個參數的函數。 False表示爲帶有兩個參數*並返回第二個參數的函數。

上面顯示的函數需要四個參數*。從它看起來，m和n應該是布爾值，a和b是其他值。如果m爲真，則它將評估爲其第一個參數，即n a b。如果n爲真，則這反過來將評估爲a，如果n爲假，則b爲b。如果m爲假，它將評估爲第二個參數b。

所以基本上，如果m和n都爲真，則函數返回a，否則返回b。 （*）其中「取兩個參數」的意思是「採用一個參數並返回一個採用另一個參數的函數」。

編輯迴應您的評論：

and true false所看到的wiki頁面是這樣的：

的第一步是簡單地用其定義來替代每個標識符，即(λm.λn. m n m) (λa.λb. a) (λa.λb. b)。現在應用功能(λm.λn. m n m)。這意味着m n m中每個出現的m被替換爲第一個參數（(λa.λb. a)），並且每個出現的n被替換爲第二個參數（(λa.λb. b)）。所以我們得到(λa.λb. a) (λa.λb. b) (λa.λb. a)。現在我們只需應用功能(λa.λb. a)。由於該函數的主體是簡單的a，即第一個參數，因此它評估爲(λa.λb. b)，即false（因爲λx.λy. y意味着false）。

Answer 3

在lambda演算中，一個布爾函數表示一個函數，該函數接受兩個參數，一個用於成功，一個用於失敗。這些參數被稱爲延續，因爲它們繼續進行其餘的計算;布爾值True調用成功延續，布爾型False調用失敗延續。這種編碼稱爲教會編碼，其思想是布爾非常像「if-then-else」函數。

所以我們可以說

true = \s.\f.s 
false = \s.\f.f 

其中s代表成功，f代表失敗，反斜槓是一個ASCII拉姆達。

現在，我希望你能看到這是怎麼回事。我們如何編碼and？那麼，在C，我們可以把它擴大到

n && m = n ? m : false 

只有這些功能，所以

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f 

，但三元結構，在演算編碼時，僅僅是功能應用，所以我們有

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f 

所以最後我們得出

&& = \n . \m . \s . \f . n (m s f) f 

如果我們重命名成功和失敗延續到a和b我們返回到原來的

&& = \n . \m . \a . \b . n (m a b) b 

與在演算其他計算，尤其是在使用邱奇數時，它往往容易解決事情用代數律和等式推理，最後轉換爲lambda表達式。