Lambda calculus :difficulty in getting hang of induction and conversion

Question

I am going through the book on lambda calculus by Hindley and Seldin . They introduce the syntactic equivalence of expressions and proving them by a technique named "induction" , which has not been directly defined in the book .

(a) $[N/x]x \equiv N$

(b) $[N/x]a \equiv a$ for all atoms $a \not \equiv x$

(c) $[N/x](PQ) \equiv ([N/x]P)([N/x]Q)$

(d) $[N/x](\lambda x.P) \equiv (\lambda x.P)$

(e) $[N/x](\lambda y.P) \equiv P$ if $x \not \in FV(P)$.

(f) $[N/x](\lambda y.P) \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.

(g) $[N/x](\lambda y.P) \equiv \lambda z. [N/x][z/y]P$ if $x \in FV(P)$ and $y \in FV(N)$.

The above are the rules given for substitution in the book. I have some difficulty in understanding (d).

Why is it so that $$ [N/x] ( \lambda x . p) = ( \lambda x . p) $$ ? How to justify this ? Why can't this be defined to be or equal to $$( \lambda N . p) $$ ?

Answer 1

In the definition of substitution $[N_1/ x]N$, we describe how to replace all free occurrences of the variable $x$ by the expression $N_1$ throughout the expression $N$.

The formation rules defining the syntax of $\lambda$-calculus expressions $e$ are

$$ N ::= x \mid \lambda x.P \mid N_1 N_2 $$

where $x$ ranges over a set of variables. One should think of the abstraction $\lambda x.P$ as a function with argument $x$ and body $P$ – or using standard programming terminology, we think of it as a procedure with formal parameter $x$ and body $P$.

In $\lambda x.P$, the variable $x$ is not free within $P$, so a substitution $[N/x](\lambda x.P)$ cannot change anything.

Moreover, writing $\lambda N.P$ does not make sense; the argument/formal parameter must be a variable.

If you are still puzzled, think of an applied lambda-calculus with integer numerals and consider the expression $\lambda x. x +7$ that informally denotes a function that adds $7$ to its argument. Your proposed substitution rule would give us that $[14/x](\lambda x. x+7) = \lambda 14. x +7$. What would that even mean? (I have no idea.)

By the way, the notion of induction is not esoteric at all. Induction is a central proof technique in mathematics and in computer science, and one cannot understand the lambda calculus without being familiar with it. See https://en.wikipedia.org/wiki/Mathematical_induction for an introduction.