archives

Lambda Calculus Notation

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?