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: propositions ordered by implication. "x > 5" implies "x > 0", so "x > 5" sits above "x > 0" in the fiber over integers. A fibration layers 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 '(-30156101120))
(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
Python
# Predicate fiber over integers
P = lambda x: x > 5
Q = lambda x: x > 0
R = lambda x: x > 10
domain = range(-5, 25)
def implies(P, Q, dom):
returnall(not P(x) or Q(x) for x in dom)
print(f"P(x>5) => Q(x>0)? {implies(P, Q, domain)}")
print(f"R(x>10) => P(x>5)? {implies(R, P, domain)}")
print(f"Q(x>0) => P(x>5)? {implies(Q, P, domain)}")
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))
'(-10123))
; x=0 is false: f(0) can produce -1; x=1 is true: f(1) produces {0, 2}, both >= 0
Python
# wp via Kleisli liftingdef f(x):
return {x - 1: 0.5, x + 1: 0.5}
Q = lambda y: y >= 0def wp(f, Q):
returnlambda x: all(Q(y) for y, p in f(x).items() if p > 0)
P = wp(f, Q)
for x inrange(-1, 4):
print(f" x={x}: wp={P(x)}, support(f)={list(f(x).keys())}")
Order enrichment makes wp monotone
The fibers are posets, so wp is monotone: if Qโ implies Qโ, then wp(f, Qโ) implies wp(f, Qโ). Stronger postconditions give stronger preconditions. The order-enriched Kleisli structure guarantees this.
# Monotonicity of wpdef f(x):
return {x - 1: 0.5, x + 1: 0.5}
def wp(f, Q):
returnlambda x: all(Q(y) for y, p in f(x).items() if p > 0)
Q1 = lambda y: y > 5# stronger
Q2 = lambda y: y > 0# weaker
P1, P2 = wp(f, Q1), wp(f, Q2)
for x inrange(0, 9):
ok = "ok"ifnot P1(x) or P2(x) else"VIOLATION"print(f" x={x}: P1={P1(x)}, P2={P2(x)} {ok}")
Composition of wp via Kleisli composition
wp(f;g, Q) = wp(f, wp(g, Q)). Computing wp of the composed pipeline in one shot gives the same answer as computing wp(g, Q) first and feeding it to wp(f, -). The fibration structure guarantees this. Not a coincidence: functoriality.
All examples use finite distributions and boolean predicates. Jacobs works with order-enriched categories where predicates form complete lattices and the fibration carries left and right adjoints to reindexing. 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 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)
fibration over a Kleisli category. The poset of predicates sitting above each type is the fiber; lifting a morphism through the fibration computes wp.
Ambient Category)