132
$\begingroup$

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus?

Specifically, I am interested in the following areas:

  • Untyped lambda calculus
  • Simply-typed lambda calculus
  • Other typed lambda calculi
  • Church's Theory of Types (I'm not sure where this fits in).

(As I understand, this should provide a solid basis for the understanding of type theory.)

Any advice and suggestions would be appreciated.

$\endgroup$

9 Answers 9

Reset to default
86
$\begingroup$

alligators

Alligator Eggs is a cool way to learn lambda calculus.

Also learning functional programming languages like Scheme, Haskell etc. will be added fun.

$\endgroup$
4
  • $\begingroup$ Hah, looks pretty funny. Maybe not the in-depth tutorial I'm looking for, but will have to check it out! $\endgroup$
    – Noldorin
    Aug 4, 2010 at 13:18
  • 4
    $\begingroup$ Looks really fun! I can use this to teach kids. $\endgroup$
    – Chao Xu
    Aug 4, 2010 at 13:41
  • 3
    $\begingroup$ Now that I call a nice model of lambda calculus! I wonder what Dana Scott has to say about this ;-) $\endgroup$
    – fgp
    May 27, 2013 at 14:10
  • 3
    $\begingroup$ Alligator Eggs may be a cool way to teach it, but the site assumes you already have knowledge and you're trying to teach it to others who don't. $\endgroup$
    – zumalifeguard
    Jul 21, 2018 at 1:55
48
$\begingroup$

Recommendations:

  1. Barendregt & Barendsen, 1998, Introduction to lambda-calculus;
  2. Girard, Lafont & Taylor, 1987, Proofs and Types;
  3. Sørenson & Urzyczyn, 1999, Lectures on the Curry-Howard Isomorphism.

All of these are mentioned in the LtU Getting Started thread.

$\endgroup$
6
  • 1
    $\begingroup$ Thanks again Charles, that looks like good material. $\endgroup$
    – Noldorin
    Jul 30, 2010 at 8:21
  • $\begingroup$ Out of curiosity, will learning simply and then more advanced typed versions of lambda calculus give me a pretty good coverage of the field of type theory? $\endgroup$
    – Noldorin
    Jul 30, 2010 at 14:23
  • 3
    $\begingroup$ Haha, only 7 years eh... better late than never, as they say! I've learnt a lot since then, but thank you. $\endgroup$
    – Noldorin
    Mar 17, 2017 at 21:40
  • 1
    $\begingroup$ @Noldorin You could write up your own answer to this question, maybe? $\endgroup$
    – Charles Stewart
    Mar 19, 2017 at 11:16
  • 1
    $\begingroup$ I'm still by no means an expert in this field. I don't think I could add much, to be honest. :) $\endgroup$
    – Noldorin
    Mar 20, 2017 at 4:30
40
$\begingroup$

Here are a couple of resources that will get you started:

  1. The Lambda Calculus, Its Syntax and Semantics - This is a must!

  2. Lecture Notes on the Lambda Calculus by Peter Selinger

  3. History of Lambda Calculi

  4. Impact of Lambda Calculus on Logic and Computer Science

  5. Introduction to Lambda Calculus

  6. Lambda Calculi with Types

  7. Tutorial Introduction to Lambda Calculus

  8. Call-by-name, call-by-value and the Lambda Calculus

  9. Control operators, the SECD-machine, and
    the lambda-calculus.     - With effects

  10. Modified basic functionality in combinatory logic- H.B. Curry.

  11. The principal type scheme of an object in combinatory logic. - J. Roger Hindley.

Since I am a computer science graduate, most of these are geared towards computer scientists rather than logicians.

Bonus : There is a new book that has come out Semantics Engineering with PLT Redex. I haven't read it but people have told me good things about it.

I hope this helps. Please feel free to ask me any questions. Thanks.

$\endgroup$
1
  • 3
    $\begingroup$ I believe that the book by Henk P. Barendregt “The Lambda Calculus, Its Syntax and Semantics” is too formal to be useful as a first textbook to learn lambda calculus. I think it is more a reference book for people working in related fields. $\endgroup$
    – Vitaly Olegovitch
    Jun 1, 2014 at 18:00
18
$\begingroup$

I like Type Theory and Functional Programming by Simon Thompson.

$\endgroup$
12
$\begingroup$

It might be nice to work through Structure and Interpretation of Computer Programs, which is available online for free. This book is an introduction to computer science and the programming language Scheme, which is a flavor of the programming language Lisp, which is based on the lambda calculus. Although it is not strictly a book about the lambda calculus, it might be fun or useful to gain some hands-on and "practical" experience with the lambda calculus by reading some of this book and working through some of its exercises.

$\endgroup$
4
  • 1
    $\begingroup$ Thanks for the tip. I'm sure you're right in saying that it will provide an insight, though I am perhaps looking for a more theoretical approach (as Alonzo Church originally formulated it). I have some active experience in F# which should provide a basis. $\endgroup$
    – Noldorin
    Jul 28, 2010 at 15:48
  • 9
    $\begingroup$ This won't help much with understanding types. $\endgroup$
    – Charles Stewart
    Jul 28, 2010 at 21:06
  • 1
    $\begingroup$ @CharlesStewart I'm responding to your old comment, because I guess with the number of upvotes the original question makes for a good reference question, and your comment somehow has a rating of 7. The question indicates an interest in untyped lambda calculus, so I don't see how your comment is relevant. $\endgroup$
    – Doug Spoonwood
    Nov 5, 2016 at 14:35
  • 2
    $\begingroup$ @DougSpoonwood Untyped lambda calculus is just one thing the question asks for. Mostly the question is after information about typed lambda calculus. $\endgroup$
    – Charles Stewart
    Dec 8, 2016 at 11:55
10
$\begingroup$

Lambda-Calculus and Combinators, an Introduction by J. ROGER HINDLEY and JONATHAN P. SELDIN is a great (and relatively modern) resource that doesn't assume any previous knowledge.

It is available online here.

$\endgroup$
10
$\begingroup$

lol

To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction by David C Keenan is a nice complement to Alligator Eggs given above. Keenan uses Smullyan's bird metaphors from To Mock a Mockingbird and augments them with diagram notation, which aids in building intuition around combinators. The above is Y combinator in Keenan's notation.

$\endgroup$
5
$\begingroup$

I found this iPhone app that works as an un-typed lambda calculator, it works with successor, addition, addition with successor, multiplication, exponentiation, predecessor and subtraction operations. It shows a step by step process which might be helpful for people who are just starting with lambda calculus.

link: https://itunes.apple.com/WebObjects/MZStore.woa/wa/viewSoftware?id=928503408&mt=8

$\endgroup$
3
$\begingroup$

Some time ago, I was surprised not to find many untyped & simply-typed lambda calculus interpreters among the answers to this question, so I started working for a while in an educational lambda calculus interpreter called Mikrokosmos (can also be used online). It implements untyped and simply typed lambda calculus (and also illustrates Curry-Howard).

Surely, you could also use some functional programming language; but at least for me, it was difficult to determine exactly which constructs of the language are lambda calculus and which are extras offered by that particular language. Haskell for instance approximately implements System-F, but I also wanted to have a simply(as simple as possible)-typed lambda calculus interpreter.

The interpreter is free software and you can integrate them on other learning materials (such as Jupyter notebooks or web pages). I have used it before to teach lambda calculus to CS students.

Please note that I am the main developer of this interpreter. I am only posting here because this same question inspired me to start the development.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .