# Appendix A: Operational Semantics

Chapter 16 of [The Resolution of Math](/content/books/resolution-of-math/index.html)

This appendix defines the full set of big-step operational semantics rules for all core constructs in the bounded arithmetic language. Each rule updates the resource state R = (steps, stack_depth, max_nat_depth).

## A.1 Arithmetic Rules

(E-Sub-Zero) If ⟨e, R⟩ ⇓ ⟨v, R’⟩, then `⟨sub(e, 0), R⟩ ⇓ ⟨v, R’ + (1, 0, 0)⟩`

(E-Sub-Succ) If ⟨e1, R⟩ ⇓ ⟨S(v1), R1⟩, ⟨e2, R1⟩ ⇓ ⟨S(v2), R2⟩, and ⟨sub(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, then `⟨sub(S(e1), S(e2)), R⟩ ⇓ ⟨v3, R3 + (1, 0, 0)⟩`

(E-Sub-Under) If ⟨e2, R⟩ ⇓ ⟨S(v2), R’⟩, then `⟨sub(0, S(e2)), R⟩ ⇓ ⟨error(“E102”), R’⟩`

(E-Mul-Zero) If ⟨e2, R⟩ ⇓ ⟨v2, R’⟩, then `⟨mul(0, e2), R⟩ ⇓ ⟨0, R’ + (1, 0, 0)⟩`

(E-Mul-Succ) If ⟨e1, R⟩ ⇓ ⟨S(v1), R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, `⟨mul(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, ⟨add(v2, v3), R3⟩ ⇓ ⟨v4, R4⟩, then `⟨mul(S(e1), e2), R⟩ ⇓ ⟨v4, R4 + (1, 0, 0)⟩`

## A.2 Division Rules

(E-Div) If ⟨div_safe(e1, e2, 0), R⟩ ⇓ ⟨v, R’⟩, then `⟨div(e1, e2), R⟩ ⇓ ⟨v, R’ + (1, 0, 0)⟩`

(E-Div-Guard) If steps ≥ max_div_steps, then `⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨error(“E004”), R⟩`

(E-Div-Zero) If ⟨e2, R⟩ ⇓ ⟨0, R’⟩, then `⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨error(“E103”), R’⟩`

(E-Div-Base) If ⟨e1, R⟩ ⇓ ⟨v1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, and lt(v1, v2) = B1, then `⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨0, R2 + (1, 0, 0)⟩`

(E-Div-Rec) If ⟨e1, R⟩ ⇓ ⟨v1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, lt(v1, v2) = B0, v2 ≠ 0, steps < max_div_steps, `⟨sub(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, `⟨div_safe(v3, v2, S(steps)), R3⟩ ⇓ ⟨v4, R4⟩, then `⟨div_safe(e1, e2, steps), R⟩ ⇓ ⟨S(v4), R4 + (1, 0, 0)⟩`

## A.3 Boolean Logic Rules

(E-And-False) If ⟨e1, R⟩ ⇓ ⟨B0, R’⟩, then `⟨and(e1, e2), R⟩ ⇓ ⟨B0, R’ + (1, 0, 0)⟩`

(E-And-True) If ⟨e1, R⟩ ⇓ ⟨B1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, then `⟨and(e1, e2), R⟩ ⇓ ⟨v2, R2 + (1, 0, 0)⟩`

(E-Or-True) If ⟨e1, R⟩ ⇓ ⟨B1, R’⟩, then `⟨or(e1, e2), R⟩ ⇓ ⟨B1, R’ + (1, 0, 0)⟩`

(E-Or-False) If ⟨e1, R⟩ ⇓ ⟨B0, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, then `⟨or(e1, e2), R⟩ ⇓ ⟨v2, R2 + (1, 0, 0)⟩`

(E-Not-True) If ⟨e, R⟩ ⇓ ⟨B1, R’⟩, then `⟨not(e), R⟩ ⇓ ⟨B0, R’ + (1, 0, 0)⟩`

(E-Not-False) If ⟨e, R⟩ ⇓ ⟨B0, R’⟩, then `⟨not(e), R⟩ ⇓ ⟨B1, R’ + (1, 0, 0)⟩`

## A.4 Comparison Rules

(E-Eq-Zero) `⟨eq(0, 0), R⟩ ⇓ ⟨B1, R + (1, 0, 0)⟩`

(E-Eq-Succ) If ⟨e1, R⟩ ⇓ ⟨S(v1), R1⟩, ⟨e2, R1⟩ ⇓ ⟨S(v2), R2⟩, `⟨eq(v1, v2), R2⟩ ⇓ ⟨v3, R3⟩, then `⟨eq(S(e1), S(e2)), R⟩ ⇓ ⟨v3, R3 + (1, 0, 0)⟩`

(E-Eq-Diff) If ⟨e1, R⟩ ⇓ ⟨v1, R1⟩, ⟨e2, R1⟩ ⇓ ⟨v2, R2⟩, and structure(v1) ≠ structure(v2), then `⟨eq(e1, e2), R⟩ ⇓ ⟨B0, R2 + (1, 0, 0)⟩`

\[Rules for lt, le, gt, ge follow the same structure.\]

## A.5 Guard and Error Rules

(E-Guard-Steps) If R.steps ≥ max_steps, then `⟨e, R⟩ ⇓ ⟨error(“E003”), R⟩`

(E-Guard-Stack) If R.stack_depth ≥ max_stack_depth, then `⟨e, R⟩ ⇓ ⟨error(“E002”), R⟩`

(E-Guard-Nat) If depth(S(v)) > max_nat_size, then `⟨S(e), R⟩ ⇓ ⟨error(“E201”), R⟩`

(E-Error-Prop) If ⟨e1, R⟩ ⇓ ⟨error(msg), R’⟩, then `⟨op(e1, e2), R⟩ ⇓ ⟨error(msg), R’⟩`