Lambda Calculus Question: If for some λ-terms M and N we have Mx =β Nx. Does it necessarily imply that M =β N?

49 Views Asked by At

I have a homework question that I can't figure out. Hope someone can help.

Assume that for some $\lambda$-terms $M$ and $N$ we have $Mx =_\beta Nx$. Does it necessarily imply that $M =_\beta N$? Here $=_\beta$ stands for $\beta$-equivalent. It is in the paragraph on the Church-Rosser property

Intuitively I would say the answer is yes, but I'm not sure how to show this.

1

There are 1 best solutions below

2
On BEST ANSWER

No, the fact that two $\lambda$-terms $M$ and $N$ are such that $Mx =_\beta Nx$ does not imply that $M =_\beta N$.

As a counterexample, consider the $\lambda$-terms $M = \lambda z.yz$ and $N = y$. We have that $Mx = (\lambda z. yz)x \to_\beta yx = Nx$, and so $Mx =_\beta Nx$. But $M \not=_\beta N$, because both $M$ and $N$ are normal terms, but they are different and hence they cannot be $\beta$-equivalent, by the Church-Rosser property.


The fact that $Mx \simeq Nx$ implies $M \simeq N$ holds if $\simeq$ stands for $\beta\eta$-equivalence, that is, the union of $\beta$-equivalence and $\eta$-equivalence. $\eta$-equivalence is the equivalence relation generated by $\lambda x. M x =_\eta M$ when $x$ is not free in $M$.