lambda-calculus - Lambda 演算自由变量问题

Question

我在网上找到了 Mike Gordon 的函数式编程 说明简介 ，我正在努力完成它。在第 9 页有这个问题：

Find an example to show that if V1 = V2 , then even if V2 is not free in E1,
it is not necessarily the case that:

(λ V1 V2 . E ) E1 E2 = E [E1/V1][E2/V2]

我猜我可以说因为 V1 和 V2 是相等的，我们可以这样重做：

(λ V2 V1 . E ) E1 E2

因此说

(λ V1 . E[E1/V2] ) E2

鉴于 E1 中 V2 不是免费的规定。但是我们不能说

E[E1/V2][E2/V1]

因为 E2 必然有 V1 免费。还是我错过了什么？

Answer 1

这不是反例。除此之外，我不明白你在最后一步的推理——为什么 V1 必须在 E2 中自由出现？除此之外，这E[E1/V2][E2/V1]在你的最后一步不是一个声明。你说“我们不能那样说”是什么意思E[E1/V2][E2/V1]？

你应该尝试为这个假设构造一个明确的反例，即选择V1=V2=x（这真的没关系，由于α转换）然后找到明确的表达式E，，使得它们满足假设的假设（不是自由在），但是表达式不等于 的约简。E1E2V2E1`E[E1/V2][E2/V2](λV1 V2. E ) E1 E2

既然你说你想自己做这个，我不会给你解决方案，但请随时要求更多指点。