Bound Variable

Definition

A bound variable in an Expression is a variable whose scope is limited by a binding construct such as a lambda abstraction, quantifier, or other binder within that expression.

A variable is bound if it is introduced and given meaning by a construct like $\lambda x$, $\forall x$, $\exists x$, or ${\Pi }_{x:A}$ within the expression.

Examples

In the expression $\lambda x.x+y$:

• $x$ is bound by the lambda abstraction
• $y$ is free (not bound within this expression)

In the expression ${\Pi }_{x:A}B(x)$:

• $x$ is bound by the dependent product
• $x$ may appear free in $B(x)$, but is bound in the overall expression

In the expression $\lambda f.\lambda x.f(x)$:

• $f$ is bound by the outer lambda
• $x$ is bound by the inner lambda
• Both bindings create nested scopes

Binding Constructs

Common binding constructs in Type Theory:

• Lambda abstraction: $\lambda x.e$ binds $x$ in $e$
• Dependent product: ${\Pi }_{x:A}B(x)$ binds $x$ in $B(x)$
• Dependent sum: ${\Sigma }_{x:A}B(x)$ binds $x$ in $B(x)$
• Universal quantification: $\forall x:A.P(x)$ binds $x$ in $P(x)$
• Existential quantification: $\exists x:A.P(x)$ binds $x$ in $P(x)$
• Let expressions: $\text{let }x=e_1\text{ in }{e}_2$ binds $x$ in $e_2$

Scope

The Scope of a bound variable is the region of the expression where the binding is active. Variables can be shadowed when inner bindings use the same name as outer bindings.

In $\lambda x.(\lambda x.x+1)+x$:

• The inner $\lambda x$ shadows the outer binding
• The first occurrence of $x$ in $(x+1)$ refers to the inner binding
• The final $x$ refers to the outer binding

Alpha Equivalence

Bound variables can be renamed consistently without changing the meaning of an expression. This property is called alpha equivalence:

$\lambda x.e{\equiv }_{\alpha }\lambda y.e[y/x]$

provided $y$ does not appear free in $e$. For example, $\lambda x.x{\equiv }_{\alpha }\lambda y.y$.

Relationship to Substitution

Substitution only affects free variables. When substituting $a$ for $x$ in $\lambda x.e$, the bound $x$ is not replaced. This is why $(\lambda x.x)[a/x]=\lambda x.x$, not $\lambda a.a$.

Care must be taken during substitution to avoid variable capture, where a free variable would incorrectly become bound.

Related Concepts

• Free Variable: The dual concept, variables not bound in an expression
• Scope: The region where a variable binding is active
• Substitution: Operation that replaces free variables while respecting bindings
• Lambda Calculus: Formal system with explicit variable binding
• Expression: The context in which variables appear
• Dependent Product: A type with variable binding