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发明了lambda 项的另一种表示法。这个想法是，我们不使用符号来表示变量，而是使用数字。我们将每个变量替换为表示需要跨越多少个 lambda 的数字，直到找到绑定该变量的抽象。抽象然后根本不需要任何信息。例如：

λx. λy. x

被转换为

λ λ 2

或者

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

被转换为

λ λ λ 3 1 (2 1)

这种表示法有几个相当大的优点。值得注意的是，由于没有变量，因此没有变量的重命名，也没有 α 转换。虽然我们在替换时必须相应地重新编号索引，但我们不必检查名称冲突并进行任何重命名。上面的 Wikipedia 文章给出了一个 β-reduction 如何使用这种表示法的示例。