Operational Semantics

Bor-Yuh Evan Chang

Thursday, August 28, 2025

\(\newcommand{\TirName}[1]{\text{#1}} \newcommand{\inferlab}[3]{ \let\and\qquad \begin{array}{l} \TirName{#1} \\ \displaystyle \frac{#2}{#3} \end{array} } \newcommand{\inferright}[3]{ \let\and\qquad \displaystyle \frac{#2}{#3}\TirName{#1} } \newcommand{\inferrule}[3][]{\inferlab{#1}{#2}{#3}} \newcommand{\infer}[3][]{\inferrule[#1]{#2}{#3}} \)

Meeting 3 - Operational Semantics

What questions do you have? What questions does your neighbor have?

Announcements

• Recommended: While getting up to speed on operational semantics this week, play with Lean (look at “Functional Programming in Lean”).

Review: What is an operational semantics?

JavaScripty Expressions

\[ \begin{array}{rrrl} \text{values} & v& \mathrel{::=}& n\mid b \\ \text{expressions} & e& \mathrel{::=}& n\mid b \mid x \mid\mathop{\mathit{uop}} e_1 \mid e_1 \mathbin{\mathit{bop}} e_2 \\ \text{unary operators} & \mathit{uop}& \mathrel{::=}& \texttt{-} \mid\texttt{!} \\ \text{binary operators} & \mathit{bop}& \mathrel{::=}& \texttt{+} \mid\texttt{-} \mid\texttt{*} \mid\texttt{/} \mid\texttt{\&\&} \mid\texttt{||} \mid\texttt{===} \mid\texttt{!==} \mid\texttt{<} \mid\texttt{<=} \mid\texttt{>} \mid\texttt{>=} \\ \text{numbers} & n \\ \text{booleans} & b \\ \text{variables} & x \end{array} \]

Figure 1: Syntax of JavaScripty expressions with variables, numbers, and booleans (i.e., arithmetic and logic).

JavaScripty Statements

\[ \begin{array}{rrrl} \text{statements} & s& \mathrel{::=}& \texttt{;} \mid x \mathrel{\texttt{=}}e \mid s_1 \mathbin{\texttt{;}} s_2 \mid\mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \mid\mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \end{array} \]

Figure 2: Syntax of JavaScripty statements with assignment, sequencing, branching, and looping.

A semantic domain

\[ \begin{array}{rrrl} \text{stores} & \rho& \mathrel{::=}& \circ \mid\rho,x \mapsto v \end{array} \]

\[ \rho(x) = v \]

\[ \rho(x \leftarrow v) = \rho' \]

\[ \rho[x \mapsto v] = \rho' \]

Evaluating Expressions

\[ \rho \vdash e \Downarrow v \]

A judgment is …

A judgment form is …

A set of inference rules …

A derivation …

Exercise: Executing Statements

Define a judgment form \(\rho \vdash s \Downarrow\rho'\) that says, “In store \(\rho\), statement \(s\) executes to yield store \(\rho'\).”

Exercise: Program Verification

Theorem 1 (Evenness Invariant, Operationally) For any expression \(e\) and store \(\rho\) such that \(\rho(\texttt{i})\) is even, if \[ \mathcal{D}:: \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow\rho' \] then \(\rho'(\texttt{i})\) is even.

Big-Step versus Small-Step Operational Semantics

Exercise: Reducing Statements

Define a judgment form \(\langle \rho, s \rangle \rightarrow\langle \rho', s' \rangle\) that says, “In store \(\rho\), statement \(s\) reduces to statement \(s'\) in store \(\rho'\).”

Exercise: Meta-Theory

Prove an equivalence between big-step evaluation and small-step reduction. You will first need to define iterating the small-step relation to state the theorem. Then, you will need to come up with a lemma that relates single-step reduction with evaluation.