Restriction Spaces: a Fixed-Point Theory

Benoît Ballenghien 📧, Benjamin Puyobro 📧 and Burkhart Wolff 📧

May 7, 2025

Abstract

Fixed-point constructions are fundamental to defining recursive and co-recursive functions. However, a general axiom $Y f = f (Y f)$ leads to inconsistency, and definitions must therefore be based on theories guaranteeing existence under suitable conditions. In Isabelle/HOL, these constructions are typically based on sets, well-founded orders or domain-theoretic models such as for example HOLCF. In this submission we introduce a formalization of restriction spaces i.e. spaces equipped with a so-called restriction, denoted by $\downarrow$, satifying three properties: \begin{align*} & x \downarrow 0 = y \downarrow 0\\ & x \downarrow n \downarrow m = x \downarrow \mathrm{min} \ n \ m\\ & x \not = y \Longrightarrow \exists n. \ x \downarrow n \not = y \downarrow n \end{align*} They turn out to be cartesian closed and admit natural notions of constructiveness and completeness, enabling the definition of a fixed-point operator under verifiable side-conditions. This is achieved in our entry, from topological definitions to induction principles. Additionally, we configure the simplifier so that it can automatically solve both constructiveness and admissibility subgoals, as long as users write higher-order rules for their operators. Since our implementation relies on axiomatic type classes, the resulting library is a fully abstract, flexible and reusable framework.

License

BSD License

Topics

Session Restriction_Spaces