# Lambda calculus :difficulty in getting hang of induction and conversion

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)$$ ?

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.

• Huttel : Hi Hans , could you explain rule (e) . I understand that if "x" is not a bound variable then the substitution would not yield anything . But isn't there any difference between lambda y.p and p ? Jun 22 '17 at 18:17
• Axiom (e) is incorrect as written. (The book by Hindley and Seldin does not contain this error.) The abstraction should not go away. Jun 22 '17 at 21:30
• :so the RHS remains lambda y.p ? Jun 23 '17 at 3:38
• Yes. I urge you to check the definition in the book. Jun 23 '17 at 3:41
• Huttel : Actually this is the screenshot from the book. Jun 23 '17 at 4:09