16
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ I was always amazed why such simple thing like change of interpretation may have influence on opinion about consistency of mathematical theory: en.wikipedia.org/wiki/Kleene%E2%80%93Rosser_paradox see: "An alternate solution is to re-interpret lambda calculus not as a theory of logical assertions, but rather as a means of expressing computation. In this way, the paradox can be "solved" by reinterpreting it as a recursive statement, that is, the infinite recursion implying". So how semantic and syntactic are really related? $\endgroup$
    – kakaz
    Mar 13, 2010 at 13:55

7 Answers 7

18
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ That's one of my favorite TWFs ever!!! $\endgroup$ Sep 2, 2010 at 16:39
10
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ @Konrad, I agree completely. That was one of the first things I remember learning in SCHEME, 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) ) ) ) $\endgroup$ Sep 2, 2010 at 3:42
8
$\begingroup$

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

$\endgroup$
7
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ That was an interesting link, it also brought me to Combinatory logic which is the kind of terms I was looking for. $\endgroup$ Oct 18, 2009 at 5:22
6
$\begingroup$

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

$\endgroup$
3
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ also see Konrad V's comment in this question that says this same thing in a different way: (power x y)= ((powertothe y) x) $\endgroup$ Sep 2, 2010 at 3:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.