Program Logics via Distributive Monoidal Categories

Bonchi, Di Lavore, Román, Staton · 2025 · arxiv arXiv:2507.18238

Every Hoare rule you learned in your algorithms course — SKIP, COMP, WHILE, ASSIGN — is a theorem, not an axiom, once your category has the right structure.

The Hoare triple

You already know this pattern:

assert P; run(c); assert Q

"If P holds before running c, then Q holds after." That's a Hoare triple: {P} c {Q}. If the precondition doesn't hold, the triple says nothing — it's vacuously satisfied.

Python

# {P} c {Q} — if P holds before, Q holds after.

P = lambda x: x > 0
c = lambda x: x * 2
Q = lambda y: y > 0

for x in range(-3, 4):
    if P(x):
        result = c(x)
        assert Q(result), f"Failed: {x} -> {result}"
        print(f"  x={x} -> {result}: Q holds ✓")
    else:
        print(f"  x={x}: P doesn't hold, triple says nothing")

SKIP — doing nothing preserves anything

The simplest rule. {P} skip {P}. If P is true before doing nothing, P is still true after. Obvious — but it's a theorem, not an assumption.

Python

# SKIP: {P} skip {P}
skip = lambda x: x

P = lambda x: x > 0
for x in [1, 5, 100]:
    assert P(skip(x)) == P(x)
    print(f"  skip({x}): P preserved ✓")

print()
print("Nothing happened. That's the point.")

COMP — the handshake

This is the big one. If {P} c₁ {R} and {R} c₂ {Q}, then {P} c₁;c₂ {Q}.

R is the handshake — stage 1's postcondition is stage 2's precondition. The output guarantee of one stage is the input assumption of the next.

Python

# COMP: {P} c1 {R} and {R} c2 {Q} implies {P} c1;c2 {Q}
# R is the handshake.

double = lambda x: x * 2     # {x > 0} double {y > 0}
sub1 = lambda y: y - 1        # {y > 1} sub1 {z > 0}
pipeline = lambda x: sub1(double(x))

print("COMP: {x > 0} double;sub1 {z > 0}")
print()
for x in range(1, 6):
    y = double(x)
    z = pipeline(x)
    print(f"  x={x} -> y={y} (R: y>1? {y > 1}) -> z={z} (Q: z>0? {z > 0})")

print()
print("Try: change sub1 to 'lambda y: y - 5'")
print("     and see where Q breaks.")

WHILE — loop invariants

If {b ∧ P} c {P}, then {P} while b do c {P ∧ ¬b}.

If the body preserves the invariant P, the loop preserves it too. When the loop exits, P still holds AND the guard b is false. This is the loop invariant from your algorithms class — except here it's a theorem derived from the categorical structure, not a proof technique you choose to apply.

Python

# WHILE: if body preserves P, loop preserves P.
# When loop exits: P holds AND guard is false.

# Invariant P: x >= 0
# Guard b: x > 0
# Body c: x - 1

x = 10
print(f"  start: x={x}, P (x>=0): {x >= 0}")

while x > 0:
    x = x - 1
    assert x >= 0, "Invariant broken!"

print(f"  end:   x={x}, P (x>=0): {x >= 0}, b (x>0): {x > 0}")
print(f"  P ∧ ¬b: x>=0 and not x>0 → x==0 ✓")
print()
print("Try: change the body to 'x = x - 3'")
print("     Does the invariant still hold?")

Weakest precondition

Flip the question. Given c and Q, what's the weakest P that guarantees Q? That's wp(c, Q). The most permissive input condition that still gives you the output you want.

Python

# wp(c, Q) = the weakest P such that {P} c {Q}

c = lambda x: x - 3
Q = lambda y: y >= 0

# What inputs make Q hold after c?
# y = x - 3 >= 0  means  x >= 3
# So wp(c, Q) = lambda x: x >= 3

wp = lambda x: x >= 3

print("wp(subtract_3, non_negative) = x >= 3")
print()
for x in range(0, 8):
    result = c(x)
    ok = Q(result)
    predicted = wp(x)
    match = "✓" if predicted == ok else "✗"
    print(f"  x={x}: wp={predicted}, Q(c(x))={ok}  {match}")

Copy and discard — the structure underneath

An imperative category has two special operations per type: copy (ν) and discard (ε). A morphism is deterministic if it commutes with copy. This is how Fritz (2020) distinguishes deterministic from stochastic morphisms.

Python

# Copy: ν(x) = (x, x) — duplicate the state
# Discard: ε(x) = None — throw it away

# A function f is DETERMINISTIC if:
#   f(copy(x)) == copy(f(x))
#   "apply then copy" = "copy then apply to both"

copy = lambda x: (x, x)

double = lambda x: x * 2
x = 5
lhs = copy(double(x))
rhs = (double(x), double(x))
print(f"  double is deterministic:")
print(f"    copy(double({x})) = {lhs}")
print(f"    (double({x}), double({x})) = {rhs}")
print(f"    equal? {lhs == rhs} ✓")
print()

# Stochastic functions FAIL this test
import random
def coin(x):
    return x if random.random() > 0.5 else -x

results = set()
for _ in range(20):
    a, b = coin(5), coin(5)
    results.add((a, b))
print(f"  coin is stochastic:")
print(f"    20 independent (coin(5), coin(5)) pairs:")
print(f"    got {len(results)} distinct results")
print(f"    deterministic would give 1 ✗")

The bridge — contracts ARE Hoare triples

The Lean artifact proves the equivalence:

-- Lean 4
theorem contract_is_triple :
ContractPreserving f Q ↔ Triple (fun _ => True) f Q

ContractPreserving f Q says: for every input, every output in the support of f satisfies Q. That's {⊤} f {Q} — a Hoare triple where the precondition is "true" (anything goes). The contract is an unconditional guarantee.

Python

# ContractPreserving f Q  =  {⊤} f {Q}
# They're the same thing.

support = lambda d: {k for k, v in d.items() if v > 0}

contract_ok = lambda f, Q, xs: all(
    Q(y) for x in xs for y in support(f(x))
)

hoare_top_Q = lambda f, Q, xs: all(  # {⊤} f {Q}
    Q(y) for x in xs for y in support(f(x))
)

# Same function, same check, same result.
f = lambda x: {abs(x): 0.7, abs(x)+1: 0.3}
Q = lambda y: y >= 0

assert contract_ok(f, Q, range(-5, 6))
assert hoare_top_Q(f, Q, range(-5, 6))
print("Both passed — they're the same check.")
print()
print("ContractPreserving f Q  ↔  {⊤} f {Q}")
print("That's the bridge theorem.")

Lean proof

theorem contract_is_triple [Monad M] [Support M]
    {f : Kernel M α β} {Q : Contract β}
    : ContractPreserving f Q ↔ Triple (fun _ => True) f Q

Bridge.lean

Confidence: Exact.

The punchline — Corollary 76

Stoch (stochastic matrices) is a posetal imperative category. That means every Hoare rule in Section 5 holds there as a theorem. Hoare triples aren't an engineering choice — they're forced by the category.

A stochastic function takes an input and returns a probability distribution over outputs. Kleisli composition chains two such functions: run the first, then for each possible output run the second, weighting by probability. This is how stochastic pipelines compose — and it's the composition that makes the COMP rule work.

Python

# Stoch = Kleisli category of the subdistribution monad
# Morphisms are stochastic functions: X -> Distribution(Y)

f = lambda x: {x: 0.7, x+1: 0.3}      # 70% stay, 30% increment
g = lambda y: {y*2: 1.0}                # always double

# Kleisli composition: marginalize the intermediate
kleisli = lambda f, g: lambda x: {
    z: sum(py * g(y).get(z, 0) for y, py in f(x).items())
    for z in {z for y in f(x) for z in g(y)}
}

h = kleisli(f, g)
print(f"  f(3) = {dict(sorted(f(3).items()))}")
print(f"  g(3) = {dict(sorted(g(3).items()))}")
print(f"  (f >=> g)(3) = {dict(sorted(h(3).items()))}")
print()
print("This composition is what makes COMP work for")
print("stochastic pipelines. The handshake chains")
print("through the bind — same as your Lean proof.")

Lean proof

theorem forward_triple [Monad M] [LawfulMonad M] [Support M]
    {I : InterfaceTypes} {p : Pipeline M I}
    (t : PipelineTriples M I p) (policy : I.policy)
    : Triple t.P_raw (p.forwardKernel policy) t.Q_ranked :=
  four_stage_comp t.h_perceive t.h_cache t.h_filter (t.h_attend policy)

Comp.lean

Confidence: Simplified. Finite dicts, not measurable spaces. Same composition law.

Notation reference

Paper	Python	Meaning
{P} c {Q}	assert P; c(); assert Q	Hoare triple
c₁ ; c₂	c2(c1(x))	Sequential composition
⊤	lambda _: True	Always true
⊥	lambda _: False	Always false
wp(c, Q)	lambda a: all(Q(b) for b in c(a))	Weakest precondition
ν	lambda x: (x, x)	Copy
ε	lambda x: None	Discard
≤	# refinement	One program refines another
kl(T)	# functions returning T(...)	Kleisli category
⊗	(x, y)	Tensor (parallel)

Rules reference (Theorem 79)

Every rule is a theorem in any posetal imperative category. Stoch is one (Corollary 76).

Rule	Statement	Plain English
SKIP	{P} skip {P}	Doing nothing preserves anything
COMP	{P}c₁{R}, {R}c₂{Q} ⇒ {P}c₁;c₂{Q}	Chain postconditions. The handshake.
WHILE	{b∧P} c {P} ⇒ {P} while b do c {P∧¬b}	Loop invariant survives
AND	{P₁}c{Q₁}, {P₂}c{Q₂} ⇒ {P₁∧P₂}c{Q₁∧Q₂}	Conjunction of specs is a spec
TOP	{P} c {⊤}	Anything satisfies "true"
BOT	{⊥} c {Q}	Impossible precondition → vacuously true

Neighbors

Other paper pages

🍞 Fritz 2020 — the category (FinStoch) where these rules hold
🍞 Gaboardi 2021 — Hoare triples with grades (track side effects)
🍞 Kura 2026 — the restricted pointwise order (handshake as graded monad)

Foundations (Wikipedia)

Translation notes

All Python examples on this page use finite dicts as probability distributions. The paper works over arbitrary measurable spaces, continuous distributions, and the full subdistribution monad on StdBorel. For example: the WHILE rule on this page counts down from 10 to 0 using integers. In the paper, the same rule applies to a probabilistic loop over continuous state spaces — a particle filter updating a belief distribution until convergence. The invariant structure (P survives each iteration) is identical. The state space is not.

The bridge theorem section is tagged Exact — the Python computes the same equivalence the Lean proof verifies. Every other example is Simplified.

Framework connection: Stoch is the ambient category for the Natural Framework pipeline; the COMP rule is the handshake between stages. (Ambient Category, The Handshake)

Ready for the real thing? arxiv

Read the paper (52 pages). Start at Section 5.1 (p.20) for correctness triples, Corollary 76 (p.19) for why Stoch qualifies.

by june.kim Fritz 2020 · 2 of 21 →