Prereqs: ๐ Fritz 2020 (Markov categories, support). 5 min.
The map "which outcomes are possible?", dropping weights and keeping only the support, is a monad morphism. It respects composition: the support of a composed pipeline equals the composition of supports.
The possibilistic shadow
Every probability distribution has a possibilistic shadow: forget the weights, keep only which outcomes can happen. This maps the probability monad P to the powerset monad ๐ซ. The shadow is a monad morphism: it preserves pure and bind.
Scheme
; The possibilistic shadow: P -> powerset; Drop probabilities, keep reachable outcomes
(define (support dist)
(map car (filter (lambda (p) (> (cdr p) 0)) dist)))
(define dist1
'((a . 0.5) (b . 0.3) (c . 0.2)))
(define dist2
'((a . 0.99) (b . 0.005) (c . 0.005)))
(display "dist1 shadow: ") (display (support dist1)) (newline)
(display "dist2 shadow: ") (display (support dist2)) (newline)
; dist1 and dist2 have the same shadow โ different probabilities, same reachability
Python
# Possibilistic shadow in Pythondef support(dist):
return {k for k, v in dist.items() if v > 0}
dist1 = {"a": 0.5, "b": 0.3, "c": 0.2}
dist2 = {"a": 0.99, "b": 0.0, "c": 0.01}
print("dist1 shadow:", support(dist1))
print("dist2 shadow:", support(dist2))
support_pure โ pure maps to singleton
The pure (return) of the probability monad places all mass on one value: pure(x) = {x: 1.0}. Its shadow is a singleton set, {x}, which is exactly the pure of the powerset monad. So support preserves pure.
Confidence: Exact. This is the unit law for the monad morphism.
support_bind โ support commutes with bind
This is the key theorem. Compose two stochastic functions, then take the support: you get the same result as taking each support first and composing the set-valued functions. In notation: supp(f >=> g) = supp(f) >=>_๐ซ supp(g). Support preserves the monad multiplication.
Scheme
; support_bind: supp(f >=> g) = supp(f) >=> supp(g); "Support of composed = compose of supports"
(define (support dist) (map car (filter (lambda (p) (> (cdr p) 0)) dist)))
(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)))))
; Set-valued compose: union of g applied to each element
(define (set-compose sf sg)
(lambda (x)
(apply append (map sg (sf x)))))
(define (f x) (list (cons 'a 0.6) (cons 'b 0.4)))
(define (g y) (if (eq? y 'a)
(list (cons 10.5) (cons 20.5))
(list (cons 20.3) (cons 30.7))))
; Path 1: compose then support
(define path1 (support ((kleisli f g) 'start)))
; Path 2: support then set-compose
(define sf (lambda (x) (support (f x))))
(define sg (lambda (y) (support (g y))))
(define path2 ((set-compose sf sg) 'start))
(display "compose then support: ") (display path1) (newline)
(display "support then compose: ") (display path2) (newline)
; Same elements โ support is a monad morphism
Confidence: Simplified. Finite sets, not measurable spaces. Same algebraic law.
Python
# support_bind in Pythondef support(d): return {k for k,v in d.items() if v > 0}
def kleisli(f, g):
def h(x):
r = {}
for y, py in f(x).items():
for z, pz in g(y).items():
r[z] = r.get(z, 0) + py * pz
return r
return h
def f(x): return {"a": 0.6, "b": 0.4}
def g(y): return {1: 0.5, 2: 0.5} if y == "a"else {2: 0.3, 3: 0.7}
# Path 1: compose then support
path1 = support(kleisli(f, g)("start"))
# Path 2: support then union-composedef set_comp(sf, sg):
def h(x):
returnset().union(*(sg(y) for y in sf(x)))
return h
path2 = set_comp(lambda x: support(f(x)), lambda y: support(g(y)))("start")
print(f"compose then support: {path1}")
print(f"support then compose: {path2}")
print(f"equal? {path1 == path2}")
Why possibilistic reasoning is sound
Because support is a monad morphism, you can reason about reachability (what can happen) without tracking exact probabilities. If a state is unreachable through a composed system, it's unreachable through each stage individually. Possibilistic gating, rejecting impossible outcomes, needs no exact probability computation.
Scheme
; Possibilistic gating: reject impossible, keep possible; No probabilities needed โ support is enough
(define (support dist) (map car (filter (lambda (p) (> (cdr p) 0)) dist)))
(define (sensor x)
(cond ((eq? x 'cat) '((meow . 0.8) (silence . 0.2)))
((eq? x 'dog) '((bark . 0.7) (silence . 0.3)))
(else '((silence . 1.0)))))
; Possibilistic filter: can this observation come from this source?
(define (possible? source observation)
(member observation (support (sensor source))))
(display "cat->meow? ") (display (if (possible? 'cat 'meow) "yes""no")) (newline)
(display "dog->meow? ") (display (if (possible? 'dog 'meow) "yes""no")) (newline)
(display "cat->silence? ") (display (if (possible? 'cat 'silence) "yes""no")) (newline)
; Meow rules out dog. Silence rules out nothing.; No probabilities needed for this gate.
Python
# Possibilistic gating in Pythondef support(d): return {k for k, v in d.items() if v > 0}
def sensor(x):
if x == "cat": return {"meow": 0.8, "silence": 0.2}
if x == "dog": return {"bark": 0.7, "silence": 0.3}
return {"silence": 1.0}
for src in ["cat", "dog", "rock"]:
for obs in ["meow", "bark", "silence"]:
ok = obs in support(sensor(src))
if ok: print(f" {src} -> {obs}: possible")
The monad morphism square
A monad morphism ฯ: T โ S satisfies two laws: ฯ โ ฮท_T = ฮท_S (preserve pure) and ฯ โ ฮผ_T = ฮผ_S โ (ฯฯ) (preserve multiplication). Support satisfies both. The first says "point mass โ singleton." The second says "support of bind = bind of supports."
Scheme
; Monad morphism laws for support; Law 1: sigma . eta_T = eta_S (pure); Law 2: sigma . mu_T = mu_S . (sigma x sigma) (mult)
(define (support d) (map car (filter (lambda (p) (> (cdr p) 0)) d)))
; Law 1: support(point-mass(x)) = singleton(x)
(define (check-pure x)
(equal? (support (list (cons x 1.0)))
(list x)))
(display "Law 1 (pure): ")
(display (and (check-pure 'a) (check-pure 'b) (check-pure 42)))
(newline)
; Law 2: flatten-then-support = support-each-then-union
(define nested '(((a . 0.3) (b . 0.7)) ((b . 0.5) (c . 0.5))))
(define flat (apply append nested))
(define path1 (support flat))
(define path2 (apply append (map support nested)))
(display "Law 2 (mult): ") (display (equal? path1 path2))
; Both laws hold โ support is a monad morphism
Confidence: Exact. These are the defining equations, computed over finite lists.
All examples use finite lists of pairs as distributions. The paper works over arbitrary measurable spaces with the Giry monad, and support becomes a measurable map between ฯ-algebras. The support_bind demo above composes two functions over small symbol sets; in the paper, the same law applies to Markov kernels between Polish spaces โ where "support" means topological support of a probability measure, and the proof requires measurable selection theorems. The algebraic structure is identical. The measure theory is not.
Ready for the real thing? Read the paper. Start at ยง3 for the support monad morphism, ยง4 for the bimonadality result.
Framework connection: The possibilistic shadow justifies the Natural Framework's Filter stage gating on reachability without exact probabilities. (Ambient Category)
arXiv:1910.03752
Polish spaces โ where "support" means topological support of a probability measure, and the proof requires measurable selection theorems. The algebraic structure is identical. The measure theory is not.
Ambient Category)