IMP Language

Overview: The “Warehouse” of Computation

If the Lambda Calculus is an elegant mathematical dream where everything is a pure, side-effect-free function evaluating to a value, IMP is the blue-collar reality of moving boxes around in a warehouse.

IMP is the theoretical “Hello World” of imperative languages. It strips away objects, types, and functions to leave only the bare essentials of how languages like C, Java, or Python actually execute: commands mutating memory over time.

In $\lambda$-calculus, computation is rewriting the code itself ($\beta$-reduction). In IMP, the code remains completely static. Instead, the code issues orders that mutate an invisible, external environment.

1. Syntax

IMP is built on three syntactic pillars: Arithmetic ($AExp$), Booleans ($BExp$), and Commands ($Com$). Commands are the only constructs that actually do things (cause side effects). Assuming variables $x \in Var$ and integers $n \in \mathbb{Z}$:

Arithmetic Expressions ($AExp$): (Evaluate to integers, no side effects)

$$a ::= n \mid x \mid a_1 + a_2 \mid a_1 - a_2 \mid a_1 \times a_2$$

Boolean Expressions ($BExp$): (Evaluate to truth values, no side effects)

$$b ::= \text{true} \mid \text{false} \mid a_1 = a_2 \mid a_1 \leq a_2 \mid \neg b \mid b_1 \wedge b_2$$

Commands ($Com$): (Do not evaluate to values; they mutate state)

$$c ::= \text{skip} \mid x := a \mid c_1 ; c_2 \mid \text{if } b \text{ then } c_1 \text{ else } c_2 \mid \text{while } b \text{ do } c$$

2. Configurations and State

Unlike pure $\lambda$-calculus (which relies on $\alpha$-conversion and environment closures), IMP relies on a mutable State (or store) to track variables.

• State ($\sigma$): A partial function mapping variables to integers, $\sigma : Var \to \mathbb{Z}$.
• Configuration: A tuple $\langle c, \sigma \rangle$ representing the current point of execution.
• State Update: $\sigma[x \mapsto n]$ denotes a new state identical to $\sigma$, except that the variable $x$ now maps to the integer $n$.

3. Big-Step Semantics (Natural Semantics)

Big-step semantics skip the intermediate machinery and tell you the final result. It reads like writing a standard recursive interpreter.

The judgment $\langle c, \sigma \rangle \Downarrow \sigma'$ means: “If you run command $c$ starting with memory $\sigma$, it will eventually terminate and leave memory in state $\sigma'$.”

(Note: $\Downarrow_a$ evaluates arithmetic to an integer; $\Downarrow_b$ evaluates booleans to true/false).

Skip & Assignment:

$$\frac{}{\langle \text{skip}, \sigma \rangle \Downarrow \sigma} \quad \frac{\langle a, \sigma \rangle \Downarrow_a n}{\langle x := a, \sigma \rangle \Downarrow \sigma[x \mapsto n]}$$

Sequencing (Do $c_1$, then do $c_2$):

$$\frac{\langle c_1, \sigma \rangle \Downarrow \sigma'' \quad \langle c_2, \sigma'' \rangle \Downarrow \sigma'}{\langle c_1 ; c_2, \sigma \rangle \Downarrow \sigma'}$$

If-Then-Else:

$$\frac{\langle b, \sigma \rangle \Downarrow_b \text{true} \quad \langle c_1, \sigma \rangle \Downarrow \sigma'}{\langle \text{if } b \text{ then } c_1 \text{ else } c_2, \sigma \rangle \Downarrow \sigma'}$$ $$\frac{\langle b, \sigma \rangle \Downarrow_b \text{false} \quad \langle c_2, \sigma \rangle \Downarrow \sigma'}{\langle \text{if } b \text{ then } c_1 \text{ else } c_2, \sigma \rangle \Downarrow \sigma'}$$

While Loop:

$$\frac{\langle b, \sigma \rangle \Downarrow_b \text{false}}{\langle \text{while } b \text{ do } c, \sigma \rangle \Downarrow \sigma}$$ $$\frac{\langle b, \sigma \rangle \Downarrow_b \text{true} \quad \langle c, \sigma \rangle \Downarrow \sigma'' \quad \langle \text{while } b \text{ do } c, \sigma'' \rangle \Downarrow \sigma'}{\langle \text{while } b \text{ do } c, \sigma \rangle \Downarrow \sigma'}$$

4. Small-Step Semantics (Structural Operational Semantics)

Big-step is great, but it has a fatal flaw: it cannot describe non-terminating programs (infinite loops) or concurrency, because there is no “final state” to return.

Small-step semantics fixes this by modeling computation as a sequence of discrete, atomic ticks of a clock: $\langle c, \sigma \rangle \rightarrow \langle c', \sigma' \rangle$. This is the imperative equivalent of step-by-step $\beta$-reduction.

Assignment:
(Assuming expression $a$ has already reduced step-by-step to integer $n$)

$$\frac{}{\langle x := n, \sigma \rangle \rightarrow \langle \text{skip}, \sigma[x \mapsto n] \rangle}$$

Sequencing:

$$\frac{\langle c_1, \sigma \rangle \rightarrow \langle c_1', \sigma' \rangle}{\langle c_1 ; c_2, \sigma \rangle \rightarrow \langle c_1' ; c_2, \sigma' \rangle}$$ $$\frac{}{\langle \text{skip} ; c_2, \sigma \rangle \rightarrow \langle c_2, \sigma \rangle}$$

If-Then-Else:

$$\frac{}{\langle \text{if true then } c_1 \text{ else } c_2, \sigma \rangle \rightarrow \langle c_1, \sigma \rangle}$$ $$\frac{}{\langle \text{if false then } c_1 \text{ else } c_2, \sigma \rangle \rightarrow \langle c_2, \sigma \rangle}$$

While Loop (The unrolling trick):
(Instead of resolving the whole loop, small-step simply unwraps one iteration and converts it into an if-statement. This allows infinite loops to just keep unrolling forever without breaking the math).

$$\frac{}{\langle \text{while } b \text{ do } c, \sigma \rangle \rightarrow \langle \text{if } b \text{ then } (c ; \text{while } b \text{ do } c) \text{ else skip}, \sigma \rangle}$$