What is lambda calculus related to? - MathOverflow

What is lambda calculus related to?

2009-10-18T02:14:57Z

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.

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.

Thanks.

Answer by Tom Leinster for What is lambda calculus related to?

2009-10-18T02:48:13Z

To get you started, you could try this:

http://math.ucr.edu/home/baez/week240.html

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.

Answer by Theo Johnson-Freyd for What is lambda calculus related to?

2009-10-18T03:39:06Z

A neighborhood of infinity is probably not a place to start, but a place to stop in on from time to time.

Answer by John Goodrick for What is lambda calculus related to?

2009-10-18T04:15:34Z

Lambda calculus is also related to the extraction of algorithms from proofs in a natural deduction system, via the Curry-Howard Isomorphism.

I vaguely recall this from proof theory classes I took long ago, but it was trivial to look it up on wikipedia:

http://en.wikipedia.org/wiki/Curry-Howard_correspondence

I recommend the textbook Basic Proof Theory by Troelstra and Schwichtenberg if you're really serious about learning more about this stuff.

Answer by physis for What is lambda calculus related to?

2009-10-19T02:20:53Z

I think, based on Your interests (programming, LISP), that it could work if You followed the path of a Haskell programmer:

Haskell wiki

Subpage Learning Haskell is a good place to start (see it in the leftmost column, second below Learning header).

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

Answer by Jon Awbrey for What is lambda calculus related to?

2009-11-18T05:18:44Z

I've posted a few recollections of my days on the SKI Patrol in this memoir on Propositions As Types. It's a bit unorthodox, but the Bibliography at the end gives a selection of more sainted references that I highly recommend.

Answer by Konrad Voelkel for What is lambda calculus related to?

2009-11-18T15:16:58Z

Just my 2 cents:

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

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.

Answer by sleepless in beantown for What is lambda calculus related to?

2010-09-02T03:47:12Z

I would recommend Structure and Interpretation of Computer Programming by Hal Abelson from M.I.T.

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.

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.

(defun (power x) (lambda (y) (exp (* x log(y) ) ) )

(defun 'squareit (power 2))

(defun 'cubeit (power 3))

(defun 'sqrtit (power 0.5))

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

Answer by Karl S for What is lambda calculus related to?

2010-12-03T03:49:11Z

I suggest learning Coq. It's pretty much the most powerful type system with a complete implementation right now.