1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I didn't know there was a more recent version of the text I referenced. The new version explains it in much more detail. Thanks. $\endgroup$ – Alistair -L. Sep 18 '13 at 9:09

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.