关联性在氧微积分

Question

我工作上的行使问题的书 Lambda微积分.其中一个问题，我坚持证明如下：表明，该申请不是缔;事实上，x(y-z)不等(x-y)z

这里是我的工作到目前为止：

Let x = λa.λb. ab
Let y = λb.λc. bc
Let z = λa.λc. ac

(xy)z => ((λa.λb. ab) (λb.λc. bc)) (λa.λc. ac)    
=> (λb. (λb.λc. bc) b) (λa.λc. ac)    
=> (λb.λc. bc) (λa.λc. ac)    
=> (λc. (λa.λc. ac) c)

x(yz) => (λa.λb. ab) ((λb.λc. bc) (λa.λc. ac))    
=> (λb. ((λb.λc. bc) (λa.λc. ac)) b)    
=> (λb. (λc. (λa.λc. ac) c) b)

这是正确的？请帮我理解。

Answer 1

一目了然，派生似乎很好。

从概念上讲，只需认为X，Y和Z可以代表任何可计算的函数，显然，其中一些功能不是关联的。说x是“减2”，y是“除以2”，而z为“双”。在此示例中，x（yz）='减2'和（xy）z ='subtract 1'。

Answer 2

我还认为您的反例是正确的。
您可能会得到这样简单的反示例：

让 x =λa.n 和 y, z 然后变量：

（xy）z =>（（λa.n）y）z => nz
x（yz）=>（λa.n）（yz）=> n

Answer 3

似乎还可以，但是为简单起见，矛盾地证明如何证明呢？

假设（xy）z = x（yz），然后

x = λa.λb. a     # x = const
y = λa. -a       # y = negate
z = 1            # z = 1

并显示（（xy）z）0≠（x（yz））0。

Answer 4

这本书你说过Barendregt是非常正式的和准确的(一个伟大的书)，因此它将是很好的具有明确说明的运动。

我想实际目的是找到实例为x、y和z类， x(y z)减少到boolean true=\xy。x和(x y)z减少到boolean false=\xy。y

然后，你可以比如x=\z。真的，z=I=\z。z(y任意的).

但是，我们如何证明真正的不可兑换的假?你有没有办法证明内部的微积分，因为你没有否定:你只能证明平等和不不平等现象。然而，让我们观察到，如果真=false然后所有条款都是平等的。

事实上，对于任何M和N，如果真=false然后

                         true M N = false M N

但真正的M N减少了，M，同时假M N降低，N，所以

                              M = N

因此，如果真=false的所有条款将是平等的，微积分将是微不足道的。因为我们可以找到不平凡模型的氧微积分，没有这样 模型可以等同于真假(更一般地可能等同的条款与不同的正常形式，这就要求我们谈谈有关波姆出技术)。