Are lambda calculus forms with different variable names the same?

Question

Someone suggested to me that the halting problem could be solved by a lambda calculus "program", which reduces to $\lambda y.y$ if an input program halts and $\lambda n.n$ if it does not. Therefore it is not possible to extend this into a program that halts if it thinks it doesn't halt. (That's just background, not the question proper)

I said this is nonsense, because obviously these are the same term written differently. He says we can just look at the output and see whether the variable is called $y$ or $n$, even though a lambda calculus program can't.

I think the lambda calculus reduction rules allow any variable to be renamed at any time for no reason whatsoever, so we can't reliably say what variables will be called after reducing a lambda calculus expression.

Are $\lambda y.y$ and $\lambda n.n$ considered "the same" or equal in lambda calculus?

Answer 1

You are right and your someone is wrong. Lambda terms that only differ in the names of bound variables are beta equivalent, and considered the same program. If the lambda calculus can't see the difference, this means that this implementation in that system is not a solution to the problem.