我正在研究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)
它是否正确？请帮我理解。
我也认为你的反例是正确的。
您可能会得到一个更简单的反例，如下所示：
让x = λa.n和y , z变量然后：
(xy)z => ((λa.n) y) z => nz
x(yz) => (λa.n) (yz) => n
乍一看，这些推导似乎很好。
从概念上讲，只要认为 x、y 和 z 可以表示任何可计算的函数，显然，其中一些函数不是关联的。比如说，x 是“减 2”，y 是“除以 2”，z 是“加倍”。对于此示例，x(yz) = '减 2' 和 (xy)z = '减 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。
你提到的 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 技术）。