Scope

What Is Scope?

The scope of λx in an expression λx.M is the body M. Every free occurrence of x inside M is bound by this λx.

Scope means: the region where a binding has effect. If an occurrence of x appears inside the body of λx, that λx is its binder. If it appears outside, this λx has no effect on it.

Scope Is the Body

In λx.M, the scope of λx is exactly the body M.

• The parameter x (between λ and .) is not "in the scope" -- it is the name the binding introduces.
• Anything outside the abstraction is not in the scope.
• Everything inside the body M is in the scope.

For example, in λx.x y, the scope of λx is x y. The x there is bound. The y is in scope but free (no λy encloses it).

Which Lambda Binds?

When an expression has multiple lambdas, each one binds occurrences of its parameter within its own body. To find which lambda binds a particular occurrence, look for the innermost enclosing λ whose parameter matches.

In λx.(λy.x y), the inner body is x y. The y is bound by the inner λy (the innermost matching binder). The x is bound by the outer λx -- there is no inner λx, so the outer one is the innermost matching binder.

Scope Boundary

The scope of λx ends at the boundary of its body. In an application like (λx.x) y, the body of λx is just x. The y sits outside the abstraction entirely -- it is the argument, not part of the body.

A variable occurrence outside the body is not bound by that lambda, even if it has the same name. In (λx.x) x, the first x (inside the body) is bound by λx, but the second x (the argument) is free -- it is outside the scope.

Identify the Binder

To find the binder of a variable occurrence, start at that occurrence and look outward. The first enclosing λ whose parameter matches the variable name is the binder.

If no enclosing λ matches, the occurrence is free.

Examples:

• In λx.λy.x, the x in the body is bound by the outer λx.
• In λx.λy.y, the y in the body is bound by the inner λy.
• In λy.x, the x is free -- no λx encloses it.

Scope Does Not Extend Left

The scope of λx extends only to the right -- into the body. A variable that appears to the left of a lambda is not inside its body and is not bound by it.

In x (λx.x), there are two occurrences of x:

• The first x is to the left of the λx. It is free.
• The second x is inside the body of λx. It is bound.

Sharing a name does not create a binding. Only being inside the body of the matching lambda does.

Multiple Binders

An expression can contain several lambdas with different parameter names. Each lambda binds only its own parameter, and only within its own body.

In λx.λy.x y:

• λx binds x in its body λy.x y
• λy binds y in its body x y
• The x in x y is bound by the outer λx
• The y in x y is bound by the inner λy

A lambda never binds a variable whose name differs from its parameter, regardless of how close the variable is to that lambda.

Scope and Free Variables

Being inside a lambda's body does not automatically make a variable bound. A variable is only bound if the enclosing lambda's parameter matches its name.

In λy.x, the occurrence of x is inside the body of λy. But λy binds y, not x. Since no λx encloses this occurrence, x is free -- even though it sits inside a lambda body.

Free means: no enclosing lambda binds this occurrence. It does not mean: outside all lambda bodies.