Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

cstheory.stackexchange.com

Post reply on HN
Print view View original

11–20 of 49 posts

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

#11

Post by arethuza »

javajosh wrote: post #9
arethuza wrote: post #8

Earlier quoted context omitted.

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

A quick Google should point you in the direction of what people use lambda calculus for:

http://en.wikipedia.org/wiki/Lambda_calculus

One fascinating area for the use of lambda calculus is as a conceptual basis for the implementation of functional programming languages - indeed you could argue that a language is functional iff it can be mapped to the lambda calculus.

Edit: Although it is rather old (like me!) I have fond memories of "The Implementation of Functional Programming Languages" by Simon Peyton Jones:

http://research.microsoft.com/en-us/um/people/simonpj/papers... [PDF]

Another very cool thing is that you can translate expressions in the lambda calculus to SK[I] combinators - which means you can actually implement real programs (including recursion - e.g. using the Y-combinator) as two extremely simple functions - not very efficiently, mind you... :-)

http://en.wikipedia.org/wiki/SKI_combinator_calculus

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

#12

Post by DanWaterworth »

mafribe wrote: post #10
tikhonj wrote: post #2

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 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-n…

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

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

#13

Post by calibraxis »

javajosh wrote: post #3

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?…

Interesting point, since personally in my experience, lambda calculus is overly held up as useful to learn. While simple models are very useful, it has a geek culture/hierarchy aspect too. (http://en.wikipedia.org/wiki/Knights_of_the_Lambda_Calculus)

In explaining things, I find it very important to deflate intimidating-sounding jargon; and discover for oneself if something really is important, or whether it has more of a dysfunctional social purpose like mystery-of-the-priesthood for initiates.

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

#14

Post by chrismonsanto »

DanWaterworth wrote: post #12
mafribe wrote: post #10

Earlier quoted context omitted.

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-n…

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

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

[1]: http://www.lix.polytechnique.fr/~fvalenci/papers/cham.pdf

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

#15

Post by fzltrp »

javajosh wrote: post #3

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?…

How would you write a program which compute the speed of the ball in your example, and how would you ensure or prove that your program is correct? That's what lambda calculus and all its derived works give you. Others have described it more elegantly here, so please refer to their posts, but if you want references, check out the Curry-Howard isomorphism, Hindley-Milner type system, System F, or what Coq, Agda and similar languages bring on the table.

You could also look at the answers given in the linked stackexchange page, of course.

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

#16

Post by chriswarbo »

arethuza wrote: post #11
javajosh wrote: post #9

Earlier quoted context omitted.

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

A quick Google should point you in the direction of what people use lambda calculus for: http://en.wikipedia.org/wiki/Lambda_calculus One fascinating area for the use of lambda calculus is as a conceptual basis for the implementation of functional programming languages - indeed you could argue that a language is functional iff it can be mapped to the lambda calculus. Edit: Although it is rather old (like me!) I have…

> indeed you could argue that a language is functional iff it can be mapped to the lambda calculus.

Lambda calculus is a higher-order, applicative functional language. There are other kinds of functional language.

For example, kappa calculus is first-order. Joy is a pure functional programming language which is based around composition instead of application.

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

#18

Post by chriswarbo »

javajosh wrote: post #9
arethuza wrote: post #8

Earlier quoted context omitted.

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

Lambda calculus is a simple model of substituting values into variables. For anyone studying the behaviour of such a system (eg. programming languages or Mathematical proofs) then LC is an nice, simple model to work with.

A physical-world analogy would be the billiard-ball model of atoms, which works well to describe the behaviour of gasses.

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

#20

Post by Confusion »

fzltrp wrote: post #15
javajosh wrote: post #3

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?…

How would you write a program which compute the speed of the ball in your example, and how would you ensure or prove that your program is correct? That's what lambda calculus and all its derived works give you. Others have described it more elegantly here, so please refer to their posts, but if you want references, check out the Curry-Howard isomorphism, Hindley-Milner type system, System F, or what Coq, Agda and sim…

Your answer is useless to the commenter you are responding to. If he would 'get' lambda calculus by studying the Curry-Howard isomorphism or the Hindley-Milner type system, he already would have. It is like showing someone that asks about rocket science a calculus book or a rocket and saying: just study how it works. For many people that is completely backwards.

First you need to teach them what the lambda calculus fundamentally is and why it is useful in small bits. Then you can explain to them how powerful it gets, by explaining how the usefulness is extended by the Curry-Howard isomorphism and how you can build the Hindley-Milner type system with it.

The commenter is an 'engineer' and you're a 'theoretician'. As a fellow 'engineer', I completely understand his exasperation with all this pointing to either nice theoretical results or the large scale end products of the theory. That's just fundamentally not how we learn.

Post reply on HN