Variable

Definition

A variable is a symbolic name that stands for a value or represents an unknown in mathematical expressions and programs. In Type Theory, variables are the most basic form of Expression, serving as placeholders that can be bound, substituted, or left free.

Types of Variables

Variables can be classified by their binding status.

Free Variables

A Free Variable is a variable that is not bound by any binding construct within an expression. Free variables refer to values from an enclosing context.

In $\lambda x.x+y$, the variable $y$ is free.

Bound Variables

A Bound Variable is a variable whose scope is limited by a binding construct such as a lambda abstraction or quantifier.

In $\lambda x.x+y$, the variable $x$ is bound.

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 reference 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

• Free Variable: Variables not bound in an expression
• Bound Variable: Variables bound by abstraction or quantification
• Substitution: The operation of replacing variables
• Scope: The region where a variable binding is active
• Expression: The context in which variables appear
• Lambda Calculus: A formal system built on variables and abstraction
• Type Theory: Framework assigning types to variables