Lambda 演算中的结合性
我正在研究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)
这是正确的吗？请帮助我理解。
I am working on the exercise questions of book The Lambda calculus. One of the questions that I am stuck is proving the following:
Show that the application is not associative; in fact, x(yz) not equals (xy)z
Here is what I have worked on so far:
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)
Is this correct? Please help me understand.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（4）
我也认为你的反例是正确的。
您可能会得到一个更简单的反例，如下所示：
I also think that your counter-example is correct.
You can probably get a simpler counter-example like this:
乍一看，推导似乎很好。
从概念上讲，只要认为 x、y 和 z 可以表示任何可计算函数，显然，其中一些函数不具有关联性。比如说，x 是“减 2”，y 是“除以 2”，z 是“双精度”。对于此示例，x(yz) =“减去 2”且 (xy)z =“减去 1”。
The derivations seem fine, at a glance.
Conceptually, just think that x, y, and z can represent any computable functions, and clearly, some of those functions are not associative. Say, x is 'subtract 2', y is 'divide by 2', and z is 'double'. For this example, x(yz) = 'subtract 2' and (xy)z = 'substract 1'.
看起来没问题，但是为了简单起见，用反证法来证明怎么样？
假设 (xy)z = x(yz)，并令
和 证明 ((xy)z) 0 ≠ (x(yz)) 0。
It seems ok, but for simplicity, how about prove by contradiction?
Assume (xy)z = x(yz), and let
and show that ((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 MN 会减少到 M，而 false MN 会减少到 N，因此
，如果 true = false，所有项都将相等，并且微积分将是微不足道的。由于我们无法找到 lambda 演算的平凡模型，因此没有这样的模型
模型可能等同于真与假（更一般地可能等同于具有不同范式的项，这需要我们讨论玻姆输出技术）。
The book you mention by Barendregt is extremely formal and precise (a great book), so it would be nice to have the precise statement of the exercise.
I guess the actual goal was to find instantiations for x, y and z such that
x (y z) reduces to the boolean true = \xy.x and (x y) z reduces to the boolean false = \xy.y
Then, you can take e.g. x = \z.true and z = I = \z.z (y arbitrary).
But how can we prove that true is not convertible with false? You have no way to prove it inside the calculus, since you have no negation: you can only prove equalities and not inequalities. However, let us observe that if true=false then all terms are equal.
Indeed, for any M and N, if true = false then
but true M N reduces to M, while false M N reduces to N, so
Hence, if true = false all terms would be equal, and the calculus would be trivial. Since we can find not trivial models of the lambda calculus, no such
model may equate true and false (more generally may equate terms with different normal forms, that would require us to talk about the bohm-out technique).