Nana Adjei Manu

Operational Semantics: Adding Variables, Functions and Conditionals

February 14, 2025

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:

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:

  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:

<λ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:

  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

<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₂,

  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:

<λ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:

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:

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.

← Back to Home