3

我正在研究The Lambda calculus书的练习题。我被困的一个问题是证明以下几点:表明应用程序不是关联的;事实上,x(yz) 不等于 (xy)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)

它是否正确?请帮我理解。

4

4 回答 4

4

我也认为你的反例是正确的。
您可能会得到一个更简单的反例,如下所示:

x = λa.ny , z变量然后:

(xy)z => ((λa.n) y) z => nz
x(yz) => (λa.n) (yz) => n

于 2010-06-20T20:18:51.267 回答
1

乍一看,这些推导似乎很好。

从概念上讲,只要认为 x、y 和 z 可以表示任何可计算的函数,显然,其中一些函数不是关联的。比如说,x 是“减 2”,y 是“除以 2”,z 是“加倍”。对于此示例,x(yz) = '减 2' 和 (xy)z = '减 1'。

于 2010-06-20T20:14:48.140 回答
1

看起来没问题,但为简单起见,用反证法证明怎么样?

假设 (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。

于 2010-06-20T20:17:42.813 回答
1

你提到的 Barendregt 的书非常正式和精确(一本很棒的书),所以如果能对练习进行精确的陈述就好了。

我猜实际目标是找到 x、y 和 z 的实例化,使得 x (yz) 减少到布尔值 true = \xy.x 并且 (xy) z 减少到布尔值 false = \xy.y

然后,您可以采用例如 x = \z.true 和 z = I = \zz (y 任意)。

但是,我们如何证明 true 不能与 false 转换呢?你无法在微积分中证明它,因为你没有否定:你只能证明等式而不能证明不等式。但是,让我们观察一下,如果 true=false,那么所有项都是相等的。

事实上,对于任何 M 和 N,如果 true = false 那么

                         true M N = false M N

但是真 MN 减少到 M,而假 MN 减少到 N,所以

                              M = N

因此,如果真 = 假,所有项都将相等,并且微积分将是微不足道的。由于我们不能找到 lambda 演算的平凡模型,因此没有这样的模型可以等同于真假(更一般地可能等同于具有不同范式的项,这将需要我们讨论 bohm-out 技术)。

于 2017-01-22T17:11:28.950 回答