why would you use lambda calculus over other forms of function notation?

What does "$\lambda x.x$" offer that "$f(x)=x$" can't cover? More generally, when would we want to represent a function through lambda calculus over another form of function notation?

• I think a better 'anonymous' notational equivalent would be $x \mapsto x$. There is nothing special about the $\lambda$ notation, it just has a lot of history behind it... Feb 15, 2015 at 4:17

This offers options like $\beta$ reduction which is part of the calculus part of lambda calculus. This turns a curious variation in notation into a model of computation, and allows impredictive function abstraction, which gives you a Turing complete models of computation in the untyped lambda calculus. With the typed lambda calculus you can use this anonymous function abstraction and function application to construct things like logical connectives and quantifiers. Without anonymous functions, you have to set up more syntax to define recursive and impredictive definitions, so lambda calculus is the path of least resistance for this sort of thing.
Lambda calculus is a computational model not a formalism for functions. It's not that one notation can do something the other can't, it's that they are used to describe two completely different things. Functions are mathematical entities commonly defined as a certain kind of relation between two sets. The notation used for functions is typically $f\colon A\to B$ and we write things like $f(x)$. Lambda terms are typographical entities described recursively by the lambda calculus definitions. Lambda terms can act on other lambda terms. The notation $\lambda x.x$ is a lambda term, it is just notation equivalent to $f(x)=x$. There are plenty of introductory texts on the lambda calculus and you'll see that if you read only the first few pages, your question here will dissolve.
• it will be impossible to adequately answer this here as basically you are now asking for a crash course in model theory. To keep it short, no, mathematics is not typographical entity. We use a typographical proof system, but the objects we study, mostly, can't even be enumerated. E.g., there are uncountably many functions (even just $\mathbb R \to \mathbb R$, but there are only countably many lambda terms. Further, no, you can't view any particular function as a computational model, at least not in any meaningful way. You really should read a bit about lambda calculus and perhaps some logic. Feb 15, 2015 at 5:02