4

In a previous question I have been told that lambda calculs is pure syntax. I see that Lambda calculus is introduced inductively, but I don't see from what axioms it follows that: $$(\lambda x.x) M \leadsto_\beta M$$ Because in the reduction above $\lambda x.x$ is seen as a function over Lambda terms.

Can somebody explain me what is the point here?

Community
  • 1
Vitaly Olegovitch
  • 586

1 Answers1

7

Posted as an answer, as requested by the OP.

Writing $$(λx.\ x)\ M=M$$ is wrong (or yields falsehood), those two terms are not equal.

I think what you want is the $β$-reduction, that is, $$(λx.\ x)\ M\ {\leadsto}_\beta\ M,$$ however, as the name suggests, reduction is not equality. In case of $\beta$-reduction, the definition clearly states why $(\lambda x.\ x)\ M\ \leadsto_\beta \ M$, namely $(\lambda x.\ x)\ M$ rewrites to $x[x \mapsto M]$ which is $M$.

I hope this helps $\ddot\smile$

dtldarek
  • 37,381
  • If I understand correctly in another example $(\lambda x.xx)M$ rewrites to $xx[x \rightarrow M]$ and then to $M$. Am I right? – Vitaly Olegovitch Feb 25 '14 at 13:35
  • 4
    @VitalijZadneprovskij No, $xx[x\mapsto M]$ rewrites to $MM$ and what then depends on $M$. E.g. if $M = (\lambda x.\ x\ x)$ then $MM \leadsto_\beta MM$. – dtldarek Feb 25 '14 at 16:34
  • 1
    Note that some authors (like Barendregt) use $=$ for equality in the theory generated by the $\lambda$-calculus, so in that case one actually has $(\lambda x.x) M = M$. – Guido Nov 25 '16 at 03:28
  • @Guido Right, but then the equality is in fact between equivalence classes of relation that groups terms equivalent in the generated theory. – dtldarek Nov 25 '16 at 05:51
  • 1
    Coming back to this, you say "$xx[x \rightarrow M]$ rewrites to $MM$". This is wrong, $xx[x \rightarrow M]$ is exactly $MM$, the substitution is not a reduction step (unless one works with explicit substitutions like Abadi, Cardelli, Curien and Levy). – Guido Mar 10 '17 at 15:47
  • 1
    @Guido Yeah, you are right, substitution operator is usually in the meta-language. – dtldarek Mar 10 '17 at 17:40