1

I just started reading the book Lambda-Calculus and Combinators An Introduction. Using this definition of Substitution in Page 7.

enter image description here

I want to prove that if $M$ is any term $[x/x] M \equiv M$. In the book it is given that proof follows by checking the clauses in the definition. I can't see any formal proof from that. I think that it requires induction on M. Any hints?

Ramana Venkata
  • 2,076
  • Yes, it requires induction on $M$ and then in each case you check the corresponding clauses of the definition. – Aleš Bizjak Dec 17 '13 at 09:40
  • @AlešBizjak We have to use some form of strong induction I guess something that goes like this if $M \equiv (PQ)$ then we have to assume $[x/x]P \equiv P$ or ... What should be the other condition?? – Ramana Venkata Dec 17 '13 at 09:48
  • 2
    You are proving a statement $\forall M \in \mathcal{T}, \forall x \in \mathcal{V}, [x/x]M = M$, where $\mathcal{T}$ is the set of lambda terms and $\mathcal{V}$ is the set of variables. The set of lambda terms is defined inductively therefore you can use structural induction. Then for instance in the case of application $M = P Q$ you can assume that $[x/x]P=P$ and $[x/x]Q = Q$ since $P$ and $Q$ are subterms of $M$. – Aleš Bizjak Dec 17 '13 at 10:09

1 Answers1

0

I am pasting the answer which Aleš Bizjac left in a comment.

Yes, it requires induction on $M$ and then in each case you check the corresponding clauses of the definition. You are proving a statement $∀M∈T,∀x∈V,[x/x]M=M$, where $T$ is the set of lambda terms and $V$ is the set of variables. The set of lambda terms is defined inductively therefore you can use structural induction. Then for instance in the case of application $M=PQ$ you can assume that $[x/x]P=P$ and $[x/x]Q=Q$ since $P$ and $Q$ are subterms of $M$.

MJD
  • 65,394
  • 39
  • 298
  • 580