λ Calculus (2013) [pdf]

Anyone knows if lambda calculus can be done with the standard function notation, or with something closer to that? I understand that lambda calculus works with expressions and symbols, while standard function notation works with functions and values, still using the same notation seems natural to me, x -> e for lambda, and e(x) for application. I haven't worked it out, but I wonder what will I get if I do it?

It was an attempt to find the simplest possible mathematical system that was universal, i.e. could compute any function. It turns out that the answer is that function application by itself is universal (if functions are first-class entities). This was a surprise at the time, and it still generally surprises people today when they first learn of it.

You might find this interesting:

https://flownet.com/ron/lambda-calculus.html

A little bit of historical background.

There was a concerted effort in the late 19th, early 20th century (perhaps earlier too) to mechanise computation i.e., reducing it to a pure symbolic manipulation. There were obvious benefits, a famous one being Enigma Machine that was used to (successfully I think) break the German code during WW-2.

On the philosophical side a parallel and overlapping effort was going on to figure out if mathematics could represent all possible truths, again as symbolic manipulation system. Bertrand Russel's magnum opus Principia Mathematica [1] was one such famous work towards it. Kurt Gödel then made a breakthrough when he proved that such a system is impossible; i.e., a system can either capture all the truths or it can be consistent but not both[2]. Put differently, any mathematical system capable of representing all the truths will necessarily contain contradictions within it.

Now coming to your question.

Lambda calculus emerged in this milieu. Alonzo Church[3] invented one such system to mechanise computation, named ƛ-calculus. Using this system one can mechanically compute any function purely by symbolic manipulation. Later on Turing, Church's student I think, invented a totally different system named Turing Machine with the same purpose. Later on it was proved (by Church and Turing I think, but I'm not 100% sure) that ƛ-Calculus and Turing Machine are equivalent, Church-Turing thesis[4].

All these work, and more, laid the theoretical foundation for the modern computers. If we can today safely assume that computers are provably correct it's because of them.

Phil Wadler has an absolutely delightful talk where he takes us through a whirlwind tour of the history of the mathematical foundation of computers [5], highly recommended.

[1] https://en.wikipedia.org/wiki/Principia_Mathematica

[2]https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...

[3] https://en.wikipedia.org/wiki/Alonzo_Church

[4] https://en.wikipedia.org/wiki/Church–Turing_thesis

[5] https://www.youtube.com/watch?v=IOiZatlZtGU

This is another excellent video if you are more of a Javascript developer: https://www.youtube.com/watch?v=OLH3L285EiY

> I understand that lambda calculus works with expressions and symbols, while standard function notation works with functions and values

There's no inherent connection. You're perfectly free to interpret lambda terms as functions on a domain, or function definitions as abstract rewrite rules.