# What Is λ-calculus essentially?

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.

• Could you rephrase the final question to something a little less opinion oriented? There should be a solid non-opinionated answer for this. Sep 19, 2014 at 23:03
• From my education, λ-calculus exists solely to make my brain hurt. I am still not sure how I made it through that class intact.
– user22815
Sep 20, 2014 at 4:48

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`.