2025-02-14

Operational Semantics: Adding Variables, Functions and Conditionals

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

<x, ρ> → <v, ρ>   where ρ(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:

<n₁ + n₂, ρ> → <n₃, ρ>      where n₃ = n₁ + n₂
<n₁ - n₂, ρ> → <n₃, ρ>      where n₃ = n₁ - n₂
<n₁ * n₂, ρ> → <n₃, ρ>      where n₃ = n₁ * n₂
<n₁ / n₂, ρ> → <n₃, ρ>      where n₃ = n₁ / n₂ and n₂ ≠ 0

Evaluation Context Rules for Arithmetic

The context rules also include environments:

<e₁, ρ> → <e₁', ρ>
--------------------------
<e₁ + e₂, ρ> → <e₁' + e₂, ρ>

<e₂, ρ> → <e₂', ρ>
--------------------------
<v₁ + e₂, ρ> → <v₁ + e₂', ρ>

Similar rules apply for subtraction, multiplication, and division.

Conditional Expressions

<e₁, ρ> → <e₁', ρ>
----------------------------------------------------
<if e₁ then e₂ else e₃, ρ> → <if e₁' then e₂ else e₃, ρ>

<if 0 then e₂ else e₃, ρ> → <e₃, ρ>      (False case: 0 is false)

<if n then e₂ else e₃, ρ> → <e₂, ρ>       (True case: any non-zero is true)

These rules say:

If the condition can be reduced, reduce it first
If the condition is 0 (representing false), evaluate the else branch
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:

<λx.e, ρ> → <λx.e, ρ>

However, we need rules for function application:

<e₁, ρ> → <e₁', ρ>
--------------------------
<e₁ e₂, ρ> → <e₁' e₂, ρ>

<e₂, ρ> → <e₂', ρ>
--------------------------
<v₁ e₂, ρ> → <v₁ e₂', ρ>

<(λx.e) v, ρ> → <e, ρ[x ↦ v]>

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:

The function is applied, creating a new environment where x is bound to 5
The variable x is looked up in this environment, yielding 5
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

<n, ρ> ⇓ n

<x, ρ> ⇓ v   where ρ(x) = v

Arithmetic Operations

<e₁, ρ> ⇓ n₁    <e₂, ρ> ⇓ n₂
-------------------------------
     <e₁ + e₂, ρ> ⇓ n₃

where n₃ = n₁ + n₂ (similar rules for -, *, /)

Conditional Expressions

<e₁, ρ> ⇓ 0    <e₃, ρ> ⇓ v
-------------------------------
<if e₁ then e₂ else e₃, ρ> ⇓ v

<e₁, ρ> ⇓ n    <e₂, ρ> ⇓ v    n ≠ 0
-------------------------------------
<if e₁ then e₂ else e₃, ρ> ⇓ v

Functions

<λx.e, ρ> ⇓ <λx.e, ρ>

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

Function Application

<e₁, ρ> ⇓ <λx.e, ρ'>    <e₂, ρ> ⇓ v₂    <e, ρ'[x ↦ v₂]> ⇓ v
-------------------------------------------------------------
                     <e₁ e₂, ρ> ⇓ v

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

Evaluate e₁ to get a function closure <λx.e, ρ’>
Evaluate e₂ to get the argument value v₂
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:

<λx. x + 1, ρ> ⇓ <λx. x + 1, ρ>    <5, ρ> ⇓ 5    <x + 1, ρ[x ↦ 5]> ⇓ 6
-----------------------------------------------------------------------
                       <(λx. x + 1) 5, ρ> ⇓ 6

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

<x, ρ[x ↦ 5]> ⇓ 5    <1, ρ[x ↦ 5]> ⇓ 1
-------------------------------------
        <x + 1, ρ[x ↦ 5]> ⇓ 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.