Guarded Recursion

Origin. Hiroshi Nakano, "A modality for recursion" (LICS 2000), which introduced the later modality ▷ and its fixed-point combinator; Appel, Melliès, Richards, and Vouillon's "very modal model" (2007) connected it to step-indexing; Birkedal, Møgelberg, Schwinghammer, and Støvring's topos of trees (2011) gave the canonical model; Clouston, Bizjak, Grathwohl, and Birkedal (2015) added clocks for productivity.

Models. A recursive definition is safe if each unfolding makes progress. The later modality makes that a typing condition: ▷A is "an A, one step from now", and the fixed-point combinator has type (▷A → A) → A — you may define something recursively provided the recursive occurrence is guarded, available only later. Nakano's insight is that this is a modality with a frame semantics, so the productivity discipline of coinductive programming is intuitionistic modal logic.

Formalism.

The later modality: ▷A — an A available at the next step. next : A → ▷A ⊛ : ▷(A → B) → ▷A → ▷B (applicative action) ▷ is an applicative functor, not a comonad: there is no ▷A → A.

The fixed point: fix : (▷A → A) → A fix f ⇝ f (next (fix f)) The recursive occurrence is under ▷, so it cannot be used now — only guarded. Without ▷ the combinator would be Y and the system would be inconsistent.

Guarded streams: Str A ≅ A × ▷(Str A) The tail is available later. Definitions are productive by construction: ones = cons 1 (next ones) typechecks; ones = ones does not.

Topos of trees (Birkedal et al. 2011): Sh(ω) — presheaves on the ordinal ω. X(n) is the "n-step approximation". ▷ is the shift: (▷X)(0) = 1, (▷X)(n+1) = X(n). The topos validates Löb's rule, and ▷ is the intended semantics of the provability box.

Löb induction: (▷A → A) → A is exactly Löb's axiom □(□A → A) → □A, one modality down. Guarded recursion's fixed point is Löb's theorem read as a program. The connection to provability logic is exact and was not the motivation.

Clocks and coinduction (Atkey–McBride 2013, Clouston et al. 2015): Guarded types are too weak: one cannot escape ▷ to get a real coinductive type. Clock quantification ∀κ. A allows the guards to be discharged. ∀κ. Str^κ A is the genuine coinductive stream type.

Symbols.

Metatheory. That the guarded fixed point is Löb's axiom is the result worth the entry: a discipline invented to make coinductive definitions productive turns out to be the provability modality, and the topos of trees validates Löb because its objects are step-indexed approximations — which is why step-indexed models in program verification and provability logic keep converging without either side intending it. Iris's step-indexing is exactly this modality, which is why Iris Logic and this entry are the same idea at two scales. The clock machinery is the acknowledgment that guarded types alone are not enough: ▷ makes recursion safe and makes coinduction unreachable, and quantifying it away is the repair.

Applies to. Productive coinductive programming. Step-indexed models in separation logic — Iris and the very modal model. Functional reactive programming, where ▷ is the delay. Denotational semantics of recursive types. Provability logic, by the Löb correspondence.

Limitations. ▷ is an applicative functor and not a comonad, so it has no counit — one cannot get from ▷A to A, which is what makes the recursion safe and what makes the modality awkward everywhere else. Guarded types are not coinductive types, and the clock quantification that repairs this is heavy: reasoning about clock variables is a burden the underlying idea does not suggest. And the topos-of-trees model is elegant and non-classical, so intuitions calibrated on ordinary domains mislead.

© 2026 Lingenic LLC