Lambda微積分的減少

Question

我最近一直在研究lambda計算，我對減少和替換有很多疑問。什麼是α和β減少？何時和爲什麼他們使用？

如果有人能夠告訴任何有關lambda caculus中減少和替代的良好資源，那將是非常棒的。

Answer 1

Beta縮減只是lambda演算中用於計算的主要應用規則。它是通過替換應用，如圖所示：

如果你有拉姆達項：（\ XX） 和一定的參考價值，它右邊：Y

，那麼你會替代所有綁定變量的權（。）在你的lambda術語中。 綁定變量是匹配（。）左側變量的變量，因此在這種情況下x。

The reduction would be of the form: 
(\x.x)y //y gets bound to all occurences of x to the right of the period 
y 

其中y綁定到lambda表達式中x的所有出現處。這是身份識別功能。

Alpha「減少」通常稱爲阿爾法等價或阿爾法重寫規則。他們聲明，你可以在不改變表達式的含義的情況下更改任何lambda表達式的名稱及其綁定變量。

例如，使用上面的標識函數，我們可以輕鬆地將lambda項寫爲（\ j.j）。它不會改變我們的應用程序的結果如下所示：

(\j.j)y //y gets bound to all occurrences of j to the right of the period 
y 

至於學習資源：維基百科的頁面是非常詳細的，但符號重，可能會需要一些良好的重讀。

如果你只是在尋找更好的直覺來了解lambda微積分的工作原理，大多數計算機科學系都會有幻燈片放置。

您可能會發現這些有用的：http://www.classes.cs.uchicago.edu/archive/2002/winter/CS33600/slides/Lesson2.pdf https://www.utdallas.edu/~gupta/courses/apl/lambda.pdf