On Categories of Nested Conditions
Arend Rensink, Andrea Corradini
TL;DR
The paper develops a categorical foundation for nested conditions used as application conditions in graph transformation, addressing the gap between structural morphisms and entailment in First-Order Logic. It introduces forward and backward root shifters and corresponding morphisms for arrow-based nested conditions, proving contravariant functors from the morphism categories to the entailment preorder. To remove structural redundancy, it defines span-based nested conditions with forward/backward span-shift morphisms, establishes their categories, and proves that they embed into entailment in a semantics-preserving way, with completeness capturing equivalence. Moreover, it proves that arrow-based and span-based frameworks are equivalent under the entailment preorder when viewed through the faithful transformation N, constructs indexed categories of shifters, and outlines connections to cartesian bicategories and further logics, thereby laying a robust foundation for reasoning about graph-based application conditions in full FOL.
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.