I have 2 lambda terms and I am not sure whether the rules of bounded variables in the lambda calculus imply that these 2 terms are equivalent or not.

They are:

  • $λc.λc.bc$
  • $λc.λa.ba$

I know that in the first of the 2 terms the c's in $\dots λ \mathbf{c}.b \mathbf{c}$ are bounded. Likewise the a's in $ \dots \lambda \mathbf{a}.b \mathbf{a}$ are bounded. But I don't know whether the fact that these are both abstracted on c mean they are equivalent or not.


Yes, $\lambda c . \lambda c. bc$ and $\lambda c . \lambda a.ba$ are $\alpha$-equivalent, i.e. they are equal up to renaming of their bound variables.

Indeed, $\lambda c. bc$ and $\lambda a. ba$ are $\alpha$-equivalent (the latter is just obtained by renaming the bound variable $c$ in the former, and vice-versa). And abstraction over a variable that does not occur free ($c$ is not free in either $\lambda c. bc$ or $\lambda a. ba$) preserves $\alpha$-equivalence. Therefore, $\lambda c . \lambda c. bc$ and $\lambda c . \lambda a.ba$ are $\alpha$-equivalent.


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.