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

31–40 of 49 posts

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

#31

Post by arethuza »

chriswarbo wrote: post #16
arethuza wrote: post #11

Earlier quoted context omitted.

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.

Thanks - it was quite a while ago that I was taught about this kind of stuff and for postgraduate study I ended up going down a AI/engineering route rather than programming languages - I now wish I had done the latter given the resurgence of interest in functional programming :-)

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

#32

Post by roywiggins »

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

Lambda calculus is a rigorous mathematical way to define what "computation" even means. You need something -like- Lambda calculus to even begin reasoning about computation mathematically.

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

#33

Post by bcoates »

analog31 wrote: post #21

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.

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.

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

#34

Post by AnimalMuppet »

moron4hire wrote: post #29
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?…

A concrete example: say we use your own. Say we do have a function f(t) that tells us the location of the ball with respect to time. Something like (I'll use JavaScript as my implementation language, as it is capable and accessible): function location_x(t){ return 2 * t; } function location_y(t){ return 3 * t; } In calculus, we say that the derivative of f(t) with respect to t can be approximated by calculating the l…

Your answer doesn't tell him anything about the lambda calculus. It tells him a lot about functional programming.

Is your claim that functional programming is the lambda calculus? Is dependent on the lambda calculus? Is an implementation of the lambda calculus? Something else?

You seem to have some implicit assumptions or claims here. Stating them explicitly could let the GP know what it is that you think you're demonstrating.

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

#35

Post by kd0amg »

bcoates wrote: post #33
analog31 wrote: post #21

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.

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

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.

In λ calculus, the only way one term can inspect another is by applying it. You don't get an intensional view of a λ abstraction. The other language features that get built on top of this (conditionals, tuples, etc.) only rely on functions' extensional features.

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

#36

Post by javajosh »

nandemo wrote: post #28
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?…

A century ago, mathematicians were busy proving theorems (for instance, about calculus), and some of them were trying to figure out if we could start with a mathematical/logical statement and just calculate the answer, "this is true" or "this is false". They were not thinking about electronic computers, and they weren't concerned about how long it would take, they just wanted to know if you could calculate the answer…

Thanks. Can you give me an example of using LC to prove a simple function can (or can't) be calculated? Is f(x){return 1/0} an example of a program that "can't be calculated" or is that just an error (does LC even have a concept of "error")? What about f(x){assert(false)}? Also, f(x){f(x)} clearly won't ever terminate; but how does LC "prove" this?

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

#37

Post by freyrs3 »

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

You're thinking about it from the wrong perspective, the lambda calculus is essentially the equivalent of assembly language for functional programming. The problems you can solve by building abstractions on top of it are infinite, it's utility comes from all properties we can deduce about it when building higher level abstractions, not from it not from being immediately useful to people programming at a higher level any more than x86 assembly is.

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

#38

Post by mafribe »

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.

As to (1) I disagree, it's difficult to express general concurrent/parallel computation in lambda-calculus. You need to resort to encodings. That's why process calculi were invented.

Regarding (2), I'm afraid I also disagree. While continuations can express classical logic in some way, it's generally only possible to express certain cut elimination strategies (e.g. call-by-value, as in the Stewart-Ong lambda-mu-calculus). I don't think we know how to do all of classical logic yet. Moreover, adding jumps (which is what continuations are) to lambda-calculus results in an extremely complicated and hard to understand system (e.g. the reduction semantics of the lambda-mu-calculus is usually only handwaved). If you write the very same semantics in pi-calculus, it's trivial and extremely transparent (see "Control in the Pi-Calculus" by Honda et al). Finally, I think it's conceptually deeply confused to 'add' continuations to lambda-calculus. A much cleaner picture emerges when one understands that the call-return jumping discipline engendered by the function-calls of lambda-calculus is a special case of the general jumping that continuations can do. So really one should start with a continuation calculus, and can then see lambda-calculus as a strict sub-calculus of especially disciplined jumps (call-return with affine usage of the return jump).

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

#39

Post by mafribe »

chrismonsanto wrote: post #14
DanWaterworth wrote: post #12

Earlier quoted context omitted.

(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 importa…

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.

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

#40

Post by mafribe »

hyp0 wrote: post #7

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

The reason why he did not there was no rigorous proof is probably in parts that the result is not controversial at all.
Post reply on HN