Evaluation and Reduction of Expressions

An expression is a syntactic term built from literals, variables, operators, and constructs like conditionals, `let`-bindings, and function applications. Formally, expressions form a tree — the abstract syntax tree (AST) — and evaluation is a function from (expression, environment) pairs to values. An environment `ρ` (rho) is a partial function from variable names to values, typically implemented as a chain of frames (see Environments); it supplies meanings for the free variables that occur inside the expression being evaluated. A value is a piece of syntax (or a semantic object) that requires no further evaluation: an integer literal like `7`, a boolean `true`, a closure representing a function, or a constructed data value. Crucially, values are a subset of expressions — every value is trivially "already evaluated." The evaluation relation therefore partitions all well-formed expressions into values (already done) and non-values (which contain at least one redex, a reducible sub-expression such as `2 + 3` or `(λx. e) v`, that some rule tells us how to simplify). There are two standard, and provably equivalent, styles for specifying this process. Big-step (natural) semantics writes judgments of the form ``` ρ ⊢ e ⇓ v ``` read "under environment `ρ`, expression `e` evaluates to value `v`," and defines this judgment by structural rules that go straight from an expression to its final value — exactly how a recursive `eval` function is coded. Small-step (structural operational) semantics instead writes ``` e / ρ → e' / ρ' ``` read "one step of computation rewrites `e` (with environment `ρ`) to `e'` (with possibly updated `ρ'`)," and defines evaluation as the reflexive-transitive closure `→*` of this single-step relation, terminating when `e'` is a value. Small-step semantics exposes intermediate configurations — essential for reasoning about non-termination, concurrency, and reduction order — while big-step semantics is closer to an implementer's intuition and more concise for languages without those subtleties. Both are used throughout the study of Expressions and Statements and both agree on the final value whenever evaluation terminates deterministically.

The syntax being evaluated

A minimal expression language, enough to illustrate every mechanism, has this grammar: ``` e ::= n -- integer literal | x -- variable | e1 op e2 -- binary operator (+, -, *, ==, <, ...) | if e1 then e2 else e3 -- conditional | let x = e1 in e2 -- local binding | λx. e -- function (lambda abstraction) | e1 e2 -- application ``` Values `v` are the literals `n`, booleans, and closures `⟨λx. e, ρ⟩` — a function paired with the environment in which it was created (this pairing is what makes Environments essential to functions, not just to variable lookup).

Big-step evaluation rules

The judgment `ρ ⊢ e ⇓ v` is defined inductively on the structure of `e`: ``` [Lit] ρ ⊢ n ⇓ n [Var] ρ(x) = v ───────────── ρ ⊢ x ⇓ v [Op] ρ ⊢ e1 ⇓ n1 ρ ⊢ e2 ⇓ n2 n = n1 op n2 ────────────────────────────────────────── ρ ⊢ e1 op e2 ⇓ n [If-T] ρ ⊢ e1 ⇓ true ρ ⊢ e2 ⇓ v ────────────────────────────── ρ ⊢ if e1 then e2 else e3 ⇓ v [If-F] ρ ⊢ e1 ⇓ false ρ ⊢ e3 ⇓ v ────────────────────────────── ρ ⊢ if e1 then e2 else e3 ⇓ v [Let] ρ ⊢ e1 ⇓ v1 ρ[x ↦ v1] ⊢ e2 ⇓ v2 ───────────────────────────────────── ρ ⊢ let x = e1 in e2 ⇓ v2 [Lam] ρ ⊢ λx. e ⇓ ⟨λx. e, ρ⟩ [App] ρ ⊢ e1 ⇓ ⟨λx. e, ρ'⟩ ρ ⊢ e2 ⇓ v2 ρ'[x ↦ v2] ⊢ e ⇓ v ─────────────────────────────────────────────────────────── ρ ⊢ e1 e2 ⇓ v ``` Each rule has premises above the line and a conclusion below; a derivation is a finite tree built from these rules that proves a specific evaluation. Note `[App]` evaluates the function's body in the closure's environment `ρ'` extended with the argument, not in the caller's environment — this is exactly the lexical scoping discipline that gives environments their well-defined meaning.

Small-step reduction rules

The same language, one step at a time, using evaluation contexts `E` to pin down exactly where the next redex is: ``` E ::= [] | E op e | v op E | if E then e2 else e3 | let x = E in e2 | E e2 | v E ``` A single global rule plugs a redex into a context: ``` [Ctx] e → e' ──────────────── E[e] → E[e'] ``` and the base reduction rules contract the innermost redex found by the grammar of `E`: ``` n1 op n2 → n where n = n1 op n2 if true then e2 else e3 → e2 if false then e2 else e3 → e3 let x = v in e2 → e2[x ↦ v] (or: extend ρ, see below) (λx. e) v → e[x ↦ v] (β-reduction, substitution form) ``` In the environment-passing formulation (matching the big-step rules above), substitution `e[x ↦ v]` is replaced by environment extension `ρ[x ↦ v]`, avoiding the cost of textual substitution — this is the standard implementation choice and is discussed further as the mechanism behind Evaluation Strategies: Call-by-Value, Name, and Need.

The `eval` algorithm

Here is the big-step rules turned directly into a recursive interpreter — this is the algorithm real interpreters run: ``` function eval(e, ρ): match e: case Lit(n): return n case Var(x): if x in ρ: return ρ[x] else: error "unbound variable: x" case BinOp(op, e1, e2): v1 = eval(e1, ρ) v2 = eval(e2, ρ) if not (isNumber(v1) and isNumber(v2)): error "type error in operator" return applyOp(op, v1, v2) case If(e1, e2, e3): v1 = eval(e1, ρ) if v1 == true: return eval(e2, ρ) else if v1 == false: return eval(e3, ρ) else: error "condition is not boolean" case Let(x, e1, e2): v1 = eval(e1, ρ) ρ' = extend(ρ, x, v1) return eval(e2, ρ') case Lambda(x, body): return Closure(x, body, ρ) -- captures ρ NOW case App(e1, e2): f = eval(e1, ρ) a = eval(e2, ρ) if not isClosure(f): error "applying a non-function" (x, body, ρcap) = unpackClosure(f) ρ'' = extend(ρcap, x, a) return eval(body, ρ'') -- body runs in CAPTURED env ``` Base cases are `Lit` and the lookup branch of `Var`; every other case is defined by recursive calls to `eval` on strictly smaller sub-expressions, guaranteeing termination of the algorithm on any finite AST, whatever the language's own halting behavior may be (a program can still loop forever via recursive functions — that non-termination lives inside the recursive call in `App`, not in the structural recursion of `eval` itself).

Reduction as a graph

The figure below shows one full big-step derivation for `let x = 5 in x * x + 3`, displayed as the recursive call tree that `eval` actually walks, alongside the environment frame it builds.

Time complexity. For an expression AST with `n` nodes and an environment implemented as a hash map or association list, each `eval` case does O(1) work (a lookup, an arithmetic operation, an environment extension) besides its recursive calls. Since `eval` recurses exactly once per child edge of the AST and every node is visited at most once per evaluation path actually taken, evaluating a straight-line expression (no functions, no loops) costs O(n) time and O(d) auxiliary stack space, where `d` is the AST's depth (from the call stack of recursive `eval` invocations). If the environment is a linked chain of frames rather than a flat array, variable lookup costs O(k) where `k` is the lexical nesting depth to the binding site, adding at most an O(k) factor per `Var` node — still linear overall for programs with bounded nesting, and this is the standard reason production interpreters prefer array-indexed "de Bruijn" environments over chains once performance matters. For a language with recursive functions (`App` calling into user-defined recursive closures), there is no finite bound on the number of `eval` invocations — the interpreter's recursion can outlive the program's static AST size, exactly mirroring the fact that the source language itself need not terminate. This is not a flaw in the algorithm; it is the expected, unavoidable consequence of Turing-completeness (no algorithm can decide termination in general — the halting problem), and the evaluator's job is only to compute the right answer when the program terminates.

Space complexity. Big-step evaluation as written is a direct recursive-descent interpreter, so its space cost is the call-stack depth, O(d) for straight-line code and O(recursion depth) for recursive programs — the same asymptotic shape as any recursive function evaluator, and the reason deeply recursive, non-tail-recursive source programs can overflow the interpreter's native stack even though the source language has no explicit stack notion.

Correctness. Three properties are what "correct" means for an evaluator, and each has a clean argument: 1. Determinism. For every expression `e` and environment `ρ`, there is at most one `v` with `ρ ⊢ e ⇓ v`. Proof sketch: induction on the structure of the big-step derivation. Every rule's conclusion is syntactically keyed to one AST constructor (`[Lit]` only concludes about literals, `[Op]` only about binary operators, etc.), so at most one rule can apply to any given `e`; each rule's premises are themselves unique evaluations of strictly smaller sub-expressions, which are unique by the induction hypothesis. Hence the whole derivation, and its resulting value, is unique. 2. Progress (for a typed language). If `e` is well-typed and is not already a value, then some evaluation rule applies to it — evaluation never gets "stuck" on a syntactically valid, type-correct program. This is proved by case analysis on typing rules matched against the corresponding evaluation rules (e.g., a well-typed `e1 op e2` guarantees `e1` and `e2` evaluate to numbers, so `[Op]`'s side condition is satisfiable). Progress together with preservation (evaluation preserves well-typedness) constitute type soundness, the guarantee that "well-typed programs don't go wrong." 3. Big-step / small-step agreement. `ρ ⊢ e ⇓ v` holds if and only if `e/ρ → v` (the small-step relation reaches the value `v` in finitely many steps). Proof sketch*: by induction on the big-step derivation for the forward direction (each big-step rule is simulated by a finite, non-empty sequence of small-step reductions built from its premises' step sequences), and by induction on the length of the small-step reduction sequence for the reverse direction. This equivalence is what licenses using whichever style is more convenient for a given proof or implementation, and it underlies proving compiler transformations (constant folding, inlining) correct: showing a rewritten expression small-step-reduces to the same value as the original, or equivalently big-step-evaluates to it, is exactly a semantics-preservation proof.

Tradeoffs. Big-step semantics is compact and matches interpreter code directly, but it cannot express or reason about non-terminating computations (there is no derivation for a diverging program — that absence is itself the fact you must reason about separately), nor easily model interleaving/concurrency. Small-step semantics handles both gracefully (a diverging program is one with an infinite `→` chain, directly observable) but is more verbose to state and prove properties about, since every intermediate configuration must be tracked. Choosing environment-extension over substitution avoids the cost and hygiene hazards (variable capture) of textual substitution, at the price of needing an explicit closure representation for functions.

Evaluate ``` let x = 2 + 3 in if x < 10 then x * x else 0 ``` under the empty environment `ρ₀ = {}`, tracing both the big-step derivation and, in parallel, the corresponding small-step reduction sequence.

Both columns agree on the final value `25`, illustrating the big-step/small-step equivalence proved above; the small-step column additionally exposes the intermediate configurations `if 5<10 then xx else 0` that the big-step derivation never writes down explicitly — exactly the extra granularity small-step semantics is built to expose. A second, trickier case shows why environment discipline, not just arithmetic, is what evaluation is really testing: ``` let x = 10 in let f = λy. x + y in let x = 20 in f 5 ``` Tracing `[Lam]`: when `f` is created, its closure captures the environment <strong>at that point</strong>, `{x↦10}` — call this `ρ_f`. The later `let x = 20` shadows `x` in the outer scope but does <strong>not</strong> touch `ρ_f`, because closures freeze their creation environment. When `f 5` is applied, `[App]` evaluates `f`'s body `x + y` in `ρ_f[y↦5] = {x↦10, y↦5}`, giving `10 + 5 = 15`, <strong>not</strong> `20 + 5 = 25`. This is the formal justification for lexical (static) scoping: rule `[App]`'s premise `ρ' ⊢ e ⇓ v` — using the closure's own `ρ'`, not the call site's `ρ` — is precisely the mechanism, and getting this rule wrong (using the caller's* environment instead) is exactly what produces dynamic scoping, a different and less common discipline.

The formal machinery of expression evaluation — substitution, reduction, normal forms — descends directly from mathematical logic's study of computation, decades before electronic computers existed, and was later reshaped into the operational-semantics style used throughout language design.

Every interpreter for every scripting or dynamic language — Python's CPython evaluator, JavaScript engines' bytecode interpreters before JIT compilation, Scheme and Lisp REPLs — implements some version of the recursive `eval` function shown here, walking an AST or its intermediate representation against an environment (or, at machine level, a stack frame and closure structure playing the same role). Compilers rely on the same reduction rules to justify constant folding (rewriting `2+3` to `5` at compile time is only sound because the small-step rule for `+` proves the two are semantically identical) and inlining (substituting a function call by its body, justified by β-reduction). Formal verification tools and proof assistants (Coq, Isabelle) encode exactly these big-step or small-step judgments to prove compiler correctness theorems, most famously in the CompCert verified C compiler. Database query planners and spreadsheet engines apply the same "reduce until no redex remains" discipline to formula evaluation. Understanding evaluation as controlled rewriting under an environment is the direct prerequisite for Evaluation Strategies: Call-by-Value, Name, and Need, which studies which redex a language chooses to contract first, and for The Functional Paradigm, which elevates expression reduction — rather than statement execution — into the entire programming model.

:::quiz[In the big-step rule `[App]`, the function's body is evaluated in which environment?]

• The environment at the call site
• A brand-new empty environment
• The environment captured inside the closure, extended with the argument ✓
• The global environment only

Ask the tutor: How does the choice between call-by-value and call-by-name change which redex the evaluator picks first, and why can that change whether a program terminates?