Parametrized functors enable refined equivalence reasoning for software behaviors
Coinductive reasoning for parametrized functors and monads
Logic in Computer ScienceProgramming Languages
Summary
Comparing computer programs or systems usually involves checking if they behave the same in every possible situation. The authors develop a way to adjust what situations count by adding parameters to how these behaviors are compared. This lets programmers control the scope of comparison, making the process more flexible and precise. Their work uses advanced math tools called lax extensions to support these new forms of comparison.
What this means in practice
- •For programming language designers: Design type systems or semantics that allow controlled behavioral equivalences improving program correctness guarantees for effectful languages.
- •For software verification engineers: Develop more precise equivalence checks modulated by parameters to verify effectful and stateful software components.
A theory result. No direct application yet.
Authors
Ugo Dal Lago, Zeinab Galal
Abstract
Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.