nLab guarded recursion

Idea

Guarded recursion is a form of recursion that ensures that solutions of self-referential descriptions exist. This is achieved by “guarding” the recursive occurrence of the object under consideration using a unary modality $\blacktriangleright$ and pronounced “later”.

The later modality was first considered by Nakano (Nakano 2000) and used to ensure productivity of coinductively defined programs.

For example, for an object $A$, the type of guarded streams is the unique solution to the equation

$$\text{Str}_g A \cong A \times \blacktriangleright \text{Str}_g A$$

The intended meaning is that the head of the stream is available now while the tail is only available after one step of computation.

(There are other forms of guarded recursion which act through syntactic restriction.)

Related concepts

• synthetic guarded domain theory

References

• Robert Atkey, Conor McBride, Productive Coprogramming with Guarded Recursion, (Productive Coprogramming with Guarded Recursion)

• Aleš Bizjak, On Semantics and Applications of Guarded Recursion, (PhD thesis)

• Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, Lars Birkedal, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, (arXiv:1606.09455)

• Nakano Hiroshi, 2000, A Modality for Recursion. In Logic in Computer Science (LICS’00). (pdf)

• Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, Guarded cubical type theory arxiv

• Jon Sterling, Robert Harper, Guarded Computational Type Theory, LICS ‘18 (2018) 879–888 [arxiv:1804.09098, doi:10.1145/3209108.3209153]

A general calculus for dependent modal type theories.

• Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters, Modal Dependent Type Theory and Dependent Right Adjoints arxiv