-
EGGs are adhesive!
Authors:
Roberto Biondo,
Davide Castelnovo,
Fabio Gadducci
Abstract:
The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way.E-graphs (EGGs) are a formalism for program optimisation via an efficien…
▽ More
The use of rewriting-based visual formalisms is on the rise. In the formal methods community, this is due also to the introduction of adhesive categories, where most properties of classical approaches to graph transformation, such as those on parallelism and confluence, can be rephrased and proved in a general and uniform way.E-graphs (EGGs) are a formalism for program optimisation via an efficient implementation of equality saturation. In short, EGGs can be defined as (acyclic) term graphs with an additional notion of equivalence on nodes that is closed under the operators of the signature. Instead of replacing the components of a program, the optimisation step is performed by adding new components and linking them to the existing ones via an equivalence relation, until an optimal program is reached. This work describes EGGs via adhesive categories. Besides the benefits in itself of a formal presentation, which renders the properties of the data structure precise, the description of the addition of equivalent program components using standard graph transformation tools offers the advantages of the adhesive framework in modelling, for example, concurrent updates.
△ Less
Submitted 27 May, 2025; v1 submitted 17 March, 2025;
originally announced March 2025.
-
Left-Linear Rewriting in Adhesive Categories
Authors:
Paolo Baldan,
Davide Castelnovo,
Andrea Corradini,
Fabio Gadducci
Abstract:
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of man…
▽ More
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of many formalisms. We investigate the issue in the context of the double pushout approach to rewriting in the general setting of adhesive categories. While a consolidated theory exists for linear rules,which can consume, preserve and generate entities, this paper focuses on left-linear rules which may also "merge" parts of the state. This is an apparently minimal, yet technically hard enhancement,since a standard characterisation of independence that - in the linear case - allows one to derive a number of properties, essential in the development of a theory of concurrency, no longer holds. The paper performs an in-depth study of the notion of independence for left-linear rules: it introduces a novel characterisation of independence, identifies well-behaved classes of left-linear rewriting systems,and provides some fundamental results including a Church-Rosser property and the existence of canonical equivalence proofs for concurrent computations. These results properly extends the class of formalisms that can be modelled in the adhesive framework
△ Less
Submitted 8 July, 2024;
originally announced July 2024.
-
On The Axioms Of $\mathcal{M},\mathcal{N}$-Adhesive Categories
Authors:
Davide Castelnovo,
Marino Miculan
Abstract:
Adhesive and quasiadhesive categories provide a general framework for the study of algebraic graph rewriting systems. In a quasiadhesive category any two regular subobjects have a join which is again a regular subobject. Vice versa, if regular monos are adhesive, then the existence of a regular join for any pair of regular subobjects entails quasiadhesivity. It is also known (quasi)adhesive catego…
▽ More
Adhesive and quasiadhesive categories provide a general framework for the study of algebraic graph rewriting systems. In a quasiadhesive category any two regular subobjects have a join which is again a regular subobject. Vice versa, if regular monos are adhesive, then the existence of a regular join for any pair of regular subobjects entails quasiadhesivity. It is also known (quasi)adhesive categories can be embedded in a Grothendieck topos via a functor preserving pullbacks and pushouts along (regular) monomorphisms. In this paper we extend these results to $\mathcal{M}, \mathcal{N}$-adhesive categories, a concept recently introduced to generalize the notion of (quasi)adhesivity. We introduce the notion of $\mathcal{N}$-adhesive morphism, which allows us to express $\mathcal{M}, \mathcal{N}$-adhesivity as a condition on the subobjects' posets. Moreover, $\mathcal{N}$-adhesive morphisms allows us to show how an $\mathcal{M},\mathcal{N}$-adhesive category can be embedded into a Grothendieck topos, preserving pullbacks and $\mathcal{M}, \mathcal{N}$-pushouts.
△ Less
Submitted 5 March, 2025; v1 submitted 23 January, 2024;
originally announced January 2024.
-
A new criterion for $\mathcal{M}, \mathcal{N}$-adhesivity, with an application to hierarchical graphs
Authors:
Davide Castelnovo,
Fabio Gadducci,
Marino Miculan
Abstract:
Adhesive categories provide an abstract framework for the algebraic approach to rewriting theory, where many general results can be recast and uniformly proved. However, checking that a model satisfies the adhesivity properties is sometimes far from immediate. In this paper we present a new criterion giving a sufficient condition for $\mathcal{M}, \mathcal{N}$-adhesivity, a generalisation of the o…
▽ More
Adhesive categories provide an abstract framework for the algebraic approach to rewriting theory, where many general results can be recast and uniformly proved. However, checking that a model satisfies the adhesivity properties is sometimes far from immediate. In this paper we present a new criterion giving a sufficient condition for $\mathcal{M}, \mathcal{N}$-adhesivity, a generalisation of the original notion of adhesivity. We apply it to several existing categories, and in particular to hierarchical graphs, a formalism that is notoriously difficult to fit in the mould of algebraic approaches to rewriting and for which various alternative definitions float around.
△ Less
Submitted 15 June, 2022; v1 submitted 1 January, 2022;
originally announced January 2022.
-
Fuzzy Algebraic Theories
Authors:
Davide Castelnovo,
Marino Miculan
Abstract:
In this work we propose a formal system for fuzzy algebraic reasoning. The sequent calculus we define is based on two kinds of propositions, capturing equality and existence of terms as members of a fuzzy set. We provide a sound semantics for this calculus and show that there is a notion of free model for any theory in this system, allowing us (with some restrictions) to recover models as Eilenber…
▽ More
In this work we propose a formal system for fuzzy algebraic reasoning. The sequent calculus we define is based on two kinds of propositions, capturing equality and existence of terms as members of a fuzzy set. We provide a sound semantics for this calculus and show that there is a notion of free model for any theory in this system, allowing us (with some restrictions) to recover models as Eilenberg-Moore algebras for some monad. We will also prove a completeness result: a formula is derivable from a given theory if and only if it is satisfied by all models of the theory. Finally, leveraging results by Milius and Urbat, we give HSP-like characterizations of subcategories of algebras which are categories of models of particular kinds of theories.
△ Less
Submitted 21 October, 2021;
originally announced October 2021.
-
Closure hyperdoctrines, with paths
Authors:
Davide Castelnovo,
Marino Miculan
Abstract:
(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems.
In this paper we introduce an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)…
▽ More
(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems.
In this paper we introduce an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). Then, we show how spatial logical constructs concerning surroundedness and reachability can be interpreted by endowing hyperdoctrines with a general notion of paths. By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators.
Therefore, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, but especially for the definition of new spatial logics for new applications.
△ Less
Submitted 31 December, 2020; v1 submitted 8 July, 2020;
originally announced July 2020.
