Return to Answer

I would like to venture an opinion that is different from those of @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with having only 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.

Added after @babou's comment: there is nothing wrong with having named functions. You can do this as follows: $ let\ f = M\ in\ N $ is a shorthand for $ (\lambda f.M)N $ in the call-by-value $\lambda$-calculus.

I would like to venture an opinion that is different from those of @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with having only 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.

Added after @babou's comment: there is nothing wrong with having named functions. You can do this as follows: $\mathsf{let} f = M \mathsf{in} N$ is a shorthand for $ (\lambda f.N)M $ in the call-by-value $\lambda$-calculus.

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 having only 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.

Added after @babou's comment: there is nothing wrong with having named functions. You can do this as follows: $ let\ f = M\ in\ N $ is a shorthand for $ (\lambda f.M)N $ in the call-by-value $\lambda$-calculus.

I would like to venture an opinion that is different from those of @babou and @YuvalFilmus: It is vital for pure $\lambda$-calculus to have anonymous functions. The problem with having only 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.

Added after @babou's comment: there is nothing wrong with having named functions. You can do this as follows: $ let\ f = M\ in\ N $ is a shorthand for $ (\lambda f.M)N $ in the call-by-value $\lambda$-calculus.

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 having only 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.

Added after @babou's comment: there is nothing wrong with having named functions. You can do this as follows: $ let\ f = M\ in\ N $ is a shorthand for $ (\lambda f.M)N $ in the call-by-value $\lambda$-calculus.

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 having only 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.

Added after @babou's comment: there is nothing wrong with having named functions. You can do this as follows: $ let\ f = M\ in\ N $ is a shorthand for $ (\lambda f.M)N $ in the call-by-value $\lambda$-calculus.