lambda-calculus - Lambda 演算中的结合性

Question

我正在做书 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)

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

Answer 1

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

let x = λa.n and y, z variables then:

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