7
$\begingroup$

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.

|cite|improve this question
$\endgroup$
  • 3
    $\begingroup$ I don't think this question is research-level (after all, I can still answer it…). It's the sort of question that a general computer science site would be an ideal home for. $\endgroup$ – Gilles Nov 12 '11 at 14:50
  • $\begingroup$ Please see the FAQ. You can post TCS questions which are not research level on Mathematics. $\endgroup$ – Kaveh Nov 12 '11 at 16:54
  • 2
    $\begingroup$ I strongly disagree with this assessment of the question. This exact question has been discussed between/with PhD students in my presence. I think this question is "research-level" for under any reasonable definition. $\endgroup$ – Sam Tobin-Hochstadt Nov 14 '11 at 20:19
  • 1
    $\begingroup$ I agree with Sam. Although it's trivial to prove that alpha-conversion isn't required when we just reduce closed terms using reduction strategies that are common in programming languages, I remember that I was quite puzzled when I realised this. I think I was confused because all books about lambda-calculi and programming languages go on about alpha-conversion, and indeed often use de Bruijn indices in their reductions, just to avoid the problem. So I though, there must be some issue that I'm overlooking. Clearly there's a disconnect. $\endgroup$ – Martin Berger Nov 16 '11 at 11:10
  • 1
    $\begingroup$ (cted) A reason why the literature rarely mentions this possibility of avoiding alpha-conversion is that (1) most theoretical accounts of lambda-calculi are written in a logical tradition, where reduction happens under lambdas, and (2) accounts from compiler writers typically, as Gilles points out elsewhere, have in mind 'real' implementations, where open terms are reduced. The discussion here could serve to clarify the matter, and lead the next generation of textbooks to be more lucid about where and when alpha-conversion is truly needed. $\endgroup$ – Martin Berger Nov 16 '11 at 11:12
10
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
8
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Do you know if there are any 'real' programming languages who do without alpha-conversion, because they only reduce closed terms, and never reduce under a binder? $\endgroup$ – Martin Berger Nov 13 '11 at 13:28
  • 1
    $\begingroup$ @MartinBerger Most real programming languages reduce in a global environment. Conceptually, there are two forms of names: global names and local names. With respect to local names, almost all real programming languages reduce only closed terms and not under binders. Thus interpreters can do a pass of resolving global names, then carry on without performing alpha conversion. I believe this technique is folklore among interpreter writers. $\endgroup$ – Gilles Nov 13 '11 at 16:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.