题
我工作上的行使问题的书 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)
这是正确的?请帮我理解。
解决方案
一目了然,派生似乎很好。
从概念上讲,只需认为X,Y和Z可以代表任何可计算的函数,显然,其中一些功能不是关联的。说x是“减2”,y是“除以2”,而z为“双”。在此示例中,x(yz)='减2'和(xy)z ='subtract 1'。
其他提示
我还认为您的反例是正确的。
您可能会得到这样简单的反示例:
让 x =λa.n 和 y, z 然后变量:
(xy)z =>((λa.n)y)z => nz
x(yz)=>(λa.n)(yz)=> n
似乎还可以,但是为简单起见,矛盾地证明如何证明呢?
假设(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。
这本书你说过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的所有条款将是平等的,微积分将是微不足道的。因为我们可以找到不平凡模型的氧微积分,没有这样 模型可以等同于真假(更一般地可能等同的条款与不同的正常形式,这就要求我们谈谈有关波姆出技术)。