Closed term and alpha-conversion

Question

In the simply-typed lambda calculus, do we ever need alpha-conversion in a small-step call-by-value reduction of a term that is closed?

The evaluation rule that uses substitution is: $(\lambda x.t_1)~v_2 \to [x\mapsto v_2]t_1$

But if $(\lambda x.t_1)~v_2$ is closed, then $v_2$ is closed and $t_1$ only has $x$ has a free variable. Since $v_2$ has no free variables, substitution won't need alpha-conversion. $[x\mapsto v_2]t_1$ is also closed because the only free variable, $x$, has been substituted by a close term. So the result of the reduction is also closed.

It's also easy to show that for the other rules, if $t$ is closed and $t \to t'$, then $t'$ is closed.

Therefore, since we only substitute closed terms, $\alpha$-conversion is not needed.

Do you agree?

Edit: Actually, what needs to be shown is that if $t$ is closed and $t \to t'$ then in any immediate reduction $t_1 \to t_1'$ used to derive $t \to t'$, $t_1$ is closed. This is not true when reducing under binders.

Answer 1

This is true as long as you're only reducing towards a weak head normal form. But if you want to go further, you start reducing under lambdas. If you're looking at the pure lambda-calculus (typed or not), you must be reducing under lambdas if you're reducing closed terms. And when you're reducing under lambdas, you're no longer operating on closed terms.

Here's an example that starts with a closed lambda-term where all binding sites use unique names, proceeds to a term with repeated but non-capturing binders, then reaches a term with capture, which requires alpha-conversion to proceed. The initial term is not simply-typed, but you can remedy this by changing it to $(\lambda w. (\lambda z. w z z) (\lambda x. \lambda y. x y))$ which is simply-typed and shows the same binding-related issues.

$$ \begin{array}{rl} (\lambda \underline{z}. \underline{z} \underline{z}) \underline{(\lambda x. \lambda y. x y)} \quad \to & (\lambda \underline{x}. \lambda \color{blue}{y}. \underline{x} \color{blue}{y}) \underline{(\lambda x. \lambda \color{red}{y}. x \color{red}{y})} \\ \to & (\lambda \color{blue}{y}. (\lambda \underline{x}. \lambda \color{red}{y}. \underline{x} \color{red}{y}) \underline{\color{blue}{y}}) \\ \to & (\lambda \color{blue}{y}. \lambda \color{red}{y}. \color{blue}{y} \color{red}{y}) \end{array} $$

That last step requires alpha-conversion, to make the blue $y$ and the red $y$ distinct.

Your proof sketch is correct as long as you apply the beta rule in a context that does not bind any variable. If you extend the proof to the lambda context case, it fails when $x$ is in the context.

Answer 2

Your observation was used in by the Sewell et al. in the paper "Ott: Effective Tool Support for the Working Semanticist" (PDF), in which they observed that, if all you really and truly ever want to do is formalize the operational semantics of core functional languages, then you don't, in fact, need alpha-conversion in the formal definition of the programming language.

The main issue is that you have to catch yourself before you do something that causes this to stop working. The most obvious example is the one Gilles mentions, reducing under binders; the paper discusses some others.