3
$\begingroup$

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

$\endgroup$
7
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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 ? $\endgroup$ – Agnivesh Singh Jun 22 '17 at 18:17
  • $\begingroup$ Axiom (e) is incorrect as written. (The book by Hindley and Seldin does not contain this error.) The abstraction should not go away. $\endgroup$ – Hans Hüttel Jun 22 '17 at 21:30
  • $\begingroup$ :so the RHS remains lambda y.p ? $\endgroup$ – Agnivesh Singh Jun 23 '17 at 3:38
  • $\begingroup$ Yes. I urge you to check the definition in the book. $\endgroup$ – Hans Hüttel Jun 23 '17 at 3:41
  • $\begingroup$ Huttel : Actually this is the screenshot from the book. $\endgroup$ – Agnivesh Singh Jun 23 '17 at 4:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.