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 Answer 1

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$
1
  • $\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$ Sep 18, 2013 at 9:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .