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