What is lambda calculus related to? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T04:08:04Z http://mathoverflow.net/feeds/question/983 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to What is lambda calculus related to? Marcus Booster 2009-10-18T02:14:57Z 2010-12-03T03:49:11Z <p>So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based.</p> <p>I was wondering if anyone had a suggestion where I should go from here if I'm interested in learning about similar fields. If would be nice if I could relate it back to programming, but not necessarily a prerequisite.</p> <p>Thanks.</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/987#987 Answer by Tom Leinster for What is lambda calculus related to? Tom Leinster 2009-10-18T02:48:13Z 2009-10-18T02:48:13Z <p>To get you started, you could try this:</p> <p><a href="http://math.ucr.edu/home/baez/week240.html" rel="nofollow">http://math.ucr.edu/home/baez/week240.html</a></p> <p>It has a whole lot of references, some of which you might want to follow up. In particular, some of them describe the close relations between functional programming, lambda calculus and cartesian closed categories. One reference that looks particularly good is the set of lecture notes by Peter Selinger, which are written from a somewhat computer sciencey perspective.</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/992#992 Answer by Theo Johnson-Freyd for What is lambda calculus related to? Theo Johnson-Freyd 2009-10-18T03:39:06Z 2009-10-18T03:39:06Z <p><a href="http://blog.sigfpe.com/" rel="nofollow">A neighborhood of infinity</a> is probably not a place to start, but a place to stop in on from time to time.</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/995#995 Answer by John Goodrick for What is lambda calculus related to? John Goodrick 2009-10-18T04:15:34Z 2009-10-18T04:15:34Z <p>Lambda calculus is also related to the extraction of algorithms from proofs in a natural deduction system, via the Curry-Howard Isomorphism.</p> <p>I vaguely recall this from proof theory classes I took long ago, but it was trivial to look it up on wikipedia:</p> <p><a href="http://en.wikipedia.org/wiki/Curry-Howard_correspondence" rel="nofollow">http://en.wikipedia.org/wiki/Curry-Howard_correspondence</a></p> <p>I recommend the textbook <em>Basic Proof Theory</em> by Troelstra and Schwichtenberg if you're really serious about learning more about this stuff.</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/1136#1136 Answer by physis for What is lambda calculus related to? physis 2009-10-19T02:20:53Z 2009-10-19T02:20:53Z <p>I think, based on Your interests (programming, LISP), that it could work if You followed the path of a Haskell programmer:</p> <p><strong><a href="http://haskell.org/" rel="nofollow">Haskell wiki</a></strong></p> <p>Subpage <strong><em>Learning Haskell</em></strong> is a good place to start (see it in the leftmost column, second below <strong><em>Learning</em></strong> header).</p> <p>Despite of Haskell being a LISP-successor, still, there will be a learning curve (Haskell is very clean, compared to LISP, and it reaches back to several deep logical foundations), but this learning curve can be distributed well along a larger time span, and it will yield fun during the whole time. Even the first minutes will yield pleasure (total lack of side effects, the beauty of currying, the extremely clean economy of concepts). The deeper details will come later automatically (category theory, lambda calculus, combinatory logic, type theory).</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/5928#5928 Answer by Jon Awbrey for What is lambda calculus related to? Jon Awbrey 2009-11-18T05:18:44Z 2009-11-18T05:18:44Z <p>I've posted a few recollections of my days on the SKI Patrol in this memoir on <a href="http://mywikibiz.com/Directory:Jon%5FAwbrey/Papers/Propositions%5FAs%5FTypes" rel="nofollow">Propositions As Types</a>. It's a bit unorthodox, but the <a href="http://mywikibiz.com/Directory:Jon%5FAwbrey/Papers/Propositions%5FAs%5FTypes#Bibliography" rel="nofollow">Bibliography</a> at the end gives a selection of more sainted references that I highly recommend.</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/5979#5979 Answer by Konrad Voelkel for What is lambda calculus related to? Konrad Voelkel 2009-11-18T15:16:58Z 2009-11-18T15:16:58Z <p>Just my 2 cents:</p> <p>When I think about Lambda Calculus, I think first about the adjunction $$Hom(X \times Y, Z) \simeq Hom(X, Hom(Y,Z))$$ which basically tells you "a function in 2 variables with 1 value is the same as a function in one variable with values in a function space of functions in 1 variable with 1 value".</p> <p>This may be a little bit hard to parse at the beginning but I think it truly contains what Currying/Schönfinkeln is about. Sadly, this is often not the way functional programming is taught.</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/37455#37455 Answer by sleepless in beantown for What is lambda calculus related to? sleepless in beantown 2010-09-02T03:47:12Z 2010-09-02T04:39:27Z <p>I would recommend <strong>Structure and Interpretation of Computer Programming</strong> by Hal Abelson from M.I.T.</p> <p>One of the first things I remember learning in SCHEME (a dialect of LISP) was that the $\lambda$-operator was a primitive operator to define a function and that you could write functions which could take functions as arguments and could return functions as results. You could, in fact, nest functions even deeper than this. </p> <p>An example: writing a function called power which when passed a value x returned a function which when passed a value would return the answer value^x. Thus, (defun 'squareit (power 2)) and (defun 'cubeit (power 3)), and (defun 'sqrtit (power 0.5)) were the simple ways to define functions such as square, cube, and square root. </p> <pre><code>(defun (power x) (lambda (y) (exp (* x log(y) ) ) ) (defun 'squareit (power 2)) (defun 'cubeit (power 3)) (defun 'sqrtit (power 0.5)) </code></pre> <p>This should show you how you can return a function of a variable as the result of a function that takes another variable to help define a function like exponentiate that takes two variables (the base and the exponent).</p> http://mathoverflow.net/questions/983/what-is-lambda-calculus-related-to/48131#48131 Answer by Karl S for What is lambda calculus related to? Karl S 2010-12-03T03:49:11Z 2010-12-03T03:49:11Z <p>I suggest learning <a href="http://coq.inria.fr/" rel="nofollow">Coq</a>. It's pretty much the most powerful type system with a complete implementation right now.</p>