User loginNavigation |
archivesLambda Calculus NotationI 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? |
Browse archivesActive forum topics |
Recent comments
22 weeks 2 days ago
22 weeks 2 days ago
22 weeks 2 days ago
44 weeks 4 days ago
48 weeks 5 days ago
50 weeks 3 days ago
50 weeks 3 days ago
1 year 1 week ago
1 year 5 weeks ago
1 year 5 weeks ago