Results 1 to 2 of 2

Math Help - Lambda Calculus: Bad Definition of Scope?

  1. #1
    Member
    Joined
    Aug 2011
    Posts
    76
    Thanks
    1

    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):

    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.
    This makes sense. However, he also provides a definition of scope:

    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.
    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):

    (λx.x)(y z)

    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?
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,537
    Thanks
    778

    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.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 1
    Last Post: September 15th 2011, 07:35 AM
  2. [SOLVED] Eigenvalues of y''+2y'+\lambda y=0
    Posted in the Differential Equations Forum
    Replies: 11
    Last Post: February 26th 2011, 05:46 PM
  3. The scope/limitation of logab X
    Posted in the Pre-Calculus Forum
    Replies: 3
    Last Post: November 24th 2009, 04:12 AM
  4. Lambda calculus
    Posted in the Calculus Forum
    Replies: 3
    Last Post: February 13th 2009, 09:02 PM
  5. show that V(X) = lambda
    Posted in the Advanced Statistics Forum
    Replies: 3
    Last Post: January 11th 2009, 03:50 AM

Search Tags


/mathhelpforum @mathhelpforum