7 ms·

What is the contribution of lambda calculus to the theory of computation?

112 points by kocheez75 13y ago

tikhonj 13y ago
The λ-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%29 http://en.wikipedia.org/wiki/Formal_semantics_%28linguistics...
- JumpCrisscross 13y ago
  > 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-predicts-eating.html http://bentilly.blogspot.com/2010/08/analysis-vs-algebra-pre...
- mafribe 13y ago
  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.
  - DanWaterworth 13y ago
    (1) I don't think that's fair to say. The lambda calculus is a way of expressing computations with little regard for how they are actually executed. (2) True, it works better if you add continuations.
    - chrismonsanto 13y ago
      re 1) one of the primary limitations of the lambda calculus wrt concurrency is that it does not model time--there is no way to determine how long a computation takes. An example of a function the lambda calculus cannot define is f(x, y) where the fastest computation of x and y wins. You'll see that function pop up in a number of places in the Haskell world, where it is called "amb". This function is obviously important from a pragmatic POV but it turns out it is also important when doing formal work as well: see the parallel-or/full abstraction problem for PCF[0]. My personal favorite concurrency formalism is the Chemical Abstract Machine[1]. The y-calculus is a neat extension that preserves the spirit of the lambda calculus, but also permits (purely non-deterministic) concurrency. [0]: http://en.wikipedia.org/wiki/Fully_abstract#Abstraction http://en.wikipedia.org/wiki/Fully_abstract#Abstraction [1]: http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf
      - mafribe 13y ago
        Most process calculi (including the CHAM) don't model time. I think it's perfectly possible to consider computation without timing. Adding timing is straightforward for any model of computation with operational semantics. This addition generally changes the semantics dramatically (eg. equalities that hold). There are many timed versions of process calculus, e.g. timed CCS, timed CSP, timed pi-calculus.
- ryanklee 13y ago
  > implement it almost for free What does this phrase mean?
  - nmrm 13y ago
    I suspect what the parent author meant is that the lambda calculus is a very simple language. If a new language feature can be defined as a small extension to the lambda calculus, then creating a toy implementation is should be easy because the new language is so small. More importantly, since your new language is small, you can eyeball the implementation and be fairly confident that the implementation "matches" your formal definition (about which you might prove theorems such as type safety). Contrast this with defining a new feature as an extension of C++, Haskell or Java. You'll invest a lot of time, and in the end might not even be very confident that your implementation matches your theory. So you might write a few hundred line program in your new programming language, get a wonky result, and not be sure if the formal definition is flawed or if the implementation is buggy. The "implement almost for free" phrase takes on a different meaning if you decide to implement computer-checkable proofs about your language.
    - ryanklee 13y ago
      Excellent! Thank you for your explanation. My initial suspicion was that the phrase somehow related to logarithmic efficiency -- which made no sense at all to me!
javajosh 13y ago
The 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.
- ericssmith 13y ago
  I'm not sure what you mean by "equivalent", but historically, the "computer science problem" that lambda calculus has been used to address is understanding the meaning of expressions in programming languages. The first paper to introduce lambda calculus in relation to computers was Peter Landin's "The mechanical evaluation of expressions" (1964). Its specific goal was to use the lambda calculus to model the facilities of other programming languages in use at the time. Landin continued this investigation with two more papers in the series: "A Correspondence Between ALGOL 60 and Church's Lambda-Notation" (1965) and "The Next 700 Programming Languages" (1966). Because of the LC's basis in mathematics and logic, it provided a useful way to define the semantics of programming languages. It continued in this role over the next few decades. One of many high points in this evolution was the use of the LC as the basis of Scheme, "An Interpreter for Extended Lambda Calculus". Among many other contributions, the "Lambda Papers" investigated other models of computation (e.g., actors). So the lambda calculus has been used as a consistent and primitive basis for understanding computation itself and how it is expressed in programming languages. I suppose it is more "equivalent" to Newton's 2nd Law than any particular way to solve a problem. It's perhaps worth remembering that Principia used geometry, not what we know of as calculus, to clarify mechanics.
hyp0 13y ago
see also https://cstheory.stackexchange.com/questions/3650/historical-reasons-for-adoption-of-turing-machine-as-primary-model-of-computatio/3680#3680 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/B/12 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.
- mafribe 13y ago
  The reason why he did not there was no rigorous proof is probably in parts that the result is not controversial at all.
betterunix 13y ago
This comes to mind: http://en.wikipedia.org/wiki/Curry-Howard_Correspondence http://en.wikipedia.org/wiki/Curry-Howard_Correspondence
nvarsj 13y ago
For anyone that wants a readable overview of the λ-calculus, I recommend reading the second chapter in Simon Peyton Jones' book: http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/ http://research.microsoft.com/en-us/um/people/simonpj/papers...
analog31 13y ago
This is probably going to sound really dumb, but I have utterly no formal computer science background. Lambda calculus in the languages where I have seen it (Scheme and Python) simply seems like a way to express a function as a one-liner. Surely, I'm missing something important, but I can't figure out what.
- tel 13y ago
  Viewed that way, that lambda calculus expresses a particular (kind of tiny) feature in a PL, it's pretty boring. What you want to do is take note that lambda calculus, this single, tiny feature in a PL, is powerful enough to simulate every other feature in the PL. The other nice thing is that if you do base your whole language on LC then you get really excellent variable scoping without further questions. That's something that a lot of languages still struggle with (js).
- maxerickson 13y ago
  The Python usage isn't very instructive: http://python-history.blogspot.com/2009/04/origins-of-pythons-functional-features.html http://python-history.blogspot.com/2009/04/origins-of-python... That's the Python language designer saying he wasn't a huge fan of the name when it was introduced, because it didn't quite live up to the expectations it set. The usage of 'lambda' to construct anonymous functions is just a reference to Lambda calculus, the actual thing is a formal system of operating on those functions.
- bcoates 13y ago
  That's just the lambda abstraction, not the lambda calculus. The idea is that a lambda abstraction, in a math sense, is much less general than a single argument function. 'sin θ' is a single argument function that's defined by some business about the ratio of sides of a right triangle with angle θ, but it's not a lambda abstraction because all they're allowed to do is substitute a variable into some expression. 'f(x) = x² - x' can be directly expressed as a lambda abstraction (f = λ x. x² - x) Once you guarantee that the function takes the specific form, you can manipulate it in ways you can't manipulate the general-case function, and it turns out those manipulations give you enough power to define almost anything else you'd want to do. As it turns out, (IIRC) Python makes lambdas essentially opaque objects, and doesn't let you peek into them any more than you can a general-case function. This means you can't do any lambda-calculus on them, even simple stuff like determining if they are exactly the same expression.

112 points by kocheez75 13y ago

The λ-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%29 http://en.wikipedia.org/wiki/Formal_semantics_%28linguistics...

JumpCrisscross 13y ago
> 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-predicts-eating.html http://bentilly.blogspot.com/2010/08/analysis-vs-algebra-pre...
mafribe 13y ago
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.
- DanWaterworth 13y ago
  (1) I don't think that's fair to say. The lambda calculus is a way of expressing computations with little regard for how they are actually executed. (2) True, it works better if you add continuations.
  - chrismonsanto 13y ago
    re 1) one of the primary limitations of the lambda calculus wrt concurrency is that it does not model time--there is no way to determine how long a computation takes. An example of a function the lambda calculus cannot define is f(x, y) where the fastest computation of x and y wins. You'll see that function pop up in a number of places in the Haskell world, where it is called "amb". This function is obviously important from a pragmatic POV but it turns out it is also important when doing formal work as well: see the parallel-or/full abstraction problem for PCF[0]. My personal favorite concurrency formalism is the Chemical Abstract Machine[1]. The y-calculus is a neat extension that preserves the spirit of the lambda calculus, but also permits (purely non-deterministic) concurrency. [0]: http://en.wikipedia.org/wiki/Fully_abstract#Abstraction http://en.wikipedia.org/wiki/Fully_abstract#Abstraction [1]: http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf
    - mafribe 13y ago
      Most process calculi (including the CHAM) don't model time. I think it's perfectly possible to consider computation without timing. Adding timing is straightforward for any model of computation with operational semantics. This addition generally changes the semantics dramatically (eg. equalities that hold). There are many timed versions of process calculus, e.g. timed CCS, timed CSP, timed pi-calculus.
ryanklee 13y ago
> implement it almost for free What does this phrase mean?
- nmrm 13y ago
  I suspect what the parent author meant is that the lambda calculus is a very simple language. If a new language feature can be defined as a small extension to the lambda calculus, then creating a toy implementation is should be easy because the new language is so small. More importantly, since your new language is small, you can eyeball the implementation and be fairly confident that the implementation "matches" your formal definition (about which you might prove theorems such as type safety). Contrast this with defining a new feature as an extension of C++, Haskell or Java. You'll invest a lot of time, and in the end might not even be very confident that your implementation matches your theory. So you might write a few hundred line program in your new programming language, get a wonky result, and not be sure if the formal definition is flawed or if the implementation is buggy. The "implement almost for free" phrase takes on a different meaning if you decide to implement computer-checkable proofs about your language.
  - ryanklee 13y ago
    Excellent! Thank you for your explanation. My initial suspicion was that the phrase somehow related to logarithmic efficiency -- which made no sense at all to me!

javajosh 13y ago

The 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.

ericssmith 13y ago
I'm not sure what you mean by "equivalent", but historically, the "computer science problem" that lambda calculus has been used to address is understanding the meaning of expressions in programming languages. The first paper to introduce lambda calculus in relation to computers was Peter Landin's "The mechanical evaluation of expressions" (1964). Its specific goal was to use the lambda calculus to model the facilities of other programming languages in use at the time. Landin continued this investigation with two more papers in the series: "A Correspondence Between ALGOL 60 and Church's Lambda-Notation" (1965) and "The Next 700 Programming Languages" (1966). Because of the LC's basis in mathematics and logic, it provided a useful way to define the semantics of programming languages. It continued in this role over the next few decades. One of many high points in this evolution was the use of the LC as the basis of Scheme, "An Interpreter for Extended Lambda Calculus". Among many other contributions, the "Lambda Papers" investigated other models of computation (e.g., actors). So the lambda calculus has been used as a consistent and primitive basis for understanding computation itself and how it is expressed in programming languages. I suppose it is more "equivalent" to Newton's 2nd Law than any particular way to solve a problem. It's perhaps worth remembering that Principia used geometry, not what we know of as calculus, to clarify mechanics.

hyp0 13y ago

see also https://cstheory.stackexchange.com/questions/3650/historical-reasons-for-adoption-of-turing-machine-as-primary-model-of-computatio/3680#3680 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/B/12 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.

mafribe 13y ago
The reason why he did not there was no rigorous proof is probably in parts that the result is not controversial at all.

betterunix 13y ago

This comes to mind: http://en.wikipedia.org/wiki/Curry-Howard_Correspondence http://en.wikipedia.org/wiki/Curry-Howard_Correspondence

nvarsj 13y ago

For anyone that wants a readable overview of the λ-calculus, I recommend reading the second chapter in Simon Peyton Jones' book: http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/ http://research.microsoft.com/en-us/um/people/simonpj/papers...

analog31 13y ago

This is probably going to sound really dumb, but I have utterly no formal computer science background. Lambda calculus in the languages where I have seen it (Scheme and Python) simply seems like a way to express a function as a one-liner. Surely, I'm missing something important, but I can't figure out what.

tel 13y ago
Viewed that way, that lambda calculus expresses a particular (kind of tiny) feature in a PL, it's pretty boring. What you want to do is take note that lambda calculus, this single, tiny feature in a PL, is powerful enough to simulate every other feature in the PL. The other nice thing is that if you do base your whole language on LC then you get really excellent variable scoping without further questions. That's something that a lot of languages still struggle with (js).
maxerickson 13y ago
The Python usage isn't very instructive: http://python-history.blogspot.com/2009/04/origins-of-pythons-functional-features.html http://python-history.blogspot.com/2009/04/origins-of-python... That's the Python language designer saying he wasn't a huge fan of the name when it was introduced, because it didn't quite live up to the expectations it set. The usage of 'lambda' to construct anonymous functions is just a reference to Lambda calculus, the actual thing is a formal system of operating on those functions.
bcoates 13y ago
That's just the lambda abstraction, not the lambda calculus. The idea is that a lambda abstraction, in a math sense, is much less general than a single argument function. 'sin θ' is a single argument function that's defined by some business about the ratio of sides of a right triangle with angle θ, but it's not a lambda abstraction because all they're allowed to do is substitute a variable into some expression. 'f(x) = x² - x' can be directly expressed as a lambda abstraction (f = λ x. x² - x) Once you guarantee that the function takes the specific form, you can manipulate it in ways you can't manipulate the general-case function, and it turns out those manipulations give you enough power to define almost anything else you'd want to do. As it turns out, (IIRC) Python makes lambdas essentially opaque objects, and doesn't let you peek into them any more than you can a general-case function. This means you can't do any lambda-calculus on them, even simple stuff like determining if they are exactly the same expression.