Associativity in Lambda calculus

Question

Hi All,

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.

Regards, darkie

Answer 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'.

Answer 2

It seems ok, but for simplicity, how about prove by contradiction?

Assume (xy)z = x(yz), and let

x = λa.λb. a     # x = const
y = λa. -a       # y = negate
z = 1            # z = 1

and show that ((xy)z) 0 ≠ (x(yz)) 0.

Answer 3

I also think that your counter-example is correct.
You can probably get a simpler counter-example like this:

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

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