Free Variable

Definition

A free variable in an Expression is a variable that is not bound by any quantifier, lambda abstraction, or other binding construct within that expression.

A variable occurrence is free if it refers to a value from an enclosing context rather than being locally bound 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 $\forall x.P(x,y)$:

• $x$ is bound by the universal quantifier
• $y$ is free

In the expression $(x+3)\times z$:

• Both $x$ and $z$ are free (no binding constructs present)

Formal Definition

The set of free variables $\text{FV}(e)$ of an expression $e$ can be defined inductively:

• $\text{FV}(x)=\{x\}$ for a variable $x$
• $\text{FV}(\lambda x.e)=\text{FV}(e)\setminus \{x\}$
• $\text{FV}(e_1{e}_2)=\text{FV}(e_1)\cup \text{FV}(e_2)$

Closed Expressions

An expression with no free variables is called closed or a combinator. Closed expressions are self-contained and do not depend on any external context.

Substitution

Free variables are the targets of substitution. When substituting $a$ for $x$ in expression $e$, written $e[a/x]$, only the free occurrences of $x$ in $e$ are replaced.

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

Related Concepts

• Bound Variable: The dual concept, variables bound by quantifiers or abstractions
• Expression: The context in which variables appear
• Lambda Calculus: A formal system with explicit variable binding
• Substitution: The operation that replaces free variables
• Scope: The region where a variable binding is active