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 do you think is actually going on in λ-calculus?