Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
DOI
Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebras with a well-founded basis.
In this paper we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq proof assistant. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it — presheaves are more amenable to mechanization in a proof assistant.
The bibtex source for this publication:
@InProceedings{10.4230/LIPIcs.FSCD.2025.30,
author="Stepanenko, Sergei and Timany, Amin",
editor="Maribel Fern\'{a}ndez",
title="Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It",
booktitle="10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)",
year="2025",
publisher="Leibniz International Proceedings in Informatics",
pages="30:1–30:24",
abstract="Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebras with a well-founded basis.
In this paper we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq proof assistant. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it — presheaves are more amenable to mechanization in a proof assistant."
}