Thread: Lambda calculus

Hey, not sure if this is even a good website to pose this question, but I thought I'd try it out.

I'm trying to teach myself some programming language principles by going through various texts/problem sets I find online about lambda calculus. Haven't gotten too far and I'm still trying to work the whole thing out. One statement I'm confused by is this:
If we assume λy.λx.x = λy.λx.yx then we can say that any two lambda terms are equal.

I'm sort of scratching my head on why this is true. Any explanations or leading statements would be much appreciated.

Thanks!

Here is my current idea:

Take two λ-terms: A,B

(λy.λx.x)AB = B
(λy.λx.yx)AB = AB

Under our assumption B = AB, thus A is the identity function.

(λy.λx.x)BA = A
(λy.λx.yx)BA = BA

Under our assumption A = BA, thus B is the identity function.

Thus A = B.

Does this proof sound reasonable? Is the identity function unique?

But any identity function must be unique, right?

Let I, I' be identity functions in λ-calculus.

II' = I
II' = I'

Thus I = I'

Does this work in λ-calculus? Does anyone know?

I'm assuming beta-equivalence is used here, so we have the reduction rule


We can do


ergo for all M,N.

I don't know if all identities are beta-equivalent though, sorry :/