An interesting detail from the paper is why it is called "LAMBDA". That is because in the original notation what current-day programmers would call formal argument of a function were denoted by putting an upward arrow-head on top of variable/name but since that could not be type-set easily the arrow-head was moved in front of such variable which resembles the Greek letter "lambda".
More likely a hat (following Russel's Principia) maybe simulated as a `/\` capital Greek letter "L" which then was changed to the Greek lower letter lambda. Church's book in 1941 was typed using what looks like a typewriter. The name was catchy though.
He provides theory and code that starts from untyped lambda calculus and progresses to typed lambda calculus, system F, and higher-order system. Note, the article above was written by Barendregt who summarized high-order systems in terms of the "lambda cube". The Pierce book provides enough theory and context to understand why that's important by the time he gets to it in chapter 30.
I really like Lambda Explorer [0]. It's an in-browser interactive tutorial that does a good job of nudging you towards the next idea so you can discover it yourself, but it's there with a solution if you get stuck.
Henk Barendregt, the author of this paper, has an excellent reference book on the untyped lambda calculus called "The Lambda Calculus: Its Syntax and Semantics". I believe he also wrote a book on the typed lambda calculus but I have never read it. This is a good reference text, but in my opinion is not a good introductory text.
For a good introduction, I would recommend J. Roger Hindley's introduction to the lambda calculus and combinatory logic entitled "Lambda-Calculus and Combinators: An Introduction". It includes some interesting info on SKI combinator calculus in addition to the lambda calculus.
Actually the question should be... why is the lambda calculus such a great programming language in practice? The lambda calculus is unique among other theoretical models of computation (automata, turing machines, etc) in that it is the syntactic and computational basis of several popular languages (lisp, Haskell, ML, etc). In all these languages, you can essentially write lambda calculus terms in a way that you cannot write turing machines in imperative languages.
Same reason Turing machines are impractical; it's too low-level. But IMHO starting with "functional composition without side effects" (LC model) and adding the practical stuff gets you a lot farther than adding practical stuff to "everything is a side effect and functions don't exist" (the TM model).
Back in the days before parallel programming, large-scale software engineering, networks, cloud computation, etc it wasn't always clear that anything was wrong with the TM model. But given how computing works today it's clear (to me at least) that LC is a much, much better substrate for designing computation.
As an aside, 1958 was definitely back in those days. But that's when John McCarthy decided the TM model was lacking and said "Hey let's build a programming language on Lambda Calculus instead" and Lisp was born. And that's how John McCarthy was smarter than the rest of us.
The same reason a Turing machine (even a finite one) is a silly programming 'language'. It's an abstract model of computation. It just happens that real-world languages based on The Lambda Calculus like Lisp are only a stone's throw away syntactically, whereas the gulf between even assembly and a Turing machine program is quite large. I suppose that's because The Lambda Calculus doesn't aim to describe a pseudo-physical machine, and therefore leaves implementation much more open to interpretation.
It is a mathematical model of computation and thus it does not concern itself with practicalities like space/time complexity or ease of implementation. On the other hand pretty much all practical functional language builds on top of LC, tackling these practical challenges.
Understood there must be many practical issues, what I'm wondering is if there is an issue, and what is the main issue of using the syntax of Lambda calculus as the basis of a programming language, how is it worse than say Lisp or JavaScript?
For the purpose it was intended (i.e. mathematical analysis of the notion of "computation") it's not worse. It is, in fact, far superior to almost any other system like that.
The point of lambda calculus isn't to be able to program servers or whatever. The point is to be able to express ideas like beta-reduction and Y-combinators in a succint way, and a way that's easy to manipulate with a pencil (or chalk). "Notation as a tool of thought", and all that. Turing machines are similar: they're excellent for modeling computation, but you wouldn't want to use it for actual programming. It's not made for that.
As someone else said: the fact that it is so remarkably close to several actual programming languages is pretty astonishing, and shows that there really is some deep brilliance to Church's original formulation. Turing is more famous for his machines, but it's interesting to note that while no programming language resembles a "raw" Turing machine, MANY languages resemble lambda calculus.
EDIT: to answer your actual question: it's worse than Lisp or JavaScript in any number of ways. There's no state, there's no "I/O" as such, no loops, no function names (well, sortof), no strings, etc, etc. And oh, btw: no numbers. All numbers in lambda calculus is defined in terms of functions, htere's no such thing as a "numeric literal".
As I said: it's not made for actual programming. Doing actual programming in lambda calculus is like trying to use the Peano axioms to calculate how much money you need to pay in the supermarket.
Everything you're saying here is true, but I think you're forgetting something incredibly important that isn't easily representable on a Turing machine at all: equivalences of the terms and their rewrite rules.
Lambda calculus provides you with a set of ways in which you could rewrite your program and get an equivalent one (by the definition of lambda calculus), or how to execute the program itself. It means that most of the functionality for deciding when the code should be executed (by the compiler or at run time) is already in the compiler.
It's something that imperative languages struggle with.
The lack of numbers is not too great a handicap, as one can design numbers to suits one's needs. For instance, the following is a program for computing the characteristic sequence of primes:
\io.let
zero = \x\y.x;
one = \x\y.y;
consz = \xs\p.p zero xs;
oneS = \cont\x\xs\p.p x (xs cont);
zeroS = \cont\x\xs.consz (xs cont);
primes = \N\p.p one (let SN = \r.oneS (N r); F = SN F in (primes SN) F);
main = consz (consz (primes zeroS))
in main
Removing the minimal syntactic sugar results in
\io.(\zero.(\one.(\consz.(\oneS.(\zeroS.(\primes.(\main.main) (consz (consz (primes zeroS)))) ((\f.(\x.x x) (\x.f (x x))) (\primes.\N.\p.p one ((\SN.(\F.primes SN F) ((\f.(\x.x x) (\x.f (x x))) (\F.SN F))) (\r.oneS (N r)))))) (\cont.\x.\xs.consz (xs cont))) (\cont.\x.\xs.\p.p x (xs cont))) (\xs.\p.p zero xs)) (\x.\y.y)) (\x.\y.x)
which can be run, as a 167 bit executable, on a binary lambda calculus machine to produce the infinitely long
"if there is an issue, and what is the main issue of using the syntax of Lambda calculus as the basis of a programming language"
have you used scheme?
From wikipedia
"Scheme is a very simple language, much easier to implement than many other languages of comparable expressive power. This ease is attributable to the use of lambda calculus to derive much of the syntax of the language from more primitive forms."
I cannot simplify the actual paper presented as I am not a mathematician and cannot read Euler expressions (academic calculus). I can speak to lambda calculus from a programming perspective though.
Lambda calculus is the basis of functional programming where a function is a portable black box containing instructions and returning a result. That said, a function is an abstraction such that a container of many instructions may be represented by a single reference. Lambda calculus also accounts for nested functions as a means of expressing layers of abstractions. One such style of layered functions is the notion of creating a new function inside a function and returning that new function, which is called currying. Currying allows for the creation of an abstraction where the computation is not ready at the time of creation, such as awaiting additional input via arguments, but ready once called.
In my own code I use nested functions to create a separation of concerns. This allows me to write code where portions are isolated from other portions but available by reference where needed. This separation provides a formal means of internal architecture and organization by which complexity is reduced.
A major consideration available from lambda calculus is the concept of lexical scope, which is a concept similar to abstraction layers but applies to reference resolution.
Right I would say and argue that lexical scope is the main thing that makes Functional Programming languages Functional Programming languages.
Why? Because it allows a function to create and return a new different instance of a function-skeleton coded in the inner scope, part of which function-instance is the values of the variables in its outer scope which were the values of those variables at the time the outer function returned.
That means it is easy to create new function-instances. Function instances are "first class citizens" as much part of the machinery of such language as any data-structure.
In this sense the "inner function" coded inside an outer is not a function at all. It is just an encoding, a set of instructions for creating a new function which instructions are executed to create a new function when you execute the outer function.
Whereas the outermost function is a function by itself since there can be only one instance of it ever.
In practice the inner function (the body of a lexical closure) is only compiled once. When a "new function is made" at runtime, a data structure for the new lexical environment is created together with a pointer to the already-compiled closure body. So the executable portion (the actual instructions of the closure) are only allocated once.
Please don't take as disregarding your probably clear explanation, but if I had to show my grandma a youtube video about this subject, wich one would you choose?
I'm regarding this subject as
Lambda calculas > lambda functions > serverless > "business logic i can define and upload and let idle in the internets without worrying about managing the computers that actually made that business logic available worldwide behing an URL "
I know the HN crowd is skeptical about serverless but as a non developper, it is pretty mindblowing the barriers that AWS + lambda functions are taking down.
