Is this a valid reduction? Someone told me this is a valid transformation, in the context of a full $\beta$-reduction.
$$
\lambda f o o . f o o  \rightarrow foo    \label{1}\tag{1}
$$
They seem pretty confident, and while it's been some time since I did any lambda calculus, I can't remember anything that would make that work. Am I just forgetting something?
I mean, it looks a little bit like where $\eta$-reduction would work, if you write it like this:
$$
\lambda f . \lambda o . \lambda o . f o o
$$
And then look at $ \lambda o . foo $ which if you were to drop the final $o$ would mean you could do $\eta$-reduction, right? But that's a totally different expression then.
Is (1) a valid transformation, even if all kinds of reduction are to be done?
 A: No, the step
$$\tag{1}\lambda foo.foo \to foo$$
is not valid either for $\beta$-reduction or for $\eta$-reduction.
Remember that $\lambda foo.foo$ is a shorthand for $\lambda f. \lambda o. \lambda o. foo$.
Indeed, $\beta$-reduction is a step of the form
$$(\lambda x.M)N \to M [N/x]$$
But your LHS term is not of the form $(\lambda x.M)N$, it is instead a term of the form $\lambda f.M$ where $M = \lambda o.\lambda o.foo$, that is,  an abstraction that is not applied, so the $\beta$-reduction step cannot be performed.
Besides, $\eta$-reduction is a step of the form
$$\lambda x .M x \to M$$
where $x$ does not occur free in $M$. In your LHS you have a term of the form $\lambda x.Mx$, it is $\lambda o. foo$ where $x = o$ and $M = fo$.
But the $\eta$-reduction step cannot be performed because $o$ does occur free in $fo$.
More in general, I cannot imagine any meaningful reduction rule such that step $(1)$ is valid, because step $(1)$ add new free variables on the RHS (the variables $f$ and $o$ are bound on the LHS), and this is absolutely meaningless from a semantic point of view.
