Support.lean

View source on GitHub

Support

A typeclass that maps any monadic computation M a to a yes/no predicate on a: "can this value come out?" For probability distributions, this is the support of the measure. For plain deterministic functions (Id), the support is a single value.

class Support (M : Type → Type) [Monad M] where
  support : {α : Type} → M α → α → Prop
  support_pure : ∀ {α : Type} (a x : α),
    support (pure a) x ↔ x = a
  support_bind : ∀ {α β : Type} (m : M α) (f : α → M β) (y : β),
    support (bind m f) y ↔ &exists; x, support m x ∧ support (f x) y

Three pieces: the predicate itself, a law for pure (wrapping a value produces exactly that value), and a law for bind (chaining two computations — y is reachable from m >>= f iff some intermediate x is reachable from m and y is reachable from f applied to x). These two laws mirror the monad laws, but for reachability instead of computation.

instance : Support Id

The deterministic case. When the monad is Id (no randomness, no effects), the only possible output is the actual output. This recovers ordinary functions as a special case.

instance : Support Id where
  support := fun {α} (m : Id α) (x : α) => x = m
  support_pure := by
    intro α a x; constructor
    · intro h; exact h
    · intro h; exact h
  support_bind := by
    intro α β m f y; constructor
    · intro h; exact ⟨m, rfl, h⟩
    · intro ⟨x, hx, hy⟩; rw [hx] at hy; exact hy

The proofs are simple: pure in Id is the identity, so its support is trivially a singleton. bind in Id is function application, so the only intermediate is the value itself.

; Support = which outputs are reachable
; A deterministic function has support {f(x)}.
; A stochastic function has support = all possible outputs.

(define (det-support f x)
  (list (f x)))  ; exactly one possible output

(define (stoch-support f x)
  (f x))  ; returns the full list of possibilities

(define (double x) (* x 2))
(define (coin-flip x) (list x (- x)))  ; two outcomes

(display "det support of double(3): ")
(display (det-support double 3))
(newline)
(display "stoch support of coin-flip(5): ")
(display (stoch-support coin-flip 5))
(newline)
(display "bind: for each y in support(f(x)),")
(display " collect support(g(y))")
(newline)
(define (bind-support sf sg x)
  (apply append (map (lambda (y) (sg y)) (sf x))))
(display "support(coin-flip >>= coin-flip)(3): ")
(display (bind-support
  (lambda (x) (coin-flip x))
  (lambda (y) (coin-flip y)) 3))

# Support = which outputs are reachable
# A deterministic function has support {f(x)}.
# A stochastic function has support = all possible outputs.

def det_support(f, x):
    return [f(x)]  # exactly one possible output

def stoch_support(f, x):
    return f(x)  # returns the full list of possibilities

def double(x):
    return x * 2

def coin_flip(x):
    return [x, -x]  # two outcomes

print(f"det support of double(3): {det_support(double, 3)}")
print(f"stoch support of coin-flip(5): {stoch_support(coin_flip, 5)}")
print("bind: for each y in support(f(x)), collect support(g(y))")

def bind_support(sf, sg, x):
    return [z for y in sf(x) for z in sg(y)]

print(f"support(coin-flip >>= coin-flip)(3): {bind_support(coin_flip, coin_flip, 3)}")

Connections

• Kleisli.lean — uses Support to define morphisms between types
• Contracts.lean — contracts quantify over support: "every reachable output satisfies the postcondition"
• SupportMonadMorphism.lean — proves Support is a monad morphism to the reachability monad