Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Iterating Non-Aggregative Structure Compositions

Marius Bozga, Radu Iosif, Florian Zuleger

TL;DR

This work introduces a non-aggregative, nondeterministic fusion operation on relational structures controlled by color-based compatibility, contrasting it with traditional aggregative HR-style composition. It proves that, for context-free sets of structures, the fusion-closure has bounded tree-width decidably, and if bounded, the closure is itself a context-free set described by an effectively constructible HR grammar. The approach hinges on RGB color schemes, color abstractions, and term-based simulations of fusion, enabling a Courcelle-style decision framework to check MSO properties over fusion-closed, tree-width-bounded families. This extends algorithmic verification techniques to a broader class of nondeterministic structural iterations, with potential applications to separation logic of relations and modeling of reconfigurable chemical/biological structures. The results connect structural width parameters to inductive grammars under non-aggregative fusion, offering tools for automated reasoning about systems with dynamic connectivity while preserving decidability guarantees.

Abstract

An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface. In this paper, we study a non-aggregative composition operation, called \emph{fusion}, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite \emph{hyperedge-replacement} (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called \emph{context-free}. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.

Iterating Non-Aggregative Structure Compositions

TL;DR

This work introduces a non-aggregative, nondeterministic fusion operation on relational structures controlled by color-based compatibility, contrasting it with traditional aggregative HR-style composition. It proves that, for context-free sets of structures, the fusion-closure has bounded tree-width decidably, and if bounded, the closure is itself a context-free set described by an effectively constructible HR grammar. The approach hinges on RGB color schemes, color abstractions, and term-based simulations of fusion, enabling a Courcelle-style decision framework to check MSO properties over fusion-closed, tree-width-bounded families. This extends algorithmic verification techniques to a broader class of nondeterministic structural iterations, with potential applications to separation logic of relations and modeling of reconfigurable chemical/biological structures. The results connect structural width parameters to inductive grammars under non-aggregative fusion, offering tools for automated reasoning about systems with dynamic connectivity while preserving decidability guarantees.

Abstract

An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface. In this paper, we study a non-aggregative composition operation, called \emph{fusion}, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite \emph{hyperedge-replacement} (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called \emph{context-free}. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.

Paper Structure

This paper contains 13 sections, 9 theorems, 14 equations, 6 figures, 1 table.

Table of Contents

  1. Introduction
  2. Definitions
  3. Relational Structures
  4. An Algebra of Structures
  5. Context-Free Sets of Structures
  6. The Closure of Context-Free Sets under Fusion
  7. Color Multisets
  8. Color Schemes
  9. Fusions as Operations on Terms
  10. Tree-width Bounded Fusion-closed Sets are Context-free
  11. Color Abstractions
  12. Conclusions and Future Work
  13. Proofs

Key Result

proposition 1

A set of structures whose Gaifman graphs contain infinitely many non-isomorphic square grids has unbounded tree-width.

Figures (6)

  • Figure 1: HR operations on structures over the alphabet $\{ {a,b,c} \}$, where $\#{a}=3$ and $\#{b}=\#{c}=2$. The order of vertices attached to an edge is indicated by an arrow pointing to the last vertex.
  • Figure 2: Building structures whose Gaifman graphs have infinitely large grid minors
  • Figure 3: Examples of RGB color schemes
  • Figure 4: Fusion of $\mathsf{G}$ structures by $3$-generated matchings
  • Figure 5: The $\mathsf{join}({t_1},{t_2},{\mathsf{c}^{i_{1}}_{\gamma_{1}}},{\mathsf{c}^{i_{2}}_{\gamma_2}})$ (a) and $\mathsf{append}({t_1},{t_2},{n},{k},{\mathsf{c}^i_\gamma})$ (b) operations
  • ...and 1 more figures

Theorems & Definitions (25)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • proposition 1
  • definition 6
  • theorem 1
  • definition 7
  • lemma 1
  • ...and 15 more