Definition
Lexical scope is the discipline by which the meaning of a variable occurrence is determined by the surrounding syntax of an expression. A variable occurrence refers to the nearest enclosing binding construct in the program text.
Most type theories use lexical scope, also called static scope, rather than a dynamic notion of name resolution.
Bound and Free Variables
An occurrence of a variable is bound when it lies inside the scope of a binder that introduces that variable. An occurrence is free when no enclosing binder in the expression binds it.
- In , the occurrence of is bound and the occurrence of is free.
- In , the binder introduces and its scope is the family .
- An expression with no free variables is closed.
The set of free variables may be defined inductively by
\text{FV}(x) &= \{x\} \\ \text{FV}(e_1\,e_2) &= \text{FV}(e_1) \cup \text{FV}(e_2) \\ \text{FV}(\lambda x. e) &= \text{FV}(e) \setminus \{x\} \end{aligned}$$ ## Binding Constructs Common binding constructs include: - Lambda abstraction: $\lambda x. e$ - Dependent product: $(x:A) \to B(x)$ - Dependent sum: $(x:A) \times B(x)$ - Universal quantification: $\forall x : A. P(x)$ - Existential quantification: $\exists x : A. P(x)$ - Let expressions: $\text{let } x = e_1 \text{ in } e_2$ ## Scope in Lambda Calculus In the [[Expression|expression]] $\lambda x. e$, the scope of the binding for $x$ is the body $e$. Within $e$, occurrences of $x$ refer to that lambda-bound variable. Example: In $e:=\lambda x. (\lambda y. x + y)$: - The scope of the outer $x$ binding is $(\lambda y. x + y)$ - The scope of the $y$ binding is $x + y$ - Both bindings are active in the subexpression $x + y$ of $e$ ## Shadowing When a variable is bound in a scope that already contains a binding for the same name, the inner binding *shadows* the outer one. Example: In $\lambda x. (\lambda x. x + 1)$: - The inner $\lambda x$ shadows the outer binding - Within $x + 1$, the name $x$ refers to the inner binding - The outer binding is temporarily hidden but not destroyed ## Context and Freshness In [[Type Theory|type theory]], scope is tracked by the typing context $\Gamma$. The judgment: $$\Gamma \vdash e : T$$ states that $e$ has type $T$ under context $\Gamma$, which lists all variables in scope and their types. Extending the context with a new binding is written $\Gamma, x : A$, bringing $x$ into scope for subsequent judgments. When performing operations like [[Structural Substitution|substitution]] or [[Alpha Equivalence|alpha conversion]], it is often necessary to choose a *fresh variable*, namely a name that is not already in scope. Freshness matters because careless substitution can cause variable capture. ## Representing Scoped Syntax Four common approaches to syntax with binders are: - [[Nameful Scoping]]: Keep variable names explicitly and identify terms up to [[Alpha Equivalence|alpha equivalence]]. - [[De Bruijn Indices]]: Replace names with numbers that count enclosing binders. - [[Higher-Order Abstract Syntax]]: Reuse binding in a meta-language to represent binding in the object language. - [[Nominal Sets]]: Keep names while treating permutations and freshness as primitive structure. These approaches solve the same basic problem in different ways: how to represent binding, renaming, and substitution without losing the intended lexical structure. ## Related Concepts [[Variable]] [[Structural Substitution]] [[Alpha Equivalence]] [[Lambda Calculus]] [[Expression]] [[Context (Type Theory)]]