Why is $\lambda x.\lambda y.xy$ not reducible to $\lambda x.x$?
(NB: λ-calculus n00b here!)
I derive the following: $$ \lambda x.\lambda y.xy \equiv \lambda x.(\lambda y.xy) \equiv \lambda x.x $$
To check myself, I tried to reduce the same expression with several online "λ-calculus calculators" (e.g. the λ Calculus Calculator or Lambda Calculator), and, to my surprise, they all agree that the original expression ($\lambda x.\lambda y.xy$) is already in normal form (and therefore, no further reductions are possible).
Where does my derivation go wrong?
My derivation consists of two "moves": (1) "insertion of parentheses" (just to make the evaluation order explicit), and (2) one reduction, namely $\lambda y.xy \equiv x$. The latter is an instance of what the book I am following1 calls an "η-reduction." I figure that one of these two moves must be wrong, but I can't see how.
(FWIW, I do agree with these online calculators that the similar-looking expression $\lambda x.\lambda y.yx$ is in normal form.)
1Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977) by Joseph E. Stoy.
Solution 1:
'Normal form' typically means '$\beta$ normal form' and not '$\beta\eta$ normal form', so your $\eta$-reduction step is not allowed by the normal form calculators.