Lambda微積分前驅函數減少步驟

Question

我在lambda微積分中遇到了前驅函數的Wikipedia描述。

維基說什麼是以下幾點：

PRED：=λnfx.n（λgh.h（GF））（λu.x）（λu.u）

有人能解釋還原工藝步驟 - 一步？

謝謝。

Answer 1

好吧，所以教會數字的想法是使用函數來編碼「數據」，對吧？工作的方式是通過一些通用操作來表示一個值，然後用它來執行。因此，我們也可以朝着另一個方向前進，這有時可以使事情更清楚。

教會數字是自然數的一元表示。所以，讓我們用Z表示零，Sn表示n的後繼。現在我們可以這樣計算：Z,SZ,SSZ,SSSZ ...等價的教會數字有兩個參數 - 第一個對應於S，第二個到Z - 然後使用它們來構建上述模式。因此，給定的參數f和x，我們可以算這樣的：x，f x，f (f x)，f (f (f x)) ......

讓我們來看看什麼PRED一樣。

首先，它創建一個lambda服用三arguments-- n是教會的數字，當然我們希望它的前身，這意味着f和x是參數所得到的數字，這從而意味着該機構lambda將會被f應用於x一次少於n會。

接下來，它適用於n到三個的論點。這是棘手的部分。

第二個參數與之前的Z相對應的是λu.x - 一個常數函數，忽略一個參數並返回x。

的第一個參數，即從對應於S更早，是λgh.h (g f)。我們可以將其重寫爲λg. (λh.h (g f))，以反映僅應用最外面的lambda的事實n次。該函數所做的是將累積結果作爲g，並返回一個帶有一個參數的新函數，該函數將該參數應用於應用於f的g。當然，這絕對是莫名其妙的。

那麼......這裏發生了什麼？考慮直接替換S和Z。在非零數字Sn中，n對應於綁定到g的參數。所以，記住f和x在外部範圍的約束，我們可以算這樣的：λu.x，λh. h ((λu.x) f)，λh'. h' ((λh. h ((λu.x) f)) f) ...表演明顯減少，我們得到這樣的：λu.x，λh. h x，λh'. h' (f x) ...這裏的模式是一個函數正在向內傳遞一層，此時S將應用它，而Z將忽略它。所以我們得到f的一個應用程序，每個S除了最外面的。

第三個參數被簡單地恆等函數，這是忠實地由最外層S施加，返回最終result-- f施加更少的一個倍的S層n對應的數字。

Answer 2

麥肯的回答很好地解釋了這一點。讓我們舉一個Pred 3 = 2的具體例子：

考慮表達式：n（λgh.h（g f））（λu.x）。令K =（λgh.h（gf））

對於n = 0，我們編碼0 = λfx.x，所以當我們應用β的縮小值爲(λfx.x)(λgh.h(gf))意味着(λgh.h(gf))被替換0次。經過進一步的測試，減少我們得到：

λfx.(λu.x)(λu.u)

降低到

λfx.x

其中λfx.x = 0，符合市場預期。

對於n = 1，我們應用K中1次：

(λgh.h (g f)) (λu.x) => λh. h((λu.x) f) => λh. h x

對於n = 2，我們應用K中2次：

(λgh.h (g f)) (λh. h x) => λh. h ((λh. h x) f) => λh. h (f x)

對於n = 3 ，我們申請K 3次：

(λgh.h (g f)) (λh. h (f x)) => λh.h ((λh. h (f x)) f) => λh.h (f (f x))

最後，我們把這個結果和應用的ID功能的話，我們得到了

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

這是數的定義2.

列表基於實現可能比較容易理解，但它需要很多中間步驟。所以它不如教會最初實施IMO那麼好。

Answer 3

你可以嘗試理解前繼函數的這個定義（不是我最喜歡的）的延續。

爲了簡化此事一點，讓我們看看下面的變型

PRED := λn.n (λgh.h (g S)) (λu.0) (λu.u) 

然後，你可以使用f代替S，和0隨x。

函數的主體通過參數N迭代n次變換M.參數N是type（nat - > nat） - > nat的函數，它需要nat的延續並返回nat。最初，N =λu.0，即它忽略了延續並剛剛返回0。我們稱N爲當前計算。函數M：（nat - > nat） - > nat） - >（nat - > nat） - > nat如下修改計算g：（nat - > nat） - > nat。 它發生在輸入的延續小時，它適用於繼續與S.

由於初始計算忽略延續當前計算克的 結果，M的一個應用程序之後，我們得到的計算（λh.h 0），然後（λh.h（S 0）），依此類推。

最後，我們將計算應用於身份延續 以提取結果。

Answer 4

閱讀以前的答案（好的）後，我想給我自己的願景，希望它有助於某人（更正歡迎）。我將用一個例子。

首先，我想在定義中添加一些括號，以便讓我的一切更加清晰。讓我們redifine給定的公式：

PRED := λn λf λx.(n (λgλh.h (g f)) (λu.x)) (λu.u) 

我們還定義了三個教會的數字，這將有助於與例如：

Zero := λfλx.x 
One := λfλx. f (Zero f x) 
Two := λfλx. f (One f x) 
Three := λfλx. f (Two f x) 

爲了理解它是如何工作的，我們首先關注的這一部分公式：

n (λgλh.h (g f)) (λu.x) 

從這裏，我們可以提取這個結論： n是教會的數字，要應用的功能λgλh.h (g f)和起動數據λu.x

考慮到這一點，讓我們嘗試一個例子：

PRED Three := λf λx.(Three (λgλh.h (g f)) (λu.x)) (λu.u) 

讓我們首先着眼於數字的減少（我們之前解釋的部分）：

Three (λgλh.h (g f)) (λu.x) 

從而降低到：

(λgλh.h (g f)) (Two (λgλh.h (g f)) (λu.x)) 
(λgλh.h (g f)) ((λgλh.h (g f)) (One (λgλh.h (g f)) (λu.x))) 
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (Zero (λgλh.h (g f)) (λu.x)))) 
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) ((λfλx.x) (λgλh.h (g f)) (λu.x)))) -- Here we lose one application of f 
(λgλh.h (g f)) ((λgλh.h (g f)) ((λgλh.h (g f)) (λu.x))) 
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h ((λu.x) f))) 
(λgλh.h (g f)) ((λgλh.h (g f)) (λh.h x)) 
(λgλh.h (g f)) (λh.h ((λh.h x) f)) 
(λgλh.h (g f)) (λh.h (f x)) 
(λh.h ((λh.h (f x) f))) 

結束了機智H：

λh.h f (f x) 

因此，我們有：

PRED Three := λf λx.(λh.h (f (f x))) (λu.u) 

再次降低：

PRED Three := λf λx.((λu.u) (f (f x))) 
PRED Three := λf λx.f (f x) 

正如你可以在削減看到，我們最終將函數一次少拜一個聰明的使用函數的方法。

使用ADD1爲f和0作爲x，我們得到：

PRED Three add1 0 := add1 (add1 0) = 2 

希望這有助於。