Cliff's Notes squared: Lambda Calculus

I say Cliff's Notes squared, because this is the Cliff's Notes guide to the Cliff's Notes.  

Up til now, I've mostly shied away from anything that had any significant lambda calculus content -- and when I didn't shy away from it, got nothing out of it.  I read one or two "intro" pieces, but they didn't really click for me.  Happily, I've recently found some stuff that works for me.  For a gentle introduction, I can recommend the following. 

This introduction to the lambda calculus is short and sweet.  It doesn't cover a lot of ground but covers it well, and the exercises really work to give you some insight into the fundamentals.  

Another good short intro is here.  It does a great job of explaining why things are done the way they are, including strategies for manipulating lambda expressions.   The exercises are fewer and I found them to less well integrated into the text. I think it's a great companion to the first article -- it provides a bit more explanation where the first article relies a bit more on the reader's intuition.  Given that, if you find yourself stumped by a section in the first article, look here for illumination. 

These class notes are a good follow up to those two articles.  I read them straight through up to page 13, when the S-combinator threw me for a bit of a loop.  I wanted to understand it a bit better before before moving on, so I stopped there and did a bit of further research before continuing.  This was a good thing, as the class notes have introduced Combinatory Logic without letting you know that they have veered from strict Lambda Calculus.

Let me talk about a newbie's view of the formulae in Lambda Calculus and in Combinatory Logic.  The S combinator is defined as S x y z = x z (y z).  This may be a bit confusing at first, it certainly was for me.  Even though I'm pretty handy with higher order functions in practice, and function composition seems as natural as can be, I still get thrown for a loop when I see an equation like this that doesn't make sense unless it's arguments are themselves functions (see the entries on "The Type of []" and "map map and Type-Wrangling"  for similar issues).  Useful exercise: with the definitions on pages 12 and 14 of the class notes, derive the equivalencies for fst and snd on the bottom of page 14. 
 
Maybe soon I can read Edward Yang's blog and get something out of it.