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.