在Haskell中使用lambda演算进行Beta约简

Question

在Haskell中使用lambda演算进行Beta约简

6

我已经定义了以下的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])

- Sara Alaa Khodeir

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Petr · Accepted Answer

评论中提供的链接描述了解决方案的详细信息。

我想提供一个不同的解决方案。荷兰数学家尼古拉斯·戈弗特·德布鲁因发明了一种lambda项的替代符号表示法。其思想是，我们不使用变量符号，而是使用数字。我们将每个变量替换为表示需要跨越多少个lambda才能找到绑定该变量的抽象的数字。抽象本身不需要任何信息。例如：

λx. λy. x

被转换为

λ λ 2

或者

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

被转换为

λ λ λ 3 1 (2 1)

这种记号有几个显著的优点。特别是，由于没有变量，因此没有变量重命名，也没有α-转换。虽然我们在替换时必须相应地重新编号索引，但我们不需要检查名称冲突或进行任何重命名。上述维基百科文章给出了一个使用此记号进行β-约简的示例。