4 ms·

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 mat

by nandemo 13y ago

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 at all, using an algorithm and pen an paper, and eventually finishing with an answer. For example, if you have just something like "10^23423 is bigger than 23454^10", there's no question about it, you can calculate the answer by using the definitions of integer numbers, product and exponentiation . But what about any mathematical or logical statement? That was the big question. A re-statement of your example is that differential calculus gives you the definitions of limit and derivative, and it helps you with real world problems that are well modeled by differentiable functions. It also tells you that some functions are not differentiable. Lambda calculus starts with a definition of what is calculating, and then it tells us that the answer to big question is "no", some functions cannot be calculated. But it also tells us that whatever can be calculated, can be done with a very, very simple programming language.

javajosh 13y ago
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?
- Grothendieck 13y ago
  All these statements/calculations/proofs are near-trivial once you've defined an appropriate semantics for your calculus - probably the easiest route is via a small-step operational semantics - see, e.g., Types and Programming Languages. There are many lambda calculi, ranging from the untyped lambda calculus with strict evaluation underlying Scheme to the Calculus of Inductive Constructions which provides an alternative foundation for mathematics to set theory and is the basis of the Coq theorem prover which has formalized proofs of the Four-Color and Feit-Thompson theorems.
  - javajosh 13y ago
    So a student asks a question about how physics helps describe the path of a thrown ball. You answer: "All these physics problems are near trivial once you've laid out the right differential equations and solved for the equations of motion. Probably the easiest route is to use the Leibnitz notation to solve f=ma for various time-independent force functions. "There are many formulations of (classical) mechanics, ranging from ordinary linear differential questions to the use of Lagrangians. The latter is an alternative foundation for mechanics which was useful in the evolution of both classical e&m (Maxwell's equations), quantum mechanics, and even statistical thermodynamics." The problem that I have with LC is not that I think it's useless - I have too much respect for Alonzo Church to believe that. Heck, I've even read Goedel Escher Bach, and enjoyed large swatches of it! What gets me is that people run around singing the praises of the lambda calculus, but when you ask about what it's really good for, you get more formalism. I'm beginning to suspect that the whole thing is an intricate practical joke, that lambda calculus is fundamentally so self-referencing it really doesn't have anything to do with anything, other than itself, which is everything.
    - groovy2shoes 13y ago
      You can think of the lambda calculus as the first general-purpose programming language. Logicians were using it to explore the theory of computation before the modern computer was even invented. But, despite being a general-purpose programming language, it's not very practical to use as one. This is simply because the lambda calculus is so minimal, and we have more sophisticated and featureful programming languages to solve problems with. So while theoretically the LC can compute anything, programmers turn to other languages instead. So what is the LC used for, if not for writing programs? Today, it's used as a basis for research into programming languages. PL researchers will often take the untyped LC and extend it with some feature. This allows that feature to be explored in isolation, and provides a rigorous, well-understood platform for writing proofs. This is how we wound up with the various typed lambda calculi for exploring type theory (e.g., the simply typed LC, System F, etc.). GHC actually reduces Haskell into a typed lambda calculus known as System FC, also known as Core. It uses the Core representation to perform most of its optimizations. I suspect that having a library of proofs about System F available helped quite a bit with implementing the optimizations. The reason students still learn and use the infinitesimal calculus is because it's still one of the best tools we have for certain problems. The reason students don't learn the lambda calculus is because we have better tools for many of it's applications (pick just about any other general-purpose PL). But if you talk to students of type theory, they'll tell you that they did learn the LC and that they use it quite a bit in their research. I think someone already mentioned Pierce's Types and Programming Languages, which is a really good introduction to the topic, starting with the untyped lambda calculus and gradually building upon it. If you're genuinely curious about the stuff LC is used for, that's the place to start. I reckon that for most programmers, the lambda calculus is nothing more than an intellectual curiosity, but for PL researchers it's still a useful tool -- a useful formalism for exploring and demonstrating properties of programming languages and type systems.

by nandemo 13y ago

javajosh 13y ago

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?

Grothendieck 13y ago
All these statements/calculations/proofs are near-trivial once you've defined an appropriate semantics for your calculus - probably the easiest route is via a small-step operational semantics - see, e.g., Types and Programming Languages. There are many lambda calculi, ranging from the untyped lambda calculus with strict evaluation underlying Scheme to the Calculus of Inductive Constructions which provides an alternative foundation for mathematics to set theory and is the basis of the Coq theorem prover which has formalized proofs of the Four-Color and Feit-Thompson theorems.
- javajosh 13y ago
  So a student asks a question about how physics helps describe the path of a thrown ball. You answer: "All these physics problems are near trivial once you've laid out the right differential equations and solved for the equations of motion. Probably the easiest route is to use the Leibnitz notation to solve f=ma for various time-independent force functions. "There are many formulations of (classical) mechanics, ranging from ordinary linear differential questions to the use of Lagrangians. The latter is an alternative foundation for mechanics which was useful in the evolution of both classical e&m (Maxwell's equations), quantum mechanics, and even statistical thermodynamics." The problem that I have with LC is not that I think it's useless - I have too much respect for Alonzo Church to believe that. Heck, I've even read Goedel Escher Bach, and enjoyed large swatches of it! What gets me is that people run around singing the praises of the lambda calculus, but when you ask about what it's really good for, you get more formalism. I'm beginning to suspect that the whole thing is an intricate practical joke, that lambda calculus is fundamentally so self-referencing it really doesn't have anything to do with anything, other than itself, which is everything.
  - groovy2shoes 13y ago
    You can think of the lambda calculus as the first general-purpose programming language. Logicians were using it to explore the theory of computation before the modern computer was even invented. But, despite being a general-purpose programming language, it's not very practical to use as one. This is simply because the lambda calculus is so minimal, and we have more sophisticated and featureful programming languages to solve problems with. So while theoretically the LC can compute anything, programmers turn to other languages instead. So what is the LC used for, if not for writing programs? Today, it's used as a basis for research into programming languages. PL researchers will often take the untyped LC and extend it with some feature. This allows that feature to be explored in isolation, and provides a rigorous, well-understood platform for writing proofs. This is how we wound up with the various typed lambda calculi for exploring type theory (e.g., the simply typed LC, System F, etc.). GHC actually reduces Haskell into a typed lambda calculus known as System FC, also known as Core. It uses the Core representation to perform most of its optimizations. I suspect that having a library of proofs about System F available helped quite a bit with implementing the optimizations. The reason students still learn and use the infinitesimal calculus is because it's still one of the best tools we have for certain problems. The reason students don't learn the lambda calculus is because we have better tools for many of it's applications (pick just about any other general-purpose PL). But if you talk to students of type theory, they'll tell you that they did learn the LC and that they use it quite a bit in their research. I think someone already mentioned Pierce's Types and Programming Languages, which is a really good introduction to the topic, starting with the untyped lambda calculus and gradually building upon it. If you're genuinely curious about the stuff LC is used for, that's the place to start. I reckon that for most programmers, the lambda calculus is nothing more than an intellectual curiosity, but for PL researchers it's still a useful tool -- a useful formalism for exploring and demonstrating properties of programming languages and type systems.