Lambda微积分免费可变问题

我发现迈克戈登的功能性编程介绍Notes在网络上，我试图通过它。第9页有这样的疑问：Lambda微积分免费可变问题

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

给出了V2在E1中不空闲的规定。但是，我们不能说

E[E1/V2][E2/V1]

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

来源

2013-03-24 user2054900

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

你应该尝试构建明确反了这一假说，即选择V1=V2=x（它其实并不重要，因为α转换），然后找到明确表达E，E1，E2使得它们满足假设的假设（V2不在E1中免费），但表达式`E[E1/V2][E2/V2]不等于(λV1 V2. E) E1 E2的减少。

既然你说过你想自己做这个，我不会给你解决方案，但可以随时索要更多的指针。

来源

2013-03-24 23:00:08

似乎在说'（v1 v1 v2。E）E1 E2 = E [E1/V1] [E2/V2]'其中'v1'和'v2'是不同的，就像是说例如'λv1。（λv2。v1）E1 E2'，它可以测试到'（λv2。E1）E2'，这将只是'E1'。但是如果我们试图用'v1 = v2'来表示原始的redex或者只是'v'，使用我们的例子：'λv。（λv。v）E1 E2'这将是beta到E2，这是一个矛盾。因此，（一般情况下）你不能使用alpha'λv1 v2。 E'到'λv v。 E'。 – user2054900 2013-03-25 04:09:41

Lambda微积分免费可变问题

回答

相关问题