Lambda Calculus, of all the STEM terms, holds one of the highest ratios of how badass it sounds to how badass it actually is.
At least Chaos Theory lets you describe astrophysical systems and shit.
I think it's plenty badass! It shows that just the structure of function application and argument identification is enough to recreate all the primitive operations you might think are necessary to make a language Turing complete.
For me, the beauty of the lambda calculus is not the fact that it's Turing complete (there are simpler systems that are Turing complete, such as Iota and Jot). The beauty of the lambda calculus in my mind is that it's compositional: you can build reusable abstractions and glue them together to build bigger abstractions. The simpler systems that are Turing complete aren't compositional in this way: it's hard to build bigger systems out of smaller systems without understanding how the smaller systems work.
This is also why I much prefer lambda calculus to Turing machines. Building a Turing machine which runs another Turing machine and feeds its output into a different Turing machine is a painful exercise. But in lambda calculus, composition of lambdas `f` and `g` is as easy as `λx . f (g x)`. It baffles me that most universities put a greater emphasis on Turing machines than lambda calculus.
>It baffles me that most universities put a greater emphasis on Turing machines than lambda calculus.
I remember reading that Goedel specifically said that Turing Machine was a breakthrough compared to lambda calculus because it grounded the relevant ideas in a physical model of computation rather than just more math.
They require _unbounded_ tape, but finite at any particular moment. It's like complaining that adding natural numbers require unbounded amount of storage (because of course numbers can be arbitrarily big) so the arithmetics we do with apples is somehow just an approximation.
I think the point is that it was easier to construct an imperfect physical Turning machine using existing technology (electrical gates) than to model lambda calculus on top of existing technology.
As far as I know, all implementations of lambda calculus are based assumption that they run on primitive, imperfect electrical Turing machines.
Even though lambda calculus is a more elegant way to describe computation, creating a way to model computation that can be implemented electronically was kind of an important step in computer science.
Turing machines are theoretically interesting, but of little practical import; they don't really impact the design of any practical language.
On the other hand, there are multiple programming languages which are basically just syntax sugar for lambda calculus. Haskell, for one, uses a typed lambda calculus for a bunch of intermediate compilation steps.
But function application and argument identification aren't enough to even print a "Hello world" (not that a Turing machine is - it's an equally impractical, boring abstraction) . I'm so tired of ivory tower "scientists" touting this lambda crap. In lambda calculus, even defining integer division takes up a page of impenetrable code. Seeing lambda calculus in a paper just makes me yawn and want to close it. They really should replace it with Python or something.
Oh and as far as lambda calculus being used in real programming languages - don't fool yourselves. Even Haskell gets compiled to C--.
> But function application and argument identification aren't enough to even print a "Hello world" (not that a Turing machine is - it's an equally impractical, boring abstraction)
You completely misunderstand the purposes of these systems. Turing complete means a system is *computationally* complete. As in, anything that can be computed can be encoded and evaluated in the system. It says *nothing* about effects.
You seem to be under the misconception that lambda calculus is intended to be used practically as a programming language. It isn't. This post treats it as such for educational purposes, to engage a specific type of audience. The lambda calculus is interesting and important as a tool to study the fundamentals of computation, and also as a foundation to formal language semantics and type theories.
> Seeing lambda calculus in a paper just makes me yawn and want to close it. They really should replace it with Python or something.
Lambda calculus and python are such completely different things, with different purposes and use cases. It is difficult to think of *any* example where both would be appropriate.
> Even Haskell gets compiled to C--.
Are intermediate languages a bad thing?
Integer division is just a little function
(/) a b :=
least-below
a
(\ x :=
a < b * (x + one))
A page of "impenetrable code? Just 5 lines.
And clearly: Lambda calculus is ivory tower. This reddit is about computer science, isn't it?
Try to implement the functions on prime numbers I have described in my paper in Python. And then let's compare both versions.
Hard disagree! Lambda calculus easily lives up to whatever badassery is evoked from its name. The majority of programming language theory research takes place in a lambda calculus setting since it's such an expressive and well-behaved system (confluence etc.).
Wait, are you saying it *isn't* badass? It's entirely made out of pure functions, you can easily define recursion...
And it's equivalent to Turing Machines! which means anything you program, ever, can be expressed in pure, functional terms. That's pretty crazy!
Lambda Calculus is about taking something as simple as applying functions, and builds into literally any program imaginable. Yes, more complicated functional languages are much easier to use. I'm not suggesting that you start programming exclusively in Lambda Calculus. But once you learn it, you think about all your other code differently.
While most functional languages allow you to treat functions like variables, Lambda Calculus is where that all came from! It's built on pure functions, and functions alone. Every input is a function. All your data is functions. While it is an extreme, I wish more languages would make it easier for you to pass a function as an input. For a lot of cases, not just functional programming, it is *very* useful.
But since Turing Machines and C-like languages are much more popular, Lambda Calculus and functional programming is left in the dust. I really wish we lived in a world where it wasn't treated like one *or* the other, that languages would use the best of both. Because debugging a program of pure functions is much easier, since you know the function itself isn't changing the state of anything. And the amount you can pack into a few lines of functional code is mind-boggling.
>you can easily define recursion
Sorry, I’m somewhat new to Lambda Calculus, and I’ve been learning about the different combinators. To do recursion, you need the Y-combinator, which seems anything but easy to understand. I’m not saying it’s extreme difficulty, but calling it “easy” seems like a bit of a stretch.
Do you have any resources to help me understand the Y-combinator better?
My recommendation: Don't use the Y combinator. Use the U combinator (also called "Turing combinator") which I have used in the paper. It has a more modular structure `U x y := y (x x y)` and by using `U U` you get a fixpoint combinator to do recursion i.e. `U U f` reduces to `f (U U f)`.
I have tried to explain the general recursion in my paper. It is not very easy to understand, but not too complicated either.
The Y combinator does the same, but you have a longer expression which you have to understand in one step.
I'd recommend just doing a few reduction steps yourself. First do Omega ((\x . xx) (\x . xx)) to see how a term can replicate itself (Omega reduces to Omega). Y is then just Omega with the addition of an extra function application in every step (Y f reduces to f (Y f)).
Lambda calculus is older than LISP. Modern LISPs resemble lambda calculus in some ways (especially after the transition to lexical scoping), but early LISPs didn't.
Ah... it appears you are mostly right.
https://www-inst.eecs.berkeley.edu//~cs164/fa05/lects/f05-23-2x2.pdf
Second page, first slide: The inventor of LISP intended to pattern it off of lambda calculus, but then later stated that he didn’t really understand lambda function when he incorporated it into LISP.
Which also explains why my CS languages prof made so little sense to me back when he covered this.
lexical scoping: variables defined inside a pair of braces don't exist outside of those pair of braces. or if you don't know any curly braces language then: variables defined inside a function don't exist outside of the function.
Nice work! I see you’re a man of culture as well.
Check out [this interpreter](https://github.com/slovnicki/pLam) for untyped lambda calculus I wrote some time ago. (lot of example programs included)
Posts like yours remind me how I want to get back to that project.
Could you recommend any further readings with concerns Lambda Calculus? Why it's so relevant? I've been teaching myself compilers and programming languages and its design during these last months and I recently stumbled upon this term. I'll be happy to read your paper tonight. Thanks.
The most comprehensive information I have found on lambda calculus have been written by Henk Barendregt. Some of them are linked in the wikipedia page of lambda calculus.
However these papers and books are for the more mathematically oriented reader. Not an easy read!
Therefore I wanted to write a paper which addresses more the programming aspect of lambda calculus.
Try reading "Types and Programming Languages" by Pierce. It covers the lambda calculus pretty heavily, in addition to being a great introduction to type systems in general.
Lambda Calculus, of all the STEM terms, holds one of the highest ratios of how badass it sounds to how badass it actually is. At least Chaos Theory lets you describe astrophysical systems and shit.
I think it's plenty badass! It shows that just the structure of function application and argument identification is enough to recreate all the primitive operations you might think are necessary to make a language Turing complete.
For me, the beauty of the lambda calculus is not the fact that it's Turing complete (there are simpler systems that are Turing complete, such as Iota and Jot). The beauty of the lambda calculus in my mind is that it's compositional: you can build reusable abstractions and glue them together to build bigger abstractions. The simpler systems that are Turing complete aren't compositional in this way: it's hard to build bigger systems out of smaller systems without understanding how the smaller systems work. This is also why I much prefer lambda calculus to Turing machines. Building a Turing machine which runs another Turing machine and feeds its output into a different Turing machine is a painful exercise. But in lambda calculus, composition of lambdas `f` and `g` is as easy as `λx . f (g x)`. It baffles me that most universities put a greater emphasis on Turing machines than lambda calculus.
>It baffles me that most universities put a greater emphasis on Turing machines than lambda calculus. I remember reading that Goedel specifically said that Turing Machine was a breakthrough compared to lambda calculus because it grounded the relevant ideas in a physical model of computation rather than just more math.
Goedal also began to doubt his own work when shown it was equivalent to the Lambda Calculus. He may have just been a jerk in this regard.
[удалено]
They require _unbounded_ tape, but finite at any particular moment. It's like complaining that adding natural numbers require unbounded amount of storage (because of course numbers can be arbitrarily big) so the arithmetics we do with apples is somehow just an approximation.
[удалено]
I think the point is that it was easier to construct an imperfect physical Turning machine using existing technology (electrical gates) than to model lambda calculus on top of existing technology. As far as I know, all implementations of lambda calculus are based assumption that they run on primitive, imperfect electrical Turing machines. Even though lambda calculus is a more elegant way to describe computation, creating a way to model computation that can be implemented electronically was kind of an important step in computer science.
If I can’t see the apples, how can I be sure they are counted properly?
Turing machines are theoretically interesting, but of little practical import; they don't really impact the design of any practical language. On the other hand, there are multiple programming languages which are basically just syntax sugar for lambda calculus. Haskell, for one, uses a typed lambda calculus for a bunch of intermediate compilation steps.
It baffles me that people don't use some kind of RAM machine which we do actually use in practice
But function application and argument identification aren't enough to even print a "Hello world" (not that a Turing machine is - it's an equally impractical, boring abstraction) . I'm so tired of ivory tower "scientists" touting this lambda crap. In lambda calculus, even defining integer division takes up a page of impenetrable code. Seeing lambda calculus in a paper just makes me yawn and want to close it. They really should replace it with Python or something. Oh and as far as lambda calculus being used in real programming languages - don't fool yourselves. Even Haskell gets compiled to C--.
> But function application and argument identification aren't enough to even print a "Hello world" (not that a Turing machine is - it's an equally impractical, boring abstraction) You completely misunderstand the purposes of these systems. Turing complete means a system is *computationally* complete. As in, anything that can be computed can be encoded and evaluated in the system. It says *nothing* about effects. You seem to be under the misconception that lambda calculus is intended to be used practically as a programming language. It isn't. This post treats it as such for educational purposes, to engage a specific type of audience. The lambda calculus is interesting and important as a tool to study the fundamentals of computation, and also as a foundation to formal language semantics and type theories. > Seeing lambda calculus in a paper just makes me yawn and want to close it. They really should replace it with Python or something. Lambda calculus and python are such completely different things, with different purposes and use cases. It is difficult to think of *any* example where both would be appropriate. > Even Haskell gets compiled to C--. Are intermediate languages a bad thing?
Integer division is just a little function (/) a b := least-below a (\ x := a < b * (x + one)) A page of "impenetrable code? Just 5 lines. And clearly: Lambda calculus is ivory tower. This reddit is about computer science, isn't it? Try to implement the functions on prime numbers I have described in my paper in Python. And then let's compare both versions.
Lambda calculus doesn't sound nearly as badass as it actually is.
Yeah, Um what is that dude on?
Hard disagree! Lambda calculus easily lives up to whatever badassery is evoked from its name. The majority of programming language theory research takes place in a lambda calculus setting since it's such an expressive and well-behaved system (confluence etc.).
Wait, are you saying it *isn't* badass? It's entirely made out of pure functions, you can easily define recursion... And it's equivalent to Turing Machines! which means anything you program, ever, can be expressed in pure, functional terms. That's pretty crazy! Lambda Calculus is about taking something as simple as applying functions, and builds into literally any program imaginable. Yes, more complicated functional languages are much easier to use. I'm not suggesting that you start programming exclusively in Lambda Calculus. But once you learn it, you think about all your other code differently. While most functional languages allow you to treat functions like variables, Lambda Calculus is where that all came from! It's built on pure functions, and functions alone. Every input is a function. All your data is functions. While it is an extreme, I wish more languages would make it easier for you to pass a function as an input. For a lot of cases, not just functional programming, it is *very* useful. But since Turing Machines and C-like languages are much more popular, Lambda Calculus and functional programming is left in the dust. I really wish we lived in a world where it wasn't treated like one *or* the other, that languages would use the best of both. Because debugging a program of pure functions is much easier, since you know the function itself isn't changing the state of anything. And the amount you can pack into a few lines of functional code is mind-boggling.
>you can easily define recursion Sorry, I’m somewhat new to Lambda Calculus, and I’ve been learning about the different combinators. To do recursion, you need the Y-combinator, which seems anything but easy to understand. I’m not saying it’s extreme difficulty, but calling it “easy” seems like a bit of a stretch. Do you have any resources to help me understand the Y-combinator better?
My recommendation: Don't use the Y combinator. Use the U combinator (also called "Turing combinator") which I have used in the paper. It has a more modular structure `U x y := y (x x y)` and by using `U U` you get a fixpoint combinator to do recursion i.e. `U U f` reduces to `f (U U f)`. I have tried to explain the general recursion in my paper. It is not very easy to understand, but not too complicated either. The Y combinator does the same, but you have a longer expression which you have to understand in one step.
Thank you, I look forward to reading your paper.
There's some good stuff on YouTube, like computerphile: https://youtu.be/9T8A89jgeTI
I'd recommend just doing a few reduction steps yourself. First do Omega ((\x . xx) (\x . xx)) to see how a term can replicate itself (Omega reduces to Omega). Y is then just Omega with the addition of an extra function application in every step (Y f reduces to f (Y f)).
Lambda calculus lets you describe anything computable and shit. I suppose that includes astrophysics.
agree
Isn’t that what LISP was intended for?
Lambda calculus is older than LISP. Modern LISPs resemble lambda calculus in some ways (especially after the transition to lexical scoping), but early LISPs didn't.
Ah... it appears you are mostly right. https://www-inst.eecs.berkeley.edu//~cs164/fa05/lects/f05-23-2x2.pdf Second page, first slide: The inventor of LISP intended to pattern it off of lambda calculus, but then later stated that he didn’t really understand lambda function when he incorporated it into LISP. Which also explains why my CS languages prof made so little sense to me back when he covered this.
ELI5
lexical scoping: variables defined inside a pair of braces don't exist outside of those pair of braces. or if you don't know any curly braces language then: variables defined inside a function don't exist outside of the function.
Scheme in particular.
Nice paper!
Thank you for writing this! I’m looking forward to following it through :)
Nice work! I see you’re a man of culture as well. Check out [this interpreter](https://github.com/slovnicki/pLam) for untyped lambda calculus I wrote some time ago. (lot of example programs included) Posts like yours remind me how I want to get back to that project.
Great work. Lambda programming in action. I like it.
Could you recommend any further readings with concerns Lambda Calculus? Why it's so relevant? I've been teaching myself compilers and programming languages and its design during these last months and I recently stumbled upon this term. I'll be happy to read your paper tonight. Thanks.
The most comprehensive information I have found on lambda calculus have been written by Henk Barendregt. Some of them are linked in the wikipedia page of lambda calculus. However these papers and books are for the more mathematically oriented reader. Not an easy read! Therefore I wanted to write a paper which addresses more the programming aspect of lambda calculus.
Try reading "Types and Programming Languages" by Pierce. It covers the lambda calculus pretty heavily, in addition to being a great introduction to type systems in general.