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?

It's not a term

The syntax for substitution (the square brackets in your example) are not part of the term language. Rather, they are part of the meta-language for working with terms. It is essential for you to understand this distinction, as it arises in many different contexts.

For example, we might want to introduce variables s, t, u ranging over terms. These are distinct from the variables a, b, c that occur in the language itself, and are only used in our description of the language.

Different authors have used a range of different conventions to distinguish meta-language syntax from language syntax. For instance, we might use an italic face for meta-language variables, which we use a monospace face for language variables. In some cases, they are indeed a bit sloppy, but usually it's clear enough. I rarely find myself confused.

Anyway, the substitution syntax is not part of the lambda calculus itself. As you study more semantics, this will hopefully become clearer.

By Matt Hellige at Mon, 2009-01-19 19:54 | login or register to post comments

More concrete

I realize that the above may be too abstract. For example, take a language like Java. When discussing Java programs, I might say something like, "Given any Java statement s..." Probably it's clear in this case that "s" is not a variable in Java itself, but only in my description of this Java program.

We can also define functions on language terms: "Given a Java method f, its xyz-closure XYZ(f) is a new method formed by adding new local variables for blah blah blah." XYZ is not a Java function, but rather a function in our meta-language for describing Java. Substitution in LC is this kind of function.

I hope this makes it clearer.

By Matt Hellige at Mon, 2009-01-19 19:59 | login or register to post comments

Given that all four books

Given that all four books (some of which are highly regarded) all define λ-term without the substitution notation, I was reasonably sure what you have written must be the case. However, the books don't really make it clear. Thank you for the reassurance.

I like the idea to "distinguish meta-language syntax from language syntax" and that actually prompted my question. As an exercise, I'm trying to write the shortest possible complete description of "classic lambda calculus" (just definitions and axioms). The mixture of actual λ-terms and meta-language notation around λ-terms and even injected in λ-terms in the books makes some things more ambiguous than I am accustom.

By Peter Michaux at Mon, 2009-01-19 20:17 | login or register to post comments

Read it as a postfix function/operator

You should read '_[_ := _]' as a substitution operator. It takes three arguments, all lambda terms, and the result is a lambda term.

x[x := N] â‰¡ N

So the equality is correct, substituting term 'N' for term 'x' in term 'x' is syntactically equal to the term 'N'.

Below is a definition:

x'[x := L] | x'  â‰¡ x     -> L
x'[x := L] | x' !â‰¡ x     -> x'

(M N)[x := L]            -> (M[x := L]) (N[x := L])  

(Î»x. M)[y := L] | x â‰¡ y  -> (Î»x. M)
(Î»x. M)[y := L] | x !â‰¡ y -> (Î»x. M[y := L])

[Btw. If you like this kind of stuff. Look here]

By marco at Mon, 2009-01-19 20:46 | login or register to post comments

Usually substitution is

Usually substitution is defined. You'll see a definition similar to the one marco gives above.

On a bit of a side note though, there are formalizations of the lambda calculus that do exactly what you suggest at the end of your original post, namely reify substitution into the language itself. These are usually called lambda calculi with explicit substitution and are used as they more closely model what actual implementations do.

By Derek Elkins at Mon, 2009-01-19 22:02 | login or register to post comments

Lambda the Ultimate

User login

Navigation