$\alpha$-equivalence and the substititution operation over equivalence classes

Question

This post is divided in two parts, viz. Definitions and Question.

---

Definitons

The following definitions are adapted from Lecture notes on the Curry-Howard Isomorphism (by Sorensen and Urzyczyn), pp. 2-5.

Definition. (Pre-terms) Let $V$ be an infinite set (of variables). The set $\Lambda^-$ of pre-terms is given by the following grammar:

$\Lambda^- ::= V|(\Lambda^- \Lambda^-)|(\lambda V\Lambda^-)$

Definition. (Substitution on pre-terms) For $M,N\in\Lambda^-$ and $x\in V$, $M[x:=N]$ is defined as follows (where $x\neq y$):

• $x[x:=N] = N$
• $y[x:=N] = y$
• $(PQ)[x:=N] = P[x:=N]Q[x:=N]$
• $(\lambda x P)[x:=N] = \lambda x P$
• $(\lambda y P)[x:=N] = \lambda y P[x:=N]\quad$ if $y\notin FV(N)$ or $x\notin FV(P)$
• $(\lambda y P)[x:=N] = \lambda z P[y:=z][x:=N]\quad$ if $y\in FV(N)$ and $x\in FV(P)$; $z$ is a fresh variable.

Definition. ($\alpha$-equivalence) Let $=_\alpha \subseteq (\Lambda^-)^2$ be the smallest relation such that:

• $P=_\alpha P\quad$ for all $P$
• $\lambda x P =_\alpha \lambda y P[x:=y]\quad$ if $y\notin FV(P)$

and closed under the rules:

• if $P =_\alpha P'$ then:

  • $\forall x\in V: \lambda x P =_\alpha \lambda x P'\quad$
  • $\forall Z\in\Lambda^-: PZ =_\alpha P'Z$
  • $\forall Z\in\Lambda^-: ZP =_\alpha ZP'$

• $P =_\alpha P'\quad$ if $P'=_\alpha P$

• $P =_\alpha P''\quad$ if $P =_\alpha P'$ and $P'=_\alpha P''$

Definition. ($\lambda$-terms) Define the set of $\lambda$-terms by $\Lambda = \Lambda^-/=_\alpha$, i.e. $\Lambda = \{[M]_{=_\alpha} : M\in\Lambda^-\}$.

Definition. (Substitution on $\lambda$-terms) For $M,N\in\Lambda$ and $x\in V$, $M\{x:=N\}$ is defined as follows:

• $x[x:=N] = N$
• $y[x:=N] = y\quad$ if $x\neq y$
• $(PQ)[x:=N] = P[x:=N]Q[x:=N]$
• $(\lambda yP)[x:=N] = \lambda y P[x:=N]\quad$ if $x\neq y$, where $y\notin FV(N)$

---

Question

My question concerns just the last definition -- substitution on $\lambda$-terms.

• First, the definition presents the notation $M\{x:=N\}$ but then $M[x:=N]$ is used. I believe this is a typo, but I'm not absolutely sure.

• Second, is this a definition by induction? I'm not familiar with definitions over equivalence classes, but I recall to have heard that we can define functions over them as if by induction over the terms.

• Third, and perhaps most importantly, how to make sense of this definition? For instance, is it capture-avoiding as its pre-term counterpart?

I tried to replace $[x:=N]$ with $\{x:=N\}$ and fill in all the $[\cdot]_{=_\alpha}$ in the definition. Is the following translation even close to what is really happening?

• $[x]_{=_\alpha}\{x:=N\} = [x]_{=_\alpha}$
• $[y]_{=_\alpha}\{x:=N\} = N\quad$ if $x\neq y$
• $[(PQ)]_{=_\alpha}\{x:=N\} = [P]_{=_\alpha}\{x:=N\}[Q]_{=_\alpha}\{x:=N\}$
• $[(\lambda yP)]_{=_\alpha}\{x:=N\} = [\lambda y [P]_{=_\alpha}\{x:=N\}]_{=_\alpha}\quad$ if $x\neq y$, where $y\notin FV(N)$

Thank you for reading this long (sorry!) post.

Answer 1

What you should take away from the definition is this :

First, the exact name used for bound variables don't actually matter. Much like $\sum_{i=1}^n i = \sum_{k=1}^n k$, or $f : i \mapsto i+1$ is the same function as $f : k \mapsto k+1$. When using $\lambda$-terms, if we see $\lambda x. E$, it is the same as $\lambda y.E'$ where $E'$ is $E$ except that every free occurence of the name $x$ is replaced with the name $y$.

Second, when you do a substitution, you have to check and make sure that there is no stupid coincidence in the names of bound variables in $M$ and of free araibales in $N$. Much like if $f(x) = \sum_{i=1}^3 (x+i)$ and $g(i) = 2+\cos i$ , if you want to evaluate $f(g(i))$, $i$ is free in $g(i)$, and of course you don't write $f(g(i)) = \sum_{i=1}^3 (2+\cos i+i)$. Instead you rename the index of the sum to some other name. It is the same in $\lambda$-calculus : if you apply $(\lambda x. \lambda y. xy)$ to $(\lambda x.y)$ (where $y$ is free), you will need to change the bound name $y$ before carrying out the computation.

Formalizing this process precisely gives very boring and long-winded definitions.

From what I can see on google book, substitution on $\lambda$-terms is actually defined by $[M]_\alpha[x:= [N]_\alpha] = [M'[x:=N']]_\alpha$ where $M =_\alpha M', N =_\alpha' N'$ and the substitution makes sense (i.e. there is no conflict between free variables in $N'$ and abstractions over occurences of $x$ in $M'$).

In practice, this means that before doing any replacement, you have to rename any conflicting bound variable name in $M$ so that it avoids the names of the free variables of $N$ (and by the way, it is important to check that $\alpha$-equivalence doesn't change the set of free variables of $N$).

When one does such a definition, you have to check that the result, $[M'[x:=N']]_\alpha$ doesn't depend on the choices of $M'$ and $N'$, i.e. if $M''$ and $N''$ are $\alpha$-equivalent to $M$ and $N$, and if the substitution also makes sense, then $M'[x:=N']$ is $\alpha$-equivalent to $M''[x:=N'']$. This will be a very boring proof by induction on the $\alpha$-equivalences between $M'$ and $M''$, and between $N'$ and $N''$.

Once you have proved that this replacement computation is compatible with $\alpha$ equivalence, then you get a well-defined operation on the equivalence classes, i.e. on lambda-terms.