2
$\begingroup$

Are there lambda terms $M$ and $B$ with $M \neq B$, so that $M B$ and $(M B) (M B)$ have the same canonical form?

Is a problem I encountered while I am still new with lambda calculus I approached this by having $M = λx.x$ and $B = λy.y$, so $MB = (λx.x) (λy.y) \to_β λy.y$.

\begin{align} (M B) (M B) = ((λx.x) (λy.y)) ((λx.x) (λy.y)) &\to_β (λy.y) ((λx.x) (λy.y)) \\ &\to_β (λx.x) (λy.y) \to_β λy.y \end{align} and thus getting the same canonical form, but I am not confident that I am correct about $(M B) (M B)$.

$\endgroup$
2
$\begingroup$

Your reductions of $MB$ and $(MB)(MB)$ are correct, but they do not answer your question, because $M = \lambda x.x$ and $B = \lambda y.y$ are the same term, while you are looking for $M \neq B$. Indeed, in the $\lambda$-calculus, terms are identified up to renaming of bound variables ($\alpha$-equivalence), where the constructor $\lambda$ (abstraction) is the only binding operator: in the term $\lambda x. N$, the constructor $\lambda x$ binds the free occurrences of $x$ in $N$.

Thus, the terms $\lambda x. x$ and $\lambda y.y$ are the same term because the variables $x$ and $y$ are bound in the first and second term, respectively; therefore, $\lambda x. x$ and $\lambda y.y$ are $\alpha$-equivalent because they can both be rewritten as $\lambda z.z$ by renaming the bound variables $x$ and $y$ by $z$.

(To have another example in mathematics about bound variables, consider that the integrals $\int x^2 dx$ and $\int y^2dy$ are the same, because $dx$ binds the occurrence of $x$ in the body of the integral).

Nonetheless, the answer to your question is positive: there are terms $M$ and $B$ with $M\neq B$, so that $MB$ and $(MB)(MB)$ have the same canonical form. Indeed, take $M = \lambda z\lambda x.x$ and $B = \lambda y.y$. The two terms are really different, in the sense that they are not $\alpha$-equivalent. But $MB$ and $(MB)(MB)$ have the same canonical form, because $MB = (\lambda z\lambda x.x) (\lambda y.y) \to_\beta \lambda x.x$ and

\begin{align} (M B) (M B) = ((\lambda z \lambda x.x) (\lambda y.y)) ((\lambda x.x) (\lambda y.y)) &\to_\beta (\lambda x.x) ((\lambda z\lambda x.x) (\lambda y.y)) \\ &\to_\beta (\lambda x.x) (\lambda x.x) \to_\beta \lambda x.x. \end{align}


Remark. What you call "canonical form" is usually called normal form in the context of the $\lambda$-calculus.

$\endgroup$

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.