1
$\begingroup$

I am reading Type Theory and Formal Proof: An Introduction by Rob Nederpelt and Herman Geuvers.

On page 6, $M \equiv N$ is defined to mean that the $\lambda$-terms $M$ and $N$ are identical.

On page 10, $\alpha$-equivalence is defined to be (Definition 1.5.2):

  1. $\lambda x. N =_\alpha \lambda y. N^{x \to y}$ if $y$ is not a variable in $N$
  2. Any other terms are lambda equivalent iff their subterms are $\alpha$-equivalent
  3. $M =_\alpha M$

On page 12, substitution is defined to be (Definition 1.6.1):

  1. $y[x := N] \equiv N$ if $x = y$ or $\equiv y$ otherwise
  2. $(PQ)[x := N] \equiv (P[x := N])(Q[x := N])$
  3. $(\lambda y. P)[x := N] \equiv \lambda z. (P^{y \to z}[x := N])$ if $P^{y \to z}$ is an $\alpha$-variant of $P$ such that $z$ is not a free variable in $N$

But since $(\lambda a. M)[x := y] \equiv \lambda a. M[x := y]$ if $a \neq x$ but also $(\lambda a. M)[x := y] \equiv \lambda b. M[x := y]^{a \to b}$ and $M[x := y] \equiv M[x := y]$, this would mean that (because of transitivity of $\equiv$) for any term $N$, $\lambda a. N \equiv \lambda b. N^{a \to b}$. Since $\equiv$ also follows rules 2 and 3 of alpha equivalence, this would mean that any $\alpha$-equivalent terms would be identical.

Is this a mistake in the book (does substitution not work for $\lambda y. P$ when $N$ contains a free $y$, as Wikipedia seems to say) ? Or can we really say that two $\alpha$-equivalent terms are identical?

Also, even if this is right, shouldn't there also be a condition that $z \neq x$ in rule 3 of substitution?

$\endgroup$
15
  • $\begingroup$ Why would $(\lambda a. M)[x := y] \equiv \lambda a. M[y := x]$ be valid? $\endgroup$ Commented Jun 22, 2017 at 14:56
  • $\begingroup$ @md2perpe: Sorry, that was a mistake, it was supposed to be $[x := y]$ on both sides. I've fixed my question $\endgroup$ Commented Jun 22, 2017 at 15:05
  • $\begingroup$ From where do you get $(\lambda a. M)[x := y] \equiv \lambda a. M[x := y]$ and $(\lambda a. M)[x := y] \equiv \lambda b. M[x := y]^{a \to b}$? I don't see how they follow from the definitions. $\endgroup$ Commented Jun 22, 2017 at 16:48
  • $\begingroup$ @md2perpe: The first one is from rule 3 of substitution assuming that $a \neq y$ (so we can leave the same name for $a$ ($M^{a \to a} \equiv M$)) and the second is from rule 3 but renaming $a$ to $b$. I've swapped the substitution and the renaming because $a \neq y$ and $b \neq x$ so the order won't matter. $\endgroup$ Commented Jun 22, 2017 at 17:06
  • $\begingroup$ Then we say that the two right hand sides are equivalent (transitivity) and we can either say that $M[x := y] \equiv M[x := y]$ or that we've picked $x$ such that it doesn't appear in $M$ to get the final result. $\endgroup$ Commented Jun 22, 2017 at 17:11

1 Answer 1

Reset to default
0
$\begingroup$

The issue in question stems from the object language/metalanguage distinction; I have edited the title accordingly to make it more explanatory.

First off, there is a file of solutions to selected exercises and errata for the book and, as the OP draws attention, $z\not\equiv x$ is added to the Definition 1.6.1, (3). Thus, the clause (3) in the definition of subsitution reads

$(\lambda y. P)[x := N] \equiv \lambda z. (P^{y\rightarrow z}[x := N])$ if $P^{y\rightarrow z}$ is an $\alpha$-variant of $P$ such that $z\not\in FV(N)$ and $z\not\equiv x$

where $\,^{y\rightarrow z}\,$ denotes renaming of the varible $y$ as $z$ and $\,\equiv\,$ is the symbol for syntactic identity.

The syntactic identity $\equiv$ is the relation between $\lambda$-terms signifying that two terms are strictly symbol-for-symbol identical if it holds. For example, for the distinct variables $y$ and $z$

$$\lambda y.y\not\equiv\lambda z.z$$

though the operational behaviour of these two terms are entirely the same. Therefore, the very clause (3) itself seems to exhibit an incoherence in its statement. Notice that what would be true for the clause (3) must be true for the other clauses as well according to our notion of syntactic identity.

The crucial point is that the definition of substitution is given in the metalanguage. Substitution is a primitive syntactic operation carried out at the meta-level. The expressions of the form $P[x:=N]$ are not among the $\lambda$-terms which are defined by ($V$ is the set of variables):

Definition 1.3.2 (The set $\Lambda$ of all $\lambda$-terms)

(1) (Variable) If $u\in V$, then $u\in\Lambda$.

(2) (Application) If $M$ and $N\in\Lambda$, then $(M N)\in\Lambda$.

(3) (Abstraction) If $u\in V$ and $M\in\Lambda$, then $(\lambda u.M)\in\Lambda$.

Note that, similarly, the commonplace notation $\phi(t/x)$ in logic for replacement of $x$ with $t$ is not part of the (object) language, but a metalinguistic aid added to facilitate comprehension of text.

In essence, the definition of substitution tells that the left-hand side expression of $\,\equiv\,$ syntactically yields the right-hand side expression by the operation, which is revertible from right to left.

It is a virtue of the book that this subtlety is not passed over and mentioned, even though with a cursory remark on page 12, unlike many tutorial texts on $\lambda$-calculus. A major reason may be that we tend to mingle object language and metalanguage in text as well as in speech to convey a fluent exposition.

Actually, later in the book, the authors state that

Notation 1.7.3 With a slight abuse of Notation 1.3.4, we use $\equiv$ also for syntactical identity modulo $\alpha$-equivalence.

$\endgroup$

You must log in to answer this question.