Email Gateway (Jun 02 2025 at 15:54): Email Gateway (Jun 02 2025 at 15:54):From: Tobias Nipkow <nipkow@in.tum.de>
Restriction Spaces: a Fixed-Point Theory
Benoît Ballenghien, Benjamin Puyobro and Burkhart Wolff
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, satifying three properties ....
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.
https://www.isa-afp.org/entries/Restriction_Spaces.html
Examples of Restriction Spaces
Benoît Ballenghien, Benjamin Puyobro and Burkhart Wolff
In this session, a number of examples are provided to illustrate how the
Restriction_Spaces library works. The simple cases are, of course, covered:
trivial restriction, booleans, integers, option type, and so on. But we also
explore more elaborate constructions, such as formal power series and a trace
model of the CSP process algebra. Additionally, we provide a lightweight
integration with HOLCF, equipping restriction spaces with the inherited partial
order structure when needed.
https://www.isa-afp.org/entries/Restriction_Spaces-Examples.html
Ultrametric Structure for Restriction Spaces
Benoît Ballenghien, Benjamin Puyobro and Burkhart Wolff
In this entry, we explore the relationship between restriction spaces and usual
metric structures by instantiating the former as ultrametric spaces. This is
classically captured by defining the distance as
but we actually generalize this perspective by introducing a hierarchy of
increasingly refined type classes to systematically relate ultrametric and
restriction-based notions. This layered approach enables a precise comparison of
structural and topological properties. In the end, our main result establishes
that completeness in the sense of restriction spaces coincides with standard
metric completeness, thus bridging the gap between our framework and Banach's
fixed-point theorem established in HOL-Analysis.
https://www.isa-afp.org/entries/Restriction_Spaces-Ultrametric.html
CSP Semantics over Restriction Spaces
Benoît Ballenghien and Burkhart Wolff
We use the Restriction_Spaces library as a semantic foundation for the process
algebra framework HOL-CSP, offering a complementary backend to the existing
HOLCF infrastructure. The type of processes is instantiated as a restriction
space, and we prove that it is complete in this setting. This enables the
construction of fixed points for recursive process definitions without having to
rely exclusively on a pointed complete partial order. Notably, some operators
are constructive without being Scott-continuous, and vice versa, illustrating
the genuine complementarity between the two approaches. We also show that key
CSP operators are either constructive or non-destructive, and verify the
admissibility of several predicates, thereby supporting automated reasoning over
recursive specifications.
https://www.isa-afp.org/entries/HOL-CSP_RS.html
Enjoy them all!
Last updated: Jun 20 2025 at 16:26 UTC