What Is λ-calculus essentially?

Question

I have what I would call a philosophical question about λ-calculus.

When you explore λ-calculus you will be surprised to see all the things that you can do there. You can define integers, arithmetic operations, booleans, if-then-else statements, loops, recursive functions, etc. I believe it has been proven computationally complete.

But on the other side, if you consider what you can do with functions in λ-calculus, you realize that the only thing you can do is to feed it a function and it returns another function. And that process never ends.

So how can you extract a result from a computation?

Suppose the result of an expression is function f. You want to check whether f is what you expected. You can test it, take a function you know, apply f to it and receive g. But to check g is correct, you now need to verify what g does. And you start all over. So how can you tell anything about f?

It seems to me that you can replace all functions in λ-calculus by a single function, the identity function I = λx.x, and everything still works as described in λ-calculus. The Church numeral 3 when given f and x returns f(f(f(x))). But since f and x can only be I, it returns I. I applied to I and I also returns I. So I satisfies the definition of 3. The “booleans” (λxy.x) and (λxy.y) need 2 arguments, which will be I and I so both booleans will return I. Each is equivalent to the identity, even though they behave exactly according to their definitions.

So how do you make the difference? How do you show that λ-calculus deals with more than just a single function?

Is there a concept of identity? Can you identify a function immediately without evaluating it? I believe it was proven that there is no way to test 2 functions for equality.

Or is λ-calculus not about functions, but about the formal description of what they do? That would mean that λ expressions not only define what the functions do but are also the data that the functions manipulates. So when you write A B, you don't apply A to B, but you apply the function described by the string A to formal definition of a function contained in B returning another formal definition.

What is actually going on in λ-calculus? What is the mathematical objects it deals with?

---

Followup:

OK, from the answer below it seems that λ-calculus is not so much about functions in the mathematical sense, but about the subset of functions that can be expressed as λ expressions. Or even more about the manipulation of λ expresssions.

Answer 1

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.

Terms effectively pull double duty as "code" and "data". That's nothing special: A Turing machine's tape (a string over some alphabet) can be --- and frequently is --- interpreted as an encoding of a Turing machine or of some aspect thereof. Likewise, the bits in a von Neumann machine's main memory can be either an encoding of a program or an encoding of something else. Or even both at once. It's only the "default perspective" that differs.