It is indeed impossible to determine semantic equivalence of lambda calculus terms. This is one application of Rice's theorem. However, it's easy to compare terms *syntactically*, that is, test if they have the exact same structure (equivalently, if their "string representation" is the same). That's really all you need to get results. For example, to compute functions `n = f(i)` from the naturals to the naturals, you supply the church encoding of `i` as parameter to your lambda calculus function, apply reduction rules until you come to a stop, and inspect the resulting term. If it matches the structure of church numerals, extract the number `n` which it encodes. That's your result. If the resulting term doesn't look like a church numeral, or reduction doesn't halt, the function is undefined at `i`. Lambda calculus terms effectively pull double duty as code and data. Likewise, a Turing machine's tape (a string over some alphabet) can also be interpreted as an encoding of a Turing machine or some aspect thereof. It's only the "default perspective" that differs.