patternMinor
Lambda calculus :difficulty in getting hang of induction and conversion
Viewed 0 times
conversioncalculushanggettingdifficultyandlambdainduction
Problem
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 \equiv ([N/x]P)([N/x]Q)$
(d) $N/x \equiv (\lambda x.P)$
(e) $N/x \equiv P$ if $x \not \in FV(P)$.
(f) $N/x \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.
(g) $N/x \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) $$ ?
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 \equiv ([N/x]P)([N/x]Q)$
(d) $N/x \equiv (\lambda x.P)$
(e) $N/x \equiv P$ if $x \not \in FV(P)$.
(f) $N/x \equiv \lambda y. [N/x]P$ if $x \in FV(P)$ and $y \not \in FV(N)$.
(g) $N/x \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) $$ ?
Solution
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$ 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 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.
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$ 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 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.
Context
StackExchange Computer Science Q#76660, answer score: 7
Revisions (0)
No revisions yet.