The Untyped Lambda Calculus: Where It All Begins

  • November 21, 2013 · 7:00 PM
  • Mixrank

Tikhon Jelvis presents the untyped lambda calculus.


The rules describing the untyped lambda calculus are absurdly simple. But those rules not only lead to a rich and fascinating field of study, they are also the metaphor in which we nearly always think about computation. You already use the lambda calculus every day, even if you don't know it.

Join or login to comment.

  • Sergei W.

    Two belated comments:

    1) I just found out that De Bruijn died in 2012 (amazing, to me - when I first read about De Bruijn indices, he was still alive...).

    2) R. Harper's short paper about translating classical logic into lambda-calculus with call/cc, but explained much more cleanly: http://www.cs.cmu.edu/~rwh/courses/logic/www/handouts/class.pdf

    April 17

  • Christopher B.

    There are video tutorials on Coq and Agda as well as lectures by Benjamin Pierce and Anrew Tolmach on parts of Software Foundations on the web pages for Oregen PL summer school years 2010 - 2013:

    http://www.cs.uoregon.edu/research/summerschool/summer10/curriculum.html
    http://www.cs.uoregon.edu/research/summerschool/summer11/curriculum.html
    http://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html
    http://www.cs.uoregon.edu/research/summerschool/summer13/curriculum.html

    November 21, 2013

    • Sergei W.

      There is far too much to see! Maybe someone could point us to the videos that are more relevant to type theory / theorem proving / lambda-calculus... Or actually we could also have a meetup about some of those videos, how's that?

      November 22, 2013

    • Adrian K.

      Sounds good to me. We might want to have a few meetups on the basics first, though, as a lot of the Oregon videos look rather sophisticated.

      November 22, 2013

  • Adrian K.

    If you want a reference on De Bruijn indices, which I mentioned as an alternative notation for the lambda calculus that does not require messing with variable names, the Wikipedia article (http://en.wikipedia.org/wiki/De_Bruijn_index) offers a pretty clear and concise explanation.

    November 22, 2013

  • Tikhon J.

    The slides are available on my site at http://jelv.is/untyped-lambda-calculus.html. The talk wasn't recorded, unfortunately. I'll fix the bugs in the slides in a bit.

    November 22, 2013

  • Byron H.

    Sorry, I timed out on getting there.

    November 21, 2013

  • Christopher B.

    May not be able to make it tonight, to my regret.

    November 21, 2013

  • Adrian K.

    Both the Coq books I mentioned (Pierce et al and Chilpala) claim that no advanced knowledge of type theory is actually needed to get started with Coq, so I'm not sure I'd want to take a long detour through type theory before starting to look at what I'm *really* interested in.

    That said, this seems to have become a big enough group that perhaps we can do more than one thing at a time.

    November 5, 2013

    • Adrian K.

      F* sounds as if it would be interesting to explore along with other things along the border between language and automated proof system, like Agda and Idris.

      November 20, 2013

    • Christopher B.

      Have been monitoring F* from a distance for a while. What I've seen of the syntax looks nice and clear, more in the vein of a familiar FP language than Agda or certainly than Coq. F* and Idris seem relatively closest to familiar FP on the FP-to-interactive theorem prover spectrum, with Agda somewhere in the middle and Coq (in you basically develop natural deduction proofs from which Ocaml code can be extracted) furthest toward the theorem proving end.

      November 21, 2013

  • Manoj K.

    I am going through the lectures on ML programming language. Will that be sufficient to understand the session's content?

    November 20, 2013

    • Adrian K.

      I can't speak to how fancy Tikhon is planning to get, but the rules for ML are a lot more complicated than the rules for the lambda calculus. So you should be well prepared.

      November 20, 2013

    • Tikhon J.

      More than enough. Mostly, it won't be about programming. There will be a little bit of code, but it will only use an algebraic data type and simple pattern matching--I believe that even somebody without functional programming experience should be able to follow along.

      November 20, 2013

  • Adrian K.

    Is there a videographer in the house?

    November 19, 2013

  • Manoj K.

    If possible, please keep the first session just an informal introduction with lots of q/a so beginners like me can get started.

    November 16, 2013

  • Dave D.

    I figured I double booked against something I can't get out of.

    In the meantime, any reading material?

    November 16, 2013

  • Tikhon J.

    Okay, I have a location and a time: Mixrank's office, next Thursday. I also have a good idea for a topic: basically everything about the untyped lambda calculus. I want to talk about the theory, implement an interpreter and talk about how to actually use the it. This will require a tiny bit of background--just basic functional programming with algebraic data types. I'll put up a few exercises or some suggested reading or something in a bit.

    How does that sound to everybody?

    1 · November 14, 2013

    • Byron H.

      I keep hearing about the (untyped) lambda calculus, but have never experienced its exposition. This talk sounds like a good idea.

      November 14, 2013

    • Jeremy H.

      Aw, dammit, that's the night I'm speaking at another meetup. What excessively bad luck.

      November 15, 2013

  • Jack F.

    Bummer, I'm going to be returning from the MVP Summit at this time. See you next time.

    November 14, 2013

  • Tikhon Jelvis changed the location for this Meetup

    November 14, 2013

  • Tikhon Jelvis changed the date and time to Thursday, November 21, 2013 at 7:00 PM

    November 14, 2013

  • Adrian K.

    Conicidentally, the exercise this week for Dan Grossman's Programming Languages course on Coursera (https://class.coursera.org/proglang-002/class) is writing an interpreter for a simple Lisp-like language -- covering everything you'd need in a simple interpretation of the untyped lambda calculus, although without ever saying "lambda calculus".

    November 11, 2013

  • Adrian K.

    If we're focusing on Simply Easy, one approach might be to devote the first session to the simply typed lambda calculus, following the layout of the paper (maybe bring a translation of the interpreter presented in the paper to your favorite language, or a small program in the simply typed lambda calculus that runs under the paper's interpreter). The next session(s?) could expand on that to the dependently typed lambda calculus. But if we're focusing on just this paper, we should probably change the title of the meeting ("Type Theory Overview" sounds intimidatingly broad to me).

    November 8, 2013

    • Sergei W.

      "Type theory overview" was the first thing that came to my mind, and the exercise currently proposed (building an interpreter for a simply typed lambda calculus) could be viewed as the first step in re-visiting type theory. Unfortunately, the format of meetup.com requires us to put all our comments under a meetup proposal. So perhaps we need another meetup proposal, more narrowly titled, and then we can rsvp and discuss there?

      November 8, 2013

    • Adrian K.

      It appears that Meetup actually lets me (lets anyone?) change a meetup title. Perhaps to "Lambda Calculus Smackdown: Simply Typed vs. Dependently Typed"?

      1 · November 8, 2013

  • Tikhon J.

    I think an overview of the lambda calculus as well as a few typed lambda calculi would be very useful. I'm imagining something like a quick overview of operational semantics, the untyped lambda calculus, type inference rules, the simply typed lambda calculus and a few variations (like system F).

    One really nice thing is that all these different lambda calculi are very easy to implement, so this could be a very hands-on lesson. I believe that going from a set of inference rules to an implementation is a great way to understand these concepts.

    All these topics are reasonably simple, but the course I took split them into several lectures--maybe covering everything in one go is too ambitious. I do think an overview like this could be very useful, especially if people do not know much about type theory.

    November 7, 2013

    • Tikhon J.

      I had a few exercises similar to the paper in mind--the paper itself is too dense for a good introduction, but I think I can adapt part of it to be much more accessible. As far as languages go, what I'm imagining is actually fairly limited--it would look identical in Haskell/OCaml/SML/F# and very similar (but uglier) in Scala. It turns out that for implementing the basic lambda calculus, all you need are really basic FP constructs.

      November 8, 2013

    • Tikhon J.

      I really don't think we need to worry about weeding people out. The programming I'm thinking about is important but relatively simple and secondary to understanding the theory. As far as language choice goes, I think Haskell is reasonable especially since we won't need to get into monads or anything like that. Compared to the alternatives, Scala would be a bit awkward syntactically. Haskell, OCaml, SML and F# would be about equal; out of those, I think Haskell is the best option because it's reasonably easy to install on any platform. OCaml on Windows is a nightmare, F# not on windows might be a pain and SML is annoying everywhere.

      November 8, 2013

20 went

Create your own Meetup Group

Get started Learn more
Henry

I decided to start Reno Motorcycle Riders Group because I wanted to be part of a group of people who enjoyed my passion... I was excited and nervous. Our group has grown by leaps and bounds. I never thought it would be this big.

Henry, started Reno Motorcycle Riders

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy