Meta Theory

Bor-Yuh Evan Chang

Thursday, September 4, 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 5 - Meta Theory

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

FAQ on the Program Verification Exercise

Theorem 1 (Evenness Invariant, Operationally) For any expression $e$ and store $\rho$ such that $\rho(\texttt{i})$ is even, if \[ \mathcal{E} :: \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.

Can you prove this by mathematical induction (i.e., induction on the number of iterations of the loop)?

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'$ in one step.”

Reducing Statements

\[ \fbox{$\langle \rho, s \rangle \rightarrow\langle \rho', s' \rangle$} \]

no $\TirName{DoSkip}$

$\inferrule[DoAssign]{ \rho \vdash e \Downarrow v }{ \langle \rho, x \mathrel{\texttt{=}}e \rangle \rightarrow \langle \rho(x \leftarrow v) , \texttt{;} \rangle }$

$\inferrule[DoSeq]{ \phantom{\Downarrow} }{ \langle \rho, \texttt{;} \mathbin{\texttt{;}} s \rangle \rightarrow \langle \rho, s \rangle }$

$\inferrule[DoIfTrue]{ \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_1 \rangle }$

$\inferrule[DoIfFalse]{ \rho \vdash e \Downarrow\mathbf{false} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_2 \rangle }$

$\inferrule[DoWhile]{ \phantom{\Downarrow} }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }$

$\inferrule[SearchSeq]{ \langle \rho, s_1 \rangle \rightarrow\langle \rho', s_1' \rangle }{ \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow \langle \rho', s_1' \mathbin{\texttt{;}} s_2 \rangle }$

Figure 1: A small-step operational semantics for JavaScripty statements.

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.

Reachabilty in a Transition System

Define a judgment form $\langle \rho, s \rangle \rightarrow^{\ast}\langle \rho', s' \rangle$ that says, “In store $\rho$, statement $s$ reduces to statement $s'$ in store $\rho'$ in 0-or-more-steps.”

Reachabilty in a Transition System

Consider the reflexive-transitive closure of the small-step relation defined as follows:

\[ \fbox{$\langle \rho, s \rangle \rightarrow^{\ast}\langle \rho', s' \rangle$} \]

$\inferrule[ReachRefl]{ \phantom{ \langle \rho, \rangle } }{ \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho, s \rangle }$

$\inferrule[ReachTrans]{ \langle \rho, s \rangle \rightarrow \langle \rho', s' \rangle \and \langle \rho', s' \rangle \rightarrow^{\ast} \langle \rho'', s'' \rangle }{ \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho'', s'' \rangle }$

Big-Step Implies Small-Step

Theorem 2 (Evaluation implies reduction) If $\mathcal{E} :: \rho \vdash s \Downarrow\rho'$, then $\mathcal{M} :: \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $

Proof. By structural induction on derivation $\mathcal{E}$.

Big-Step Implies Small-Step

Proof. By structural induction on derivation $\mathcal{E}$.

Case: $\mathcal{E} = \inferright{EvalSkip}{ }{ \rho \vdash \texttt{;} \Downarrow\rho }$

$\mathcal{M} = \inferright{ReachRefl}{ }{ \langle \rho, \texttt{;} \rangle \rightarrow^{\ast} \langle \rho, \texttt{;} \rangle }$

by definition

Case: $\mathcal{E} = \inferright{EvalAssign}{ \mathcal{E_1} :: \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }$

$\rho' = \rho(x \leftarrow v)$

by assumption

$\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoAssign}{ \mathcal{E_1} :: \rho \vdash e \Downarrow v }{ \langle \rho, x \mathrel{\texttt{=}}e \rangle \rightarrow \langle \rho' , \texttt{;} \rangle } \and \inferright{ReachRefl}{ }{ \langle \rho', \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, x \mathrel{\texttt{=}}e \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$

by definition

Case: $\mathcal{E} = \inferright{EvalSeq}{ \mathcal{E_1} :: \rho \vdash s_1 \Downarrow\rho'' \and \mathcal{E_2} :: \rho'' \vdash s_2 \Downarrow\rho' }{ \rho \vdash s_1 \mathbin{\texttt{;}} s_2 \Downarrow \rho' }$

$\mathcal{M_1} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle $	by the i.h. on $\mathcal{E_1}$
$\mathcal{M_2} :: \langle \rho'', s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $	by the i.h. on $\mathcal{E_2}$
$\mathcal{M} :: \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $	by Lemma 1 on $\mathcal{M_1}$ and $\mathcal{M_2}$

Case: $\mathcal{E} = \inferright{EvalIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E_2} :: \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }$

$\mathcal{E_{21}} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $

by the i.h. on $\mathcal{E_2}$

$\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_1 \rangle } \and \mathcal{E_{21}} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$

by definition

Case: $\mathcal{E} = \inferright{EvalIfFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} \and \mathcal{E_2} :: \rho \vdash s_2 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }$

$\mathcal{E_{21}} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $

by the i.h. on $\mathcal{E_2}$

$\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoIfFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow \langle \rho, s_2 \rangle } \and \mathcal{E_{21}} :: \langle \rho, s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$

by definition

Case: $\mathcal{E} = \inferright{EvalWhileFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }$

$\mathcal{S_1} = \inferright{DoWhile}{ }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }$

by definition

$\mathcal{M} = \inferright{ReachTrans}{ \mathcal{S_1} \and \inferright{ReachTrans}{ \inferright{DoIfFalse}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{false} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\;\texttt{;} \rangle \rightarrow \langle \rho, \texttt{;} \rangle } \and \inferright{ReachRefl}{ }{ \langle \rho', \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho', \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$

by definition

Case: $\mathcal{E} = \inferright{EvalWhileTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E_2} :: \rho \vdash s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho' }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho' }$

$\mathcal{S_1} = \inferright{DoWhile}{ }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }$	by definition
$\mathcal{M_2} :: \langle \rho, s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $	by the i.h. on $\mathcal{E_2}$
$\mathcal{M} = \inferright{ReachTrans}{ \mathcal{S_1} \and \inferright{ReachTrans}{ \inferright{DoIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\;\texttt{;} \rangle \rightarrow \langle \rho, s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle } \and \mathcal{M_2} }{ \langle \rho', \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$	by definition

Lemma: Sequential Composition

Lemma 1 (Reduction composes sequentially) If $\mathcal{M_1} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle $ and $\mathcal{M_2} :: \langle \rho'', s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $, then $\mathcal{M} :: \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $

Proof. By structural induction on derivation $\mathcal{M_1}$.

Lemma: Sequential Composition

Proof. By structural induction on derivation $\mathcal{M_1}$.

Case: $\mathcal{M_1} = \inferright{ReachRefl}{ }{ \langle \rho, \texttt{;} \rangle \rightarrow^{\ast} \langle \rho, \texttt{;} \rangle }$

$\mathcal{M} = \inferright{ReachTrans}{ \inferright{DoSeq}{ }{ \langle \rho, \texttt{;} \mathbin{\texttt{;}} s_2 \rangle \rightarrow \langle \rho, s_2 \rangle } \and \mathcal{M_2} :: \langle \rho, s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, \texttt{;} \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$

by definition

Case: $\mathcal{M_1} = \inferright{ReachTrans}{ \mathcal{S_{11}} :: \langle \rho, s_1 \rangle \rightarrow \langle \rho''', s_1' \rangle \and \mathcal{M_{12}} :: \langle \rho''', s_1' \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle }{ \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle }$

$\mathcal{M'} :: \langle \rho''', s_1' \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $

by the i.h. on $\mathcal{M_{12}}$ with $\mathcal{M_{2}}$

$\mathcal{M} = \inferright{ReachTrans}{ \inferright{SearchSeq}{ \mathcal{S_{11}} :: \langle \rho, s_1 \rangle \rightarrow \langle \rho''', s_1' \rangle }{ \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow \langle \rho''', s_1' \mathbin{\texttt{;}} s_2 \rangle } \and \mathcal{M'} :: \langle \rho''', s_1' \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }{ \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }$

by definition

Small-Step Implies Big-Step

Theorem 3 (Reduction implies evaluation) If $\mathcal{M} :: \langle \rho, s \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle $, then $\mathcal{E} :: \rho \vdash s \Downarrow\rho'$.

Proof. By structural induction on derivation $\mathcal{M}$.

\(\mathcal{M_1} :: \langle \rho, s_1 \rangle \rightarrow^{\ast} \langle \rho'', \texttt{;} \rangle \)	by the i.h. on \(\mathcal{E_1}\)
\(\mathcal{M_2} :: \langle \rho'', s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \)	by the i.h. on \(\mathcal{E_2}\)
\(\mathcal{M} :: \langle \rho, s_1 \mathbin{\texttt{;}} s_2 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \)	by Lemma 1 on \(\mathcal{M_1}\) and \(\mathcal{M_2}\)

\(\mathcal{S_1} = \inferright{DoWhile}{ }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle }\)	by definition
\(\mathcal{M_2} :: \langle \rho, s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle \)	by the i.h. on \(\mathcal{E_2}\)
\(\mathcal{M} = \inferright{ReachTrans}{ \mathcal{S_1} \and \inferright{ReachTrans}{ \inferright{DoIfTrue}{ \mathcal{E_1} :: \rho \vdash e \Downarrow\mathbf{true} }{ \langle \rho, \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\;\texttt{;} \rangle \rightarrow \langle \rho, s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle } \and \mathcal{M_2} }{ \langle \rho', \mathbf{if}\;\texttt{(}e\texttt{)}\; s_1 \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \;\mathbf{else}\; \texttt{;} \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle } }{ \langle \rho, \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \rangle \rightarrow^{\ast} \langle \rho', \texttt{;} \rangle }\)	by definition