Induction

Bor-Yuh Evan Chang

Tuesday, September 2, 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 4 - Induction

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

Announcements

• Reminder: Reading/Post-Lecture Assignments
  • Post \(\ge\) 1 substantive comment, question, or answer for each lecture
  • Due before the next meeting

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 1: Syntax of JavaScripty statements with assignment, sequencing, branching, and looping.

Executing Statements

\[ \fbox{$\rho \vdash s \Downarrow\rho'$} \]

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

Figure 2: JavaScripty stores map variables \(x\) to values \(v\).

Exercise: Executing Statements

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

Executing Statements

\[ \fbox{$\rho \vdash s \Downarrow\rho'$} \]

\(\inferrule[EvalSkip]{ \phantom{\Downarrow} }{ \rho \vdash \texttt{;} \Downarrow\rho }\)

\(\inferrule[EvalAssign]{ \rho \vdash e \Downarrow v }{ \rho \vdash x \mathrel{\texttt{=}}e \Downarrow \rho(x \leftarrow v) }\)

\(\inferrule[EvalSeq]{ \rho \vdash s_1 \Downarrow\rho' \and \rho' \vdash s_2 \Downarrow\rho'' }{ \rho \vdash s_1 \mathbin{\texttt{;}} s_2 \Downarrow \rho'' }\)

\(\inferrule[EvalIfTrue]{ \rho \vdash e \Downarrow\mathbf{true} \and \rho \vdash s_1 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\)

\(\inferrule[EvalIfFalse]{ \rho \vdash e \Downarrow\mathbf{false} \and \rho \vdash s_2 \Downarrow\rho' }{ \rho \vdash \mathbf{if}\;\texttt{(}e\texttt{)}\;s_1\;\mathbf{else}\;s_2 \Downarrow \rho' }\)

\(\inferrule[EvalWhileFalse]{ \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\;s_1 \Downarrow \rho }\)

\(\inferrule[EvalWhileTrue]{ \rho \vdash e \Downarrow\mathbf{true} \and \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' }\)

Figure 3: A big-step operational semantics for JavaScripty statements.

Exercise: Program Verification

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.

Proof. By induction on derivation \(\mathcal{E}\).

Exercise: Program Verification

Proof. By induction on derivation \(\mathcal{E}\).

Case

\(\mathcal{E} = \inferright{EvalWhileFalse}{ \rho \vdash e \Downarrow\mathbf{false} }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow\rho }\)

\(\rho' = \rho\)	by assumption
\(\rho'(\texttt{i})\) is even	by assumption

Case

\(\mathcal{E} = \inferright{EvalWhileTrue}{ \rho \vdash e \Downarrow\mathbf{true} \and \mathcal{E_1} :: \rho \vdash \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \mathbin{\texttt{;}} \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow \rho' }{ \rho \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow\rho' }\)

\(\mathcal{E_{11}} :: \rho \vdash \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow\rho''\) and \(\mathcal{E_{12}} :: \rho'' \vdash \mathbf{while}\;\texttt{(}e\texttt{)}\; \texttt{i} \mathrel{\texttt{=}} \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow \rho' \)	for some store \(\rho''\) by inversion on \(\mathcal{E_1}\)
\(\mathcal{E_{111}} :: \rho \vdash \texttt{i} \mathbin{\texttt{+}} \texttt{2} \Downarrow v' \)	for some value \(v'\) s.t. \(\rho''(\texttt{i}) = v'\) by inversion on \(\mathcal{E_{11}}\)
\(\rho \vdash \texttt{i} \Downarrow \rho(\texttt{i}) \) and \(\rho \vdash \texttt{2} \Downarrow 2 \) s.t. \(v' = \rho(\texttt{i}) + 2\)	by inversion on \(\mathcal{E_{111}}\)
\(v'\) is even	by arithmetic
\(\rho''(\texttt{i})\) is even	since \(\rho''(\texttt{i}) = v'\)
\(\rho'(\texttt{i})\) is even	by the i.h. on \(\mathcal{E_{12}}\)

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.”

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.