Lambda the Ultimate

I am diving into the world of lambda calculi by reading a few of the books that I've seen mentioned here on LtU. The books sensibly start with "classic lambda calculus". Even though each book uses a different terminology and notation, there seems to be a common inconsistency in the definition verses the use of "term" (a.k.a "expression", "lambda-term", "lambda-expression"). Being new to the formalism, I imagine there is a good chance the inconsistency is only perceived on my part.

In Chris Hankin's Lambda Calculi: A guide for computer scientists (1994), a "λ-term" is defined on page 8 by the following

  Definition 2.2 (λ-terms)
  The class Λ of λ-terms is the least class specifying the following
    (1) x ∈ Λ, x is a variable
    (2) if M ∈ Λ, then (λxM) ∈ Λ
    (3) if M, N ∈ Λ then (MN) ∈ Λ

Page 9 continues with more notation...

  We will generally use the symbol ≡ to denote 
  syntactic equality between terms.

It seems to me that the above is a relatively sloppy statement. The use of "generally" leaves me guessing later and "terms" was not defined as a synonym for "λ-terms". I understand this book is a relaxed introduction so I am not really nitpicking these points.

The inconsistency comes on page 15 when substitution is introduced.

  x[x := N] ≡ N

Definition 2.2 did not allow for square brackets indicating substitution to be part of a λ-term; however, from what I understand the ≡ symbol is to have a λ-term on each side.

To resolve this inconsistency it seems to me that Definition 2.2 needs to be extended.

    (4) if x, M, N ∈ Λ then M[x := N] ∈ Λ

I have used Hankin's book as my example above but the other books I am reading repeat this inconsistency: Revesz (1988), Hindley and Seldin (1986), Barendregt (1984).

Certainly something basic like this would have been noticed in the past if it was incorrect. What is it that I am missing here?

Are you interested in presenting a 45-minute talk on some Domain Specific Language (DSL) related topic? It doesn't matter which platform or OS you're targeting. It also doesn't matter whether you're an author, a vendor, a professional speaker or a developer in the trenches (in fact, I tend to be biased toward the latter). We're after interesting and unique applications of DSL technology and if you're doing good work in that area, then I need you to send me a session topic and 2-4 sentence abstract along with a little bit about yourself.

I'll be taking submissions 'til February 9th, 2009, but don't delay. Passion and a burning story to tell count twice as much as anything else.

And don't be shy about spreading this announcement around! I've got good coverage in the .NET and Windows communities, but don't know very many folks in the Java or Unix or hardcore modeling worlds, so if you're in that world, let those guys know! Thanks.

The DSL DevCon itself will be in Redmond, WA on the Microsoft campus April 16-17, 2009, right after the Lang.NET conference. Lang.NET will be focused on general-purpose languages, whereas the DSL DevCon will focus on domain-specific languages. The idea is that if you want to attend one or the other or both, that's totally fine. We'll have 2.5 days of Lang.NET on April 14-16 and then 1.5 days of DSL DevCon content. Oh, and the cost for both conferences is the same: $0.

We're only accepting 150 attendees to either conference. Every one of the five previous DevCons have sold out, so when we open registration, you'll want to be quick about getting your name on the list. Submit your DSL-related talk idea!