Lambda Calculus: Bad Definition of Scope?
I'm working through Davie's "Introduction to Functional Programming", and in chapter 5 he provides detailed recursive definitions of how to determine if a variable is free or bound in an expression. Here is the bound part (where ⇔ means "if and if only):
This makes sense. However, he also provides a definition of scope:
DEFN 5.3: The variable X is bound in [lambda expression] E as decided by the following cases:
a) if E is a variable then X is not bound in it.
b) if E is a combination E1 E2 then X is bound in E ⇔ X is bound in E1 or bound in E2
c) if E is an abstraction λY.E1 then X is bound in E ⇔ X ≡ Y or X is bound in E1.
While that definition makes intuitive sense, it leads me to some strange results in a case such as the following lambda expression (one given in the book):
DEFN 5.4: The scope of a bound variable is the entire λ-expression in which it occurs bound except for the text of any included abstractions whose bound variable is the same identifier.
If I use DEFN 5.3, I discover that variable x is bound in the entire lambda expression "(λx.x)(y z)" because the lambda expression is a combination, and according to part b, the variable is bound in a combination if the variable is bound in either of the sub-expressions. Thus, by DEFN 5.4, it must also be true that the scope of x is the entire λ-expression "(λx.x)(y z)". The problem of course with this understanding of his definition is that if x is bound in the entire λ-expression "(λx.x)(y z)" then, by DEFN 5.4, then x is not bound in "(λx.x)" because the definition states that "the scope of a bound variable is the entire λ-expression in which it occurs bound except for the text of any included abstractions whose bound variable is the same identifier".
So, I'm left without a precisely defined means of determining variable scope. Do you think I'm just failing to understand his definition (DEFN 5.4) properly, and/or do you think it needs to be reworded?
Re: Lambda Calculus: Bad Definition of Scope?
I agree with you. These definitions seem to be a little sloppy.
First, to be fully precise, one must talk about free or bound occurrences of a variable. A given occurrence of x is bound if it occurs under λx and is free otherwise. A less precise statement "x is free in E" means that there is a free occurrence of x in E, and similarly for bound. Note that one variable can have both free and bound occurrences in the same expression.
For a thorough account see "Lectures on the Curry-Howard Isomorphism," chapter 1. It even formally introduces alpha-equivalence (the renaming of bound variables) whereas most other sources just say informally that terms obtained from each other by the renaming of bound variables are identified. See also the classic text "Lambda Calculi with Types" by Henk Barendregt. If you need more textbook recommendations, let us know.