Associativity in Lambda calculus

Question

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.

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

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

Answer 3

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 4

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

                         true M N = false M N

but true M N reduces to M, while false M N reduces to N, so

                              M = N

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).