Variable

Definition

A variable is a syntactic placeholder that may appear as an atomic expression or as a named position inside a larger expression. In type theory, variables are the simplest terms from which more complex expressions are built.

In languages with binders, variable occurrences are interpreted relative to lexical scope: some occurrences are bound by an enclosing construct and others are free.

Variables in Type Theory

In type theory, variables appear in typing contexts and are assigned types. A typing judgment has the form:

$\Gamma ,x:A⊢e:B$

This states that under context $\Gamma$ extended with variable $x$ of type $A$, expression $e$ has type $B$.

Variable Operations

Key operations involving variables:

• Substitution: Replacing free occurrences of a variable with an expression, written $e[t/x]$
• Alpha Equivalence: Renaming bound variables, as in $\lambda x.e{\equiv }_{\alpha }\lambda y.e[y/x]$
• Scope: Determining which binding a variable occurrence refers to

Fresh Variables

A fresh variable is a variable name that does not appear in the current context or expression. Fresh variables are needed to avoid variable capture during Substitution or when applying alpha conversion.

Related Concepts

Lexical Scope
Structural Substitution
Expression
Lambda Calculus
Type Theory