What is the contribution of lambda calculus to the theory of computation?
cstheory.stackexchange.com
What is the contribution of lambda calculus to the theory of computation?
1–10 of 49 posts
Re: What is the contribution of lambda calculus to the theory of computation?
#2The λ-calculus is basically the MVP of programming languages. It allows somebody designing a language feature or part of a type system to experiment with that feature in isolation. Fast iteration for programming language designers.
It's also great as the core of a programming language. If you can express a feature just in terms of the λ-calculus, you can implement it almost for free. It's just desugaring. Most of Haskell is like this: while the surface language has become rather complex, the majority of the features boil away rather transparently into typed lambda terms. Haskell uses a variant of System F which it actually calls "Core" to underscore how core this concept is :).
Of course, as the accepted answer points out, the λ-calculus is also very useful for logic. In some sense, it is a sort of "proof essence": the basic building block of what a proof is. I really like this notion because it gives me a concrete, first-class object to represent a proof. Seeing proofs as programs really helped me come to terms (heh) with mathematical logic.
One surprising use for the λ-calculus outside of CS is in linguistics. In particular, linguists use typed λ-calculi to construct formal semantics for sentences. It's a way to build up the meaning of, well, meaning. Or at least the things we say ;). I'm not super familiar with semantics in linguistics, but I've always thought it was very cool that they also use some of the same tools as programming language theory! Wikipedia has more about this: http://en.wikipedia.org/wiki/Formal_semantics_%28linguistics...
Re: What is the contribution of lambda calculus to the theory of computation?
#3The importance of calculus is most easily demonstrated by applying it to physics problems. For example, if I tell you how a ball moves in time, and then ask you how fast it's moving after a certain number of seconds, then calculus will help you find the answer (take the derivative of the equation of motion and plug in the time).
What is the equivalent computer science problem that lambda calculus can help you solve? Challenge: pretend like you're Richard Feynman and avoid jargon, if at all possible.
EDIT: I find it quite curious that I got so badly down-voted (-3 and counting!) for simply asking for concrete examples of applicability to actual, concrete problems. I've always found that tools are best understood in the context of their use. Even an abstract concept is useful to speak about in this way - for example, complexity/Big O analysis helps us with capacity planning, comparing algorithms, and so on. It may be that lambda calculus helps us with, oh, decomposition of computation or something like that. But for all the digital ink I've read about it, it's always seemed like an academic form of name-dropping. Even the name is intimidating, right? Reminds me of terms like "schroedinger's equation" or "canonical ensemble" from the good old days in physics class. But behind the intimidating names is just a tool for solving problems - and I have yet to see anyone demonstrate this for lambda calculus. Granted I haven't looked very hard!
It takes self-awareness to realize that you are enthralled with something without understanding it. The litmus test for this is the umbrage taken by someone who's asked simple question about what their high-status concept is really used for. That's why I mentioned Feynman in particular, because of his wonderful reputation as having knowledge that was totally grounded in reality.
Re: What is the contribution of lambda calculus to the theory of computation?
#4The λ-calculus is basically the MVP of programming languages. It allows somebody designing a language feature or part of a type system to experiment with that feature in isolation . Fast iteration for programming language designers. It's also great as the core of a programming language. If you can express a feature just in terms of the λ-calculus, you can implement it almost for free. It's just desugaring. Most of Ha…
> Seeing proofs as programs really helped me come to terms (heh) with mathematical logic.
I suppose this underscores how some people think algebraically while others think analytically. I am an algebraic thiner. I like to break apart algorithms into a mathematical calculus to understand them.
Humorous: http://bentilly.blogspot.com/2010/08/analysis-vs-algebra-pre...
Re: What is the contribution of lambda calculus to the theory of computation?
#5The importance of calculus is most easily demonstrated by applying it to physics problems. For example, if I tell you how a ball moves in time, and then ask you how fast it's moving after a certain number of seconds, then calculus will help you find the answer (take the derivative of the equation of motion and plug in the time). What is the equivalent computer science problem that lambda calculus can help you solve?…
The term calculus generally refers to a system of calculation. I don't get why you're expecting lambda calculations to solve anything.
Re: What is the contribution of lambda calculus to the theory of computation?
#6The importance of calculus is most easily demonstrated by applying it to physics problems. For example, if I tell you how a ball moves in time, and then ask you how fast it's moving after a certain number of seconds, then calculus will help you find the answer (take the derivative of the equation of motion and plug in the time). What is the equivalent computer science problem that lambda calculus can help you solve?…
The lambda calculus is an intellectual framework for the description of computation and logic, just like Newton's calculus forms the basis for a description of physical processes.
Re: What is the contribution of lambda calculus to the theory of computation?
#7see also https://cstheory.stackexchange.com/questions/3650/historical...
It's interesting that Turing never rigorously proved Turing Machines were a model of computation, it was only an intuitive appeal. He actually apologised for this when introducing them, in his Entscheidungsproblem paper http://www.turingarchive.Entscheidungsproblemorg/browse.php/...
Also curious is that Church wrote to him, saying that he found Turing's model more intuitively convincing.
Intuitive appeal isn't everything of course.
Re: What is the contribution of lambda calculus to the theory of computation?
#8The importance of calculus is most easily demonstrated by applying it to physics problems. For example, if I tell you how a ball moves in time, and then ask you how fast it's moving after a certain number of seconds, then calculus will help you find the answer (take the derivative of the equation of motion and plug in the time). What is the equivalent computer science problem that lambda calculus can help you solve?…
Lambda calculus, like Turing Machines, was created as part of an investigation into the fundamentals of mathematics and in particular what is meant by "computation" - so it was never really intended as a practical tool for solving real world problems - which was arguably very much the motivation for Newton's creation of what is generally called "calculus".
Edit: I don't think javajosh's question is unreasonable - not sure why it is getting downvoted.
Re: What is the contribution of lambda calculus to the theory of computation?
#9The importance of calculus is most easily demonstrated by applying it to physics problems. For example, if I tell you how a ball moves in time, and then ask you how fast it's moving after a certain number of seconds, then calculus will help you find the answer (take the derivative of the equation of motion and plug in the time). What is the equivalent computer science problem that lambda calculus can help you solve?…
Lambda calculus, like Turing Machines, was created as part of an investigation into the fundamentals of mathematics and in particular what is meant by "computation" - so it was never really intended as a practical tool for solving real world problems - which was arguably very much the motivation for Newton's creation of what is generally called "calculus". Edit: I don't think javajosh's question is unreasonable - not…
When you say "real-world problems" are you referring to the physical world? I don't expect that. I'd settle for using it to help me solve a mathematical problem. So far, all I see is a lot of hand-waving and not a lot of "this is a tool that can be applied to this sort of problem".
Re: What is the contribution of lambda calculus to the theory of computation?
#10The λ-calculus is basically the MVP of programming languages. It allows somebody designing a language feature or part of a type system to experiment with that feature in isolation . Fast iteration for programming language designers. It's also great as the core of a programming language. If you can express a feature just in terms of the λ-calculus, you can implement it almost for free. It's just desugaring. Most of Ha…
Two brief comments:
(1) The λ-calculus is better thought of as the MVP of SEQUENTIAL programming languages. It is not a good formalism for concurrency. Thee π-calculus is more suitable for concurrency, and, in a real sense, subsumes λ-calculus (see R. Milner's "Functions as Processes" and its subsequent elaborations for details).
(2) Proofs = λ-terms works best for CONSTRUCTIVE logic. With classical logic where not-not-A = A, it kind of works, but not really well.