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.