On Categories of Nested Conditions

TL;DR

This paper introduces a new structural framework for nested conditions in graph transformations, addressing weaknesses in existing definitions and organizing models into richer categorical structures.

Contribution

It proposes a novel notion of structural morphism among nested conditions and a span-based extension, enhancing the theoretical understanding of their structure.

Findings

Defined a notion of structural morphism consistent with formula entailment

Identified weaknesses in existing nested conditions definitions

Organized models into categories connected by functors

Abstract

Nested conditions are used, among other things, as a graphical way to express first order formulas ruling the applicability of a graph transformation rule to a given match. In this paper, we propose (for the first time) a notion of structural morphism among nested conditions, consistent with the entailment of the corresponding formulas. This reveals a structural weakness of the existing definition of nested conditions, which we overcome by proposing a new notion of span-based nested conditions, embedding the original ones. We also introduce morphisms for the latter, showing that those form a richer structure by organising the various models in a number of categories suitably related by functors.