User loginNavigation 
Lambda 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", "lambdaterm", "lambdaexpression"). 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? By Peter Michaux at 20090119 19:34  LtU Forum  previous forum topic  next forum topic  other blogs  5424 reads

Browse archivesActive forum topics 
Recent comments
6 hours 41 sec ago
8 hours 20 sec ago
13 hours 54 min ago
1 day 6 hours ago
1 day 15 hours ago
2 days 2 hours ago
2 days 3 hours ago
2 days 3 hours ago
2 days 4 hours ago
2 days 5 hours ago