Skip to main content
1 of 5
Martin Berger
  • 8.4k
  • 28
  • 46

I would like to venture an opinion that is different from those of @RealJohnConnor, @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with replacing anonymous functions by named functions is that you need to know in advance how many names you will need. But in the pure $\lambda$-calculus you have no a priori bound on the number of functions used (think about recursion), so you either use (1) anonymous functions, or (2) you go the $\pi$-calculus route and provide a fresh name combinator ($\nu x.P$ in $\pi$-calculus) that gives an inexhaustible supply of fresh names at run-time.

The reason pure $\lambda$-calculus does not have an explicit mechanism for recursion is that pure $\lambda$-calculus was originally intended to be a foundation of mathematics by A. Church, and recursion makes such a foundation trivially unsound. So it came as a shock when Stephen Kleene and J. B. Rosser discovered that pure $\lambda$-calculus is unsuitable as a foundation of mathematics (Kleene–Rosser paradox). Haskell Curry analysed the Kleene-Rosser paradox and realised that its essence is what we now know as Y-Combinator.

Martin Berger
  • 8.4k
  • 28
  • 46