Why is beta-reduction called *beta*-reduction?

Question

In the context of the lambda calculus, why is beta-reduction called "beta-reduction" and not just reduction, or evaluation? Is there a different kind of reduction that it needs to be distinguished from?

Answer 1

I don't think it's mnemonic for anything. I think it was just ordering. $\alpha$-conversion is a prior concept to $\beta$-reduction. Next, $\beta$-reduction is the core rule of the lambda calculus. $\eta$-expansion/reduction is an important but less significant transformation (and was likely identified later). There's also $\delta$-reduction which in this case is likely mnemonic for "definitions". The Calculus of Inductive Constructions also has $\iota$-reduction for inductive types, and $\zeta$-reduction for let expressions. (I have no idea why they chose $\zeta$, though clearly they weren't going to choose $\lambda$.) Other formal systems built on the lambda calculus have no doubt introduced other reductions and used a similar naming scheme (mainly for tradition at this point).

Answer 2

I don't know how widespread this is, but in some of the literature $\alpha$- and $\eta$-conversion are called $\alpha$- and $\eta$-reduction. E.g. see here, or google "alpha reduction" or "eta reduction" for more examples. (Personally, I prefer calling all three reductions, but there might be a good reason for separating them that I'm not seeing.