haskell - 使用 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

评论中给出的链接hammar详细描述了解决方案。

我只是想提供一个不同的解决方案。 Nicolaas Govert de Bruijn ，一位荷兰数学家，发明了alternative notation for lambda terms 。我们的想法是，我们不使用符号来表示变量，而是使用数字。我们将每个变量替换为代表需要交叉的 lambda 数量的数字，直到找到绑定(bind)该变量的抽象。抽象根本不需要任何信息。例如:

λx. λy. x

转换为

λ λ 2

或

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

转换为

λ λ λ 3 1 (2 1)

这种表示法有几个显着的优点。值得注意的是，由于没有变量，因此没有变量重命名，也没有 α 转换。尽管我们在替换时必须相应地重新编号索引，但我们不必检查名称冲突并进行任何重命名。上述维基百科文章给出了如何使用此表示法进行 β 约简的示例。