3
$\begingroup$

I'm learning from the 1998 version of "Lectures on the Curry-Howard Isomorphism" book, since it's freely available online (https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf) as opposed to the newer version. If you are not familiar with this version of the book, but you have some experience with the topic, that's fine, I've only read the first few pages of the book so you can help.

The book goes a bit differently than the standard literature on the subject and first defines the concept of pre-terms and only after that defines the concept of $\lambda$-terms. I understood definition 1.1.13 on page 3, of the substitution of $N$ for $x$ in $M$, where $N$ and $M$ are pre-terms, but I have a problem with definition 1.1.22 in page 5 for $\lambda$-terms. It seems like the definition doesn't address every possible case, am I'm wrong? I thought that that's just a typo mistake, as they also mistakenly wrote in the beginning of this definition $M\{x:=N\}$ instead of $M[x:=N]$.

So I assumed they meant an equivalent definition to that for pre-terms, just like definition 1.1.20 of free variables of a $\lambda$-term is the same as definition 1.1.11 of the free variables of a pre-term. But now I'm confused, because in example 1.2.4(i) in page 6, they write $$(xx)[x:=\lambda z.z ] = (\lambda z.z)\lambda y.y,$$ but shouldn't it be $$(xx)[x:=\lambda z.z ] = (\lambda z.z)\lambda z.z?$$ If someone understands what's going on here, I would appreciate their help.

$\endgroup$
2
  • $\begingroup$ You say: "It seems like the definition doesn't address every possible case, am I'm wrong?". Why do you say that? Which case should be missing, according to you? If you are more explicit about that, I can understand better what you don't understand in such a definition. $\endgroup$ Dec 5, 2019 at 0:42
  • $\begingroup$ @Taroccoesbrocco for example the case $(\lambda x. P)[x:=N]$ $\endgroup$ Dec 5, 2019 at 0:51

1 Answer 1

2
$\begingroup$

Both definition 1.1.22 and example 1.2.4 (i) are correct, except for the typo you have already noticed in definition 1.1.22 (they write $M\{x:=N\}$ instead of $M[x:=N]$).

In example 1.2.4 (i), the $\lambda$-terms $(\lambda z.z)\lambda y.y$ and $(\lambda z.z)\lambda z.z$ are identical (as $\lambda$-terms). Indeed, a $\lambda$-term is a class of equivalence of pre-terms modulo $\alpha$-equivalence, which roughly means that $\lambda$-terms identify pre-terms that differ only for renaming of bound variables. Now, $\lambda z.z =_\alpha \lambda y.y$ (as pre-terms), hence $(\lambda z.z)\lambda y.y =_\alpha (\lambda z.z)\lambda z.z$ (as pre-terms) and so $(\lambda z.z)\lambda y.y = (\lambda z.z)\lambda z.z$ (as $\lambda$-terms).

In definition 1.1.22 (substitution) no cases are missing. Indeed, this is a definition on $\lambda$-terms (which are classes of equivalence of pre-terms, modulo $\alpha$-equivalence), hence when you write $(\lambda y.N)[x := M]$ (i.e. $([\lambda y.N]_\alpha)[x := [M]_\alpha]$), you can always suppose without loss of generality that $y$ is not a free variable in $M$ and is different from $x$. This is true because if you choose a pre-term $\lambda y.N$ where $y = x$ or $y \in FV(M)$ as a representative of the $\lambda$-term $\lambda y.N$ (i.e. of $[\lambda y.N]_\alpha$), then you can always take a pre-term $\lambda z.N[y:=z]$ where $z \notin FV(N) \cup (M) \cup \{x\}$, which is $\alpha$-equivalent to the pre-term $\lambda y.N$ and hence is another representative of the same $\lambda$-term $\lambda y.N$ (i.e. $[\lambda y.N]_\alpha$).

Concretely, apply for instance definition 1.1.22 (substitution for $\lambda$-terms) to $(\lambda y. yx)[x := yy]$. Now, $y \in FV(yy)$ so apparently we cannot apply definition 1.1.22 (which requires that the abstracted variable should not be in $FV(yy) \cup \{x\}$). However, since $\lambda y.yx$ is a $\lambda$-term, then $\lambda y. yx = \lambda z.zx$ as $\lambda$-terms (i.e. $\lambda y. yx =_\alpha \lambda z.zx$ as pre-terms) and $z \notin FV(yy) \cup \{x\}$, thus we can apply definition 1.1.22:
\begin{align} (\lambda y. yx)[x := yy] = (\lambda z. zx)[x := yy] = \lambda z.z(yy) \end{align}

$\endgroup$
2
  • $\begingroup$ Thank you so much, this was one of the most helpful answers I've ever got in the site. $\endgroup$ Dec 5, 2019 at 11:28
  • 1
    $\begingroup$ @MichaelNovak - You're welcome! $\endgroup$ Dec 5, 2019 at 14:57

You must log in to answer this question.

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