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.
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.
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.
I think, based on Your interests (programming, LISP), that it could work if You followed the path of a Haskell programmer:
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).
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.
A neighborhood of infinity is probably not a place to start, but a place to stop in on from time to time.
I suggest learning Coq. It's pretty much the most powerful type system with a complete implementation right now.
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).
