Introduction to Effectus Theory

Kenta Cho & Bart Jacobs · 2015 · arxiv arXiv:1512.05813

Prereqs: 🍞 Fritz 2020 (Markov categories). Basic probability (what a distribution is).

A predicate on X is a morphism X → 1+1 — a "fuzzy test" that returns yes with some probability. States and effects (predicates) are dual: a state picks a point, an effect tests it. This duality gives you the Born rule for free — probability = state applied to effect.

Effects as fuzzy predicates

In classical logic, a predicate is a function X → 1: either true or false. An effect generalizes this to X → [0,1]: a fuzzy test that returns "yes" with some probability. In the categorical setting, this is a morphism X → 1+1 (the coproduct of two terminal objects).

Scheme

; An effect: X -> [0,1] — fuzzy predicate
; Classical predicate: always 0 or 1
; Effect: can be any probability

(define (classical-even? x)
  (if (even? x) 1 0))

(define (fuzzy-big x)
  ; How "big" is x? Gradually increases
  (min 1.0 (max 0.0 (/ x 10.0))))

(display "classical-even:") (newline)
(for-each (lambda (x)
  (display "  ") (display x) (display " -> ")
  (display (classical-even? x)) (newline))
  '(1 2 3 4 5))

(display "fuzzy-big:") (newline)
(for-each (lambda (x)
  (display "  ") (display x) (display " -> ")
  (display (fuzzy-big x)) (newline))
  '(0 3 5 8 10 15))

States — dual to effects

A state on X is a morphism 1 → D(X) — a distribution over X. States pick points (probabilistically). Effects test points (fuzzily). They're dual: pairing a state with an effect gives a probability.

Scheme

; State: 1 -> D(X) — a distribution
; Effect: X -> [0,1] — a fuzzy test
; Pairing: state(effect) = expected value = probability

(define (make-state dist) dist)
(define (make-effect test) test)

(define state '((1 . 0.2) (2 . 0.3) (3 . 0.5)))
(define effect (lambda (x) (if (> x 2) 1.0 0.0)))

; Pairing: sum_x state(x) * effect(x)
(define (pair state effect)
  (apply + (map (lambda (p)
    (* (cdr p) (effect (car p))))
  state)))

(display "state: ") (display state) (newline)
(display "effect: x > 2") (newline)
(display "P(x > 2) = ") (display (pair state effect))
; 0.5 — the probability that x > 2 under this state

The Born rule

The pairing of state and effect is the Born rule: probability = ⟨state | effect⟩. In quantum mechanics, this is |⟨ψ|φ⟩|². In the effectus framework, it's the categorical pairing. Classical probability and quantum probability are both instances.

Scheme

; Born rule: probability = <state | effect>
; Classical version: expected value of effect under state
; Quantum version: |<psi|phi>|^2

(define (born-rule state effect)
  (apply + (map (lambda (p)
    (* (cdr p) (effect (car p))))
  state)))

; State: uniform over {1,2,3,4}
(define uniform '((1 . 0.25) (2 . 0.25) (3 . 0.25) (4 . 0.25)))

; Effect 1: is it even?
(define even-effect (lambda (x) (if (even? x) 1.0 0.0)))
; Effect 2: how close to 3?
(define near-3 (lambda (x) (max 0 (- 1.0 (/ (abs (- x 3)) 3.0)))))

(display "P(even) = ") (display (born-rule uniform even-effect)) (newline)
(display "P(near 3) = ") (display (born-rule uniform near-3)) (newline)
; Both computed by the same pairing. Born rule unifies them.

Effect algebra

Effects on X form an effect algebra: you can add effects (if they don't exceed 1), negate them (1 - e), and the constant effects 0 and 1 are the extremes. This structure is weaker than a Boolean algebra — you can't always form e ∧ f — which is exactly the non-classical part of quantum logic.

Scheme

; Effect algebra operations
; Negation: 1 - e
; Partial addition: e + f (defined when e + f <= 1)

(define (effect-neg e)
  (lambda (x) (- 1.0 (e x))))

(define (effect-add e1 e2)
  ; Only defined when e1(x) + e2(x) <= 1 for all x
  (lambda (x) (+ (e1 x) (e2 x))))

(define e (lambda (x) 0.3))
(define not-e (effect-neg e))
(define zero (lambda (x) 0.0))
(define one (lambda (x) 1.0))

(display "e(5) = ") (display (e 5)) (newline)
(display "not-e(5) = ") (display (not-e 5)) (newline)
(display "(e + not-e)(5) = ")
(display ((effect-add e not-e) 5)) (newline)
; e + not-e = 1 always. Effect algebra axiom.

Notation reference

Paper	Scheme	Meaning
1 + 1	; two outcomes, [0,1]	Two-element coproduct (test outcomes)
Eff(X) = X → 1+1	(lambda (x) ...)	Effect (fuzzy predicate)
Stat(X) = 1 → X	'((val . prob) ...)	State (distribution)
⟨ω\|p⟩	(born-rule state effect)	Born rule (state-effect pairing)
p⊥	(effect-neg p)	Effect negation (1 − p)

Neighbors

Other paper pages

🍞 Fritz 2020 — the Markov category where effects live
🍞 Parzygnat 2020 — quantum Markov categories (where effects are non-commutative)
🍞 Jacobs 2014 — weakest preconditions as lifted predicates (same author)
🍞 Di Lavore 2025 — partial Markov categories (effects and observations)

Foundations (Wikipedia)

Translation notes

All examples use classical probability (effects are functions to [0,1], states are finite distributions). Cho and Jacobs work in the general setting of effectus categories, which includes quantum probability (effects are positive operators bounded by the identity, states are density matrices). For example: the Born rule on this page computes an expected value via a weighted sum. In the quantum case, the same pairing is tr(ρE) — the trace of a density matrix times a positive operator. The pairing structure is identical. The algebraic setting (commutative vs non-commutative) is not.

Every example is Simplified — classical stand-ins for a framework that covers both classical and quantum.

Ready for the real thing? arxiv

Read the paper. Start at §2 for effectus categories, §4 for states and effects, §6 for the Born rule.

Framework connection: Effects as fuzzy predicates model the Natural Framework's Filter stage — a probabilistic gate that passes or blocks data. (The Natural Framework)

← Panangaden 2009 · 18 of 21 by june.kim Ho, Wu 2026 · 20 of 21 →