Weakest Preconditions in Fibrations

Bart Jacobs · 2014 · preprint

Prereqs: 🍞 Staton 2025 (Hoare triples, weakest precondition). 🍞 Fritz 2020 (Kleisli categories) helps.

Weakest preconditions arise automatically from a fibration over a Kleisli category. The poset of predicates sitting above each type is the fiber; lifting a morphism through the fibration computes wp.

Predicates as a poset fibration

Above each type X sits a poset of predicates on X — propositions ordered by implication. "x > 5" implies "x > 0", so "x > 5" sits above "x > 0" in the fiber over integers. A fibration is this layered structure: types on the bottom, predicates stacked above, ordered by strength.

Scheme

; Fiber over integers: predicates ordered by implication
; P ≤ Q means P implies Q (P is stronger)

(define (implies? P Q domain)
  (every (lambda (x) (or (not (P x)) (Q x))) domain))

(define P (lambda (x) (> x 5)))
(define Q (lambda (x) (> x 0)))
(define R (lambda (x) (> x 10)))

(define dom '(-3 0 1 5 6 10 11 20))

(display "P(x>5) => Q(x>0)? ")
(display (implies? P Q dom)) (newline)
(display "R(x>10) => P(x>5)? ")
(display (implies? R P dom)) (newline)
(display "Q(x>0) => P(x>5)? ")
(display (implies? Q P dom)) (newline)
; R ≤ P ≤ Q in the fiber — stronger to weaker

Lifting through the Kleisli category

A stochastic function f: X → D(Y) lives in the Kleisli category of the distribution monad. To compute wp(f, Q), you lift the predicate Q on Y back through f: for each input x, check whether every possible output satisfies Q.

Scheme

; wp(f, Q)(x) = for all y in support(f(x)), Q(y)
; Lifting Q backwards through the Kleisli morphism f

(define (wp f Q)
  (lambda (x)
    (every (lambda (pair) (Q (car pair)))
           (filter (lambda (pair) (> (cdr pair) 0))
                   (f x)))))

; f: x -> {x-1: 0.5, x+1: 0.5}
(define (f x)
  (list (cons (- x 1) 0.5) (cons (+ x 1) 0.5)))

(define Q (lambda (y) (>= y 0)))

(define P (wp f Q))

(display "wp(f, y>=0):") (newline)
(for-each (lambda (x)
  (display "  x=") (display x)
  (display " -> ") (display (P x)) (newline))
  '(-1 0 1 2 3))
; x=0 is false: f(0) can produce -1
; x=1 is true: f(1) produces {0, 2}, both >= 0

Order enrichment makes wp monotone

The fibers are posets (predicates ordered by implication). The wp functor is monotone: if Q₁ implies Q₂, then wp(f, Q₁) implies wp(f, Q₂). Stronger postconditions give stronger preconditions. This monotonicity comes for free from the order-enriched Kleisli structure.

Scheme

; Monotonicity: Q1 => Q2 implies wp(f,Q1) => wp(f,Q2)

(define (wp f Q)
  (lambda (x)
    (every (lambda (pair) (Q (car pair)))
           (filter (lambda (pair) (> (cdr pair) 0))
                   (f x)))))

(define (f x) (list (cons (- x 1) 0.5) (cons (+ x 1) 0.5)))

; Q1 is stronger than Q2
(define Q1 (lambda (y) (> y 5)))
(define Q2 (lambda (y) (> y 0)))

(define P1 (wp f Q1))
(define P2 (wp f Q2))

(display "monotonicity check:") (newline)
(for-each (lambda (x)
  (display "  x=") (display x)
  (display " P1=") (display (P1 x))
  (display " P2=") (display (P2 x))
  (display (if (and (P1 x) (not (P2 x))) " VIOLATION" ""))
  (newline))
  '(0 1 3 5 6 7 8))
; P1(x) => P2(x) always — no violations

Composition of wp via Kleisli composition

wp(f;g, Q) = wp(f, wp(g, Q)). Composing two stochastic functions and computing wp in one step gives the same result as computing wp for g first, then using that as the postcondition for f. The fibration structure guarantees this — it's not a coincidence, it's functoriality.

Scheme

; wp(f;g, Q) = wp(f, wp(g, Q))
; Functoriality of the fibration

(define (wp f Q)
  (lambda (x)
    (every (lambda (pair) (Q (car pair)))
           (filter (lambda (pair) (> (cdr pair) 0))
                   (f x)))))

(define (kleisli f g)
  (lambda (x)
    (apply append
      (map (lambda (pair)
        (let ((y (car pair)) (py (cdr pair)))
          (map (lambda (qp) (cons (car qp) (* py (cdr qp))))
               (g y))))
      (f x)))))

(define (f x) (list (cons (+ x 1) 0.5) (cons (+ x 2) 0.5)))
(define (g y) (list (cons (* y 2) 1.0)))
(define Q (lambda (z) (> z 5)))

(define direct (wp (kleisli f g) Q))
(define staged (wp f (wp g Q)))

(display "wp(f;g, Q) = wp(f, wp(g, Q)):") (newline)
(for-each (lambda (x)
  (display "  x=") (display x)
  (display " direct=") (display (direct x))
  (display " staged=") (display (staged x)) (newline))
  '(0 1 2 3 4))

Notation reference

Paper	Scheme	Meaning
Pred(X)	(lambda (x) ...)	Fiber: predicates on X
P ≤ Q	(implies? P Q dom)	P implies Q (stronger precondition)
wp(f, Q)	(wp f Q)	Weakest precondition via lifting
Kl(D)	; Kleisli(Distribution)	Kleisli category of distribution monad
p*	(wp f ...)	Reindexing functor (pullback along f)

Neighbors

Other paper pages

🍞 Staton 2025 — Hoare rules as theorems in imperative categories (uses wp)
🍞 Cho, Jacobs 2015 — effectus theory (same author, predicates as effects)
🍞 Ho, Wu 2026 — Bayesian separation logic (wp for probabilistic programs)

Foundations (Wikipedia)

Translation notes

All examples use finite distributions and boolean predicates. Jacobs works with order-enriched categories, where predicates form complete lattices and the fibration carries a rich adjunction structure (left and right adjoints to reindexing). For example: the wp computation on this page checks all elements of a small support set. In the paper, wp is a right adjoint to substitution in the fibration — a universal construction that works over arbitrary effect monads, not just distributions. The pointwise "for all y" check is the same; the categorical machinery that guarantees it exists is not.

Every example is Simplified.

Ready for the real thing? Start at §3 for the fibration of predicates over Kleisli categories, §5 for the wp-semantics.

Framework connection: The fibration-based wp construction is the theoretical backbone for computing weakest preconditions in the Natural Framework's ambient Kleisli category. (Ambient Category)

← Spivak 2013 · 11 of 21 by june.kim Kidney, Wu 2021 · 13 of 21 →