Motivation behind Lambda Calculus

computer sciencelambda-calculuslogictype-theory

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?

Best Answer

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 ^_^

Related Question