Scope

Definition

In Type Theory and programming languages, the scope of a variable binding is the region of an Expression where that binding is active and the variable can be referenced.

Scope determines which bindings are visible at each point in a program and how variable names are resolved.

Lexical Scope

Most type theories use lexical scope (or static scope), where the scope of a binding is determined by the syntactic structure of the expression.

In lexical scope, a variable refers to the nearest enclosing binding in the program text.

Scope in Lambda Calculus

In the expression $\lambda x.e$, the scope of the binding for $x$ is the body $e$. Within $e$, occurrences of $x$ refer to the lambda-bound variable.

Example: In $\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 expression $x+y$

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

Scope in Dependent Types

In dependent types, scope becomes more complex because types can depend on values.

In a Dependent Product ${\Pi }_{x:A}B(x)$, the variable $x$ is in scope in the type expression $B(x)$.

In a Dependent Pair ${\Sigma }_{x:A}B(x)$, the variable $x$ is similarly in scope in $B(x)$.

Scope and Typing Context

In type theory, scope is formalized through the typing context $\Gamma$. The judgment:

$\Gamma ⊢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.

Fresh Variables

When performing operations like Substitution or α-conversion, it is often necessary to choose fresh variables—names that are not already in scope—to avoid unintended variable capture.

Related Concepts

• Bound Variable: Variables whose scope is determined by a binding construct
• Free Variable: Variables that appear outside the scope of their binding
• Substitution: An operation that must respect scope to avoid variable capture
• Lambda Calculus: The foundational system with explicit scoping rules
• Expression: The context in which scope is determined
• Type Theory: The formal system using scope and contexts