Expression

Definition

An expression (or term) is a syntactic construct in a formal language that can be evaluated or reduced to a value. In Type Theory and programming languages, expressions are the basic units of computation.

Components

Expressions are typically built from:

• Variables: $x$, $y$, $z$
• Constants: $0$, $\text{true}$, $\text{nil}$
• Applications: $f(x)$, $e_1{e}_2$
• Abstractions: $\lambda x.e$
• Constructors: $(a,b)$, $\text{inl}(a)$

Classification

Expressions can be classified by their structure:

• Closed expressions: Contain no free variables
• Open expressions: Contain free variables
• Well-typed expressions: Have a valid type in a given context
• Normal forms: Cannot be reduced further

Typing

In typed languages, expressions are assigned types. A typing judgment has the form:

$\Gamma ⊢e:T$

This states that in context $\Gamma$, expression $e$ has type $T$.

Evaluation

Expressions are evaluated according to reduction rules:

• β-reduction: $(\lambda x.e)(a)\to e[a/x]$
• η-expansion: $f\to \lambda x.f(x)$
• Pattern matching and case analysis

Related Concepts

• Free Variable: Variables not bound in an expression
• Type Theory: The formal system for typed expressions
• Lambda Calculus: The foundational calculus of expressions
• Function Type: Types of function expressions
• Computation Rule: Rules for evaluating expressions