In our previous article, we explored operational semantics using a simple language of arithmetic expressions. While instructive, a language with only arithmetic operations is quite limited. In this article, we’ll extend our language with three powerful features: variables, functions, and conditionals. These additions transform our simple calculator into a complete functional programming language.

Extending Our Language

Let’s start by extending the syntax of our language:

e ::= n                       (Number literals)
    | x                       (Variables)
    | e + e                   (Addition)
    | e - e                   (Subtraction)
    | e * e                   (Multiplication)
    | e / e                   (Division)
    | if e then e else e      (Conditional)
    | λx.e                    (Function abstraction/Lambda)
    | e e                     (Function application)

Where:

• n represents integer constants
• x represents variable names
• λx.e defines a function with parameter x and body e
• e e applies the function in the first expression to the argument in the second
• if e then e else e evaluates the first expression and then evaluates either the second or third expression based on the result

Values in Our Extended Language

With the addition of functions, we need to update what we consider “values” in our language:

v ::= n                       (Number literals)
    | λx.e                    (Function values)

A value is now either a number or a function abstraction. Both represent fully evaluated expressions that cannot be reduced further.

Introducing Environments

To handle variables, we need a way to keep track of their bindings. This is done with environments. An environment (typically denoted ρ or Γ) maps variable names to their values:

ρ ::= ∅                       (Empty environment)
    | ρ[x ↦ v]                (Environment extended with a binding)

We use the notation ρ(x) to look up the value of variable x in environment ρ.

Small-Step Operational Semantics with Environments

With environments, our small-step transition relation becomes ⟨e, ρ⟩ → ⟨e', ρ'⟩, indicating that expression e in environment ρ reduces to expression e' in environment ρ'.

Variable Lookup

$$ \langle x, \rho \rangle \to \langle v, \rho \rangle \qquad \text{where } \rho(x) = v $$

This rule says: A variable reference evaluates to the value it’s bound to in the current environment.

Arithmetic Operations

The rules for arithmetic are similar to before, but now include the environment:

$$ \begin{aligned} \langle n_1 + n_2, \rho \rangle &\to \langle n_3, \rho \rangle &&\text{where } n_3 = n_1 + n_2\\ \langle n_1 - n_2, \rho \rangle &\to \langle n_3, \rho \rangle &&\text{where } n_3 = n_1 - n_2\\ \langle n_1 \times n_2, \rho \rangle &\to \langle n_3, \rho \rangle &&\text{where } n_3 = n_1 \times n_2\\ \langle n_1 / n_2, \rho \rangle &\to \langle n_3, \rho \rangle &&\text{where } n_3 = n_1 / n_2,\ n_2 \neq 0 \end{aligned} $$

Evaluation Context Rules for Arithmetic

The context rules also include environments:

$$ \frac{\langle e_1, \rho \rangle \to \langle e_1', \rho \rangle}{\langle e_1 + e_2, \rho \rangle \to \langle e_1' + e_2, \rho \rangle} $$

$$ \frac{\langle e_2, \rho \rangle \to \langle e_2', \rho \rangle}{\langle v_1 + e_2, \rho \rangle \to \langle v_1 + e_2', \rho \rangle} $$

Similar rules apply for subtraction, multiplication, and division.

Conditional Expressions

$$ \frac{\langle e_1, \rho \rangle \to \langle e_1', \rho \rangle}{\langle \text{if } e_1 \text{ then } e_2 \text{ else } e_3, \rho \rangle \to \langle \text{if } e_1' \text{ then } e_2 \text{ else } e_3, \rho \rangle} $$

$$ \begin{aligned} \langle \text{if } 0 \text{ then } e_2 \text{ else } e_3, \rho \rangle &\to \langle e_3, \rho \rangle &&\text{(false: 0)}\\ \langle \text{if } n \text{ then } e_2 \text{ else } e_3, \rho \rangle &\to \langle e_2, \rho \rangle &&\text{(true: } n \neq 0\text{)} \end{aligned} $$

These rules say:

1. If the condition can be reduced, reduce it first
2. If the condition is 0 (representing false), evaluate the else branch
3. If the condition is any non-zero number (representing true), evaluate the then branch

Function Rules

A lambda expression (function) is already a value, so it doesn’t reduce further:

$$ \langle \lambda x.e, \rho \rangle \to \langle \lambda x.e, \rho \rangle $$

However, we need rules for function application:

$$ \frac{\langle e_1, \rho \rangle \to \langle e_1', \rho \rangle}{\langle e_1\, e_2, \rho \rangle \to \langle e_1'\, e_2, \rho \rangle} \qquad \frac{\langle e_2, \rho \rangle \to \langle e_2', \rho \rangle}{\langle v_1\, e_2, \rho \rangle \to \langle v_1\, e_2', \rho \rangle} $$

$$ \langle (\lambda x.e)\, v, \rho \rangle \to \langle e, \rho[x \mapsto v] \rangle $$

The first two rules are evaluation context rules that ensure we evaluate the function and argument expressions. The third rule is the crucial one for function application: when a function (λx.e) is applied to a value v, we evaluate the function body e in an environment extended with a binding from the parameter x to the argument value v.

Example Derivation with a Function

Let’s see how (λx. x + 1) 5 evaluates:

⟨(λx. x + 1) 5, ρ⟩
→ ⟨x + 1, ρ[x ↦ 5]⟩     (function application)
→ ⟨5 + 1, ρ[x ↦ 5]⟩     (variable lookup)
→ ⟨6, ρ[x ↦ 5]⟩         (arithmetic operation)

This shows how:

1. The function is applied, creating a new environment where x is bound to 5
2. The variable x is looked up in this environment, yielding 5
3. The addition is performed, yielding the final result 6

Example with Conditionals

Let’s evaluate if (3 - 3) then 10 else 20:

⟨if (3 - 3) then 10 else 20, ρ⟩
→ ⟨if 0 then 10 else 20, ρ⟩     (evaluating the condition)
→ ⟨20, ρ⟩                       (condition is 0, so take else branch)

Big-Step Operational Semantics with Environments

For big-step semantics with our extended language, our relation is ⟨e, ρ⟩ ⇓ v, meaning expression e in environment ρ evaluates to value v.

Constants and Variables

$$ \langle n, \rho \rangle \Downarrow n \qquad\qquad \langle x, \rho \rangle \Downarrow v \quad \text{where } \rho(x) = v $$

Arithmetic Operations

$$ \frac{\langle e_1, \rho \rangle \Downarrow n_1 \quad \langle e_2, \rho \rangle \Downarrow n_2}{\langle e_1 + e_2, \rho \rangle \Downarrow n_3} \qquad (n_3 = n_1 + n_2) $$

Similar rules apply for subtraction, multiplication, and division.

Conditional Expressions

$$ \frac{\langle e_1, \rho \rangle \Downarrow 0 \quad \langle e_3, \rho \rangle \Downarrow v}{\langle \text{if } e_1 \text{ then } e_2 \text{ else } e_3, \rho \rangle \Downarrow v} $$

$$ \frac{\langle e_1, \rho \rangle \Downarrow n \quad \langle e_2, \rho \rangle \Downarrow v \quad n \neq 0}{\langle \text{if } e_1 \text{ then } e_2 \text{ else } e_3, \rho \rangle \Downarrow v} $$

Functions

$$ \langle \lambda x.e, \rho \rangle \Downarrow \langle \lambda x.e, \rho \rangle $$

In big-step semantics, a function evaluates to a closure, which captures both the function and its defining environment.

Function Application

$$ \frac{\langle e_1, \rho \rangle \Downarrow \langle \lambda x.e, \rho' \rangle \quad \langle e_2, \rho \rangle \Downarrow v_2 \quad \langle e, \rho'[x \mapsto v_2] \rangle \Downarrow v}{\langle e_1\, e_2, \rho \rangle \Downarrow v} $$

This rule says: To evaluate a function application e₁ e₂,

1. Evaluate e₁ to get a function closure ⟨λx.e, ρ’⟩
2. Evaluate e₂ to get the argument value v₂
3. Evaluate the function body e in the function’s captured environment ρ’ extended with a binding from parameter x to argument value v₂

Example with Big-Step Semantics

Here’s how we would derive the evaluation of (λx. x + 1) 5 using big-step semantics:

$$ \frac{\langle \lambda x.\, x + 1, \rho \rangle \Downarrow \langle \lambda x.\, x + 1, \rho \rangle \quad \langle 5, \rho \rangle \Downarrow 5 \quad \langle x + 1, \rho[x \mapsto 5] \rangle \Downarrow 6}{\langle (\lambda x.\, x + 1)\, 5, \rho \rangle \Downarrow 6} $$

Where ⟨x + 1, ρ[x ↦ 5]⟩ ⇓ 6 would be derived as:

$$ \frac{\langle x, \rho[x \mapsto 5] \rangle \Downarrow 5 \quad \langle 1, \rho[x \mapsto 5] \rangle \Downarrow 1}{\langle x + 1, \rho[x \mapsto 5] \rangle \Downarrow 6} $$

Lexical vs. Dynamic Scoping

The semantics we’ve defined uses lexical scoping (also called static scoping): a function captures the environment where it was defined. This is why our closures include both the function code and its environment.

To see the importance of this, consider:

let x = 1 in
let f = λy. x + y in
let x = 2 in
f 3

With lexical scoping, this evaluates to 4 (1 + 3) because f captures the environment where x is 1.

With dynamic scoping, it would evaluate to 5 (2 + 3) because x would be looked up in the calling environment.

Most modern languages use lexical scoping because it leads to more predictable behavior and supports better encapsulation.

A More Complex Example: Higher-Order Functions

One of the powerful features of functional programming is higher-order functions—functions that take other functions as arguments or return them as results. Let’s see how our semantics handles a simple higher-order function:

(λf. λx. f (f x)) (λy. y * 2) 3

This applies a function twice to an input. Let’s trace through the evaluation:

⟨(λf. λx. f (f x)) (λy. y * 2) 3, ρ⟩
→ ⟨(λx. f (f x))[f ↦ (λy. y * 2)], 3, ρ⟩    (applying the first function)
→ ⟨f (f 3), ρ[f ↦ (λy. y * 2)][x ↦ 3]⟩     (applying the second function)
→ ⟨(λy. y * 2) ((λy. y * 2) 3), ρ[f ↦ (λy. y * 2)][x ↦ 3]⟩    (variable lookup)
→ ⟨(λy. y * 2) (3 * 2), ρ[f ↦ (λy. y * 2)][x ↦ 3]⟩    (applying inner function)
→ ⟨(λy. y * 2) 6, ρ[f ↦ (λy. y * 2)][x ↦ 3]⟩     (arithmetic)
→ ⟨6 * 2, ρ[f ↦ (λy. y * 2)][x ↦ 3][y ↦ 6]⟩     (applying outer function)
→ ⟨12, ρ[f ↦ (λy. y * 2)][x ↦ 3][y ↦ 6]⟩    (arithmetic)

This demonstrates how our semantics correctly handles the intricate behavior of higher-order functions.

Adding Recursion

One crucial feature in functional programming is recursion. To add recursion to our language, we could introduce a special construct rec f.e that defines a recursive function:

e ::= ... | rec f.e   (Recursive function definition)

The semantics for this would involve a fixed-point operator, allowing the function to refer to itself.

Using this, we could define a factorial function:

rec fact. λn. if n then 1 else n * (fact (n - 1))

Applying this to 5 would compute 5!, or 120.

Conclusion

By extending our language with variables, functions, and conditionals, we’ve created a small but complete functional programming language. The formal semantics we’ve defined provides a precise specification of how programs in this language execute, covering:

• Variable binding and lookup through environments
• Control flow through conditionals
• Abstraction through function definitions
• Computation through function application
• Lexical scoping and closures
• Higher-order functions

This framework forms the foundation of many real-world functional programming languages like Scheme, ML, Haskell, and even the functional aspects of JavaScript.

Further extensions to our language could include:

• Algebraic data types for structured data
• Pattern matching for data decomposition
• Mutable state for imperative features
• Exception handling for error management
• Module systems for code organization

Each of these would require additional semantic rules, but the fundamental approach would remain the same: precisely defining how programs execute, step by step.

Through operational semantics, we gain a rigorous understanding of programming language behavior, which guides language design, implementation, and verification—essential activities for building reliable and well-understood programming systems.