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?