使用Haskell在lambda微積分中減少Beta測試

Question

我已經定義了以下函數用於beta測試，但我不確定如何考慮自由變量受限的情況。

data Term = Variable Char | Lambda Char Term | Pair Term Term deriving (Show,Eq) 
--substition 
s[M:x]= if (s=x) then M else s 
AB[M:x]= (A[M:x] B [x:M]) 
Lambda x B[M:x] = Lambda x B 
Lambda y P[M:x]= if x=y then Lambda y P else Lambda y P (M:x) 



--beta reduction 
Reduce [s]= s 
Reduce[Lambda x B]M = B[M:x] 
Reduce[L1 L2] = (Reduce [L1] Reduce [L2]) 

Answer 1

鏈接哈馬爾給在評論詳細介紹了該解決方案。

我只是想提供一個不同的解決方案。荷蘭數學家Nicolaas Govert de Bruijn發明了一種alternative notation for lambda terms。這個想法是，我們使用數字而不是使用變量的符號。我們用代表我們需要跨越多少個lambda表達式的數字替換每個變量，直到找到綁定變量的抽象。抽象然後不需要任何信息。例如：

λx. λy. x 

轉換爲

λ λ 2 

或

λx. λy. λz. (x z) (y z) 

轉換爲

λ λ λ 3 1 (2 1) 

這種表示法具有幾個顯着的優點。值得注意的是，由於沒有變量，所以沒有變量的重命名，也沒有α變換。雖然我們必須在更換時相應地重新編號，但我們不必檢查名稱衝突並進行任何重命名。上面的維基百科文章給出了一個β減數如何用這個記數法的例子。