Motivation behind Lambda Calculus?

Question

The lambda calculus provides a formalism broad used in theoreretical cs to write functions without giving them explicit names, it declares anonymous functions. That is at first glance it's just an alternative form of function notation to write $\lambda$.$f(x)$ instead of $f(x)=x$. But I don't see the reason why this lambda calculus is so important and provides a better way to deal with functions for functional programming languages and from viewpoint of theoretical computer science instead of convential "mathematical" notation $f(x)=x$?

The techniques like curring work fine also with later notation, so what what are the main reasons why lambda calculus is prefered?

Answer 1

There's no difference. Lambda Calculus can't tell if you write $\lambda x . M$, if you write $f(x) = M$ or if you write $\hat{x} . M$ (which apparently was church's original notation? I haven't fact checked that, though).

The reason people care about lambda calculus is because it has exactly 3 combinatorial rules from which all computation follows. The dream is that, by studying these (very simple!) combinatorial rules (and we as mathematicians, and arguably as humans, are very good at reasoning about combinatorics) we can understand something about computation itself.

If you compare even the length of the definition of lambda calculus to the length of the definition of turing machines you'll see why people like this framework.

As a last reason, it's very flexible. We have the 3 basic combinatorial rules, but if we want to express other properties, or make certain operations primitive, it's very easy to extend the lambda calculus to make reasoning about more complicated computation easy.

There's a deep connection between lambda calculus and category theory that's also interesting and worth studying in its own right, but that's a longer discussion.

---

I hope this helps ^_^

Answer 2

Specifically for the question about functional programming, I'd note that lambda calculus is essentially a direct formalization of computation for higher order functions using syntax that is reasonable/desirable to actually use. First-class functions are highly desirable when programming, and once you have them, a 'function literal' is a natural thing to want, which leads to something like λ.

So, from this perspective, λ-calculus is exactly what you want for thinking about programmatic functions, and most other things are inferior. In lambda calculus, you imagine the function just is syntax you wrote, and the way it computes is just by simple rewriting rules that give you other things you might have actually written. Actual programming languages will do something more optimal, but this mental model is pretty close in a lot of ways. By contrast:

• Set theoretic encodings tell you that a function is a set of ordered pairs (of sets, probably), and applying a function is just like a lookup table. The actual thing you wrote has been discarded, and probably some notion of computation has to be added back in to explain what computing actually happens.

• Turing machines require you to first translate the syntax you'd like to write into a state machine operating on symbol strings, which is not at all easy. Then, the machines are a mathematical construction, and to model higher-order programs, one must have a further level of encoding of machines as symbol strings, and the details of all this are far removed from reasoning about the original program.

• μ-recursive functions operate on natural numbers, so the situation is similar to Turing machines, where higher-order programs require a baroque encoding of syntax, and the way the encoding operates may not be obviously related to the original specification.

• SKI combinators check most of the same boxes as λ-calculus, but as mentioned in the comments, writing programs exclusively in combinators is often not nice, and not what people actually want to do.

• ...

That's not to say these other models of computation are worthless. However, when considering a formal, rigorous basis for a programming language based on higher-order functions, lambda calculus or something like it (some variety of type theory) is a pretty natural choice. It gives you exactly what you want with no unnecessary cruft.