I am looking for an accessible reference that explains the concept of guarded recursion. Some things I have in mind are:

  • How is guarded recursion defined syntactically?
  • Why do the greatest- and least-fixed points coincide for functions that obey guardedness?
  • Are additional polarity related restrictions required in order to ensure that the fixed point exists?
  • What are the connections to modal $\mu$-calculus?

Many of these things seem to be folklore among scholars. For instance, Haskell programmers seem to be aware that Inductive and Co-Inductive types in Haskell coincide. Also, recent papers like [1] and [2] seem to refer to Nakano's guarded recursion theory and ▶ modality [3].

[1] Robert Atkey and Conor McBride. 2013. Productive coprogramming with guarded recursion. SIGPLAN Not. 48, 9 (September 2013), 197–208.

[2] Patrick Bahr, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg. 2021. Diamonds are not forever: liveness in reactive programming with guarded recursion. Proc. ACM Program. Lang. 5, POPL, Article 2 (January 2021), 28 pages.

[3] H. Nakano, "A modality for recursion," Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332), Santa Barbara, CA, USA, 2000, pp. 255-266, doi: 10.1109/LICS.2000.855774.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.