Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Moving a Derivation Along a Derivation Preserves the Spine in Adhesive Categories

Hans-Jörg Kreowski, Aaron Lye, Aljoscha Windhorst

TL;DR

The paper addresses how two basic operations on derivations in graph-transformational systems—moving a derivation along another derivation and restricting a derivation to a start-object monomorphism—interact within adhesive categories using the double-pushout framework. It formalizes forward and backward moving via parallel and sequential independence, introduces accessed parts, and defines the spine as the minimal restriction of a derivation. The main contribution is a rigorous proof that moving a derivation preserves its spine up to isomorphism, enabling stable composition of reductions and transformations, particularly in NP-problem reductions framed as graph derivations. This result provides a robust toolbox for reasoning about complex derivation compositions and suggests broader applicability to adhesive model categories beyond graphs, with potential impact on correctness proofs for reductions between combinatorial problems.

Abstract

In this paper, we investigate the relationship between two elementary operations on derivations in the framework of graph transformation based on adhesive categories: moving a derivation along a derivation based on parallel and sequential independence on one hand and restriction of a derivation with respect to a monomorphism into the start object on the other hand. Intuitively, a restriction clips off parts of the start object that are never matched by a rule application throughout the derivation on the other hand. As main result, it is shown that moving a derivation preserves its spine being the minimal restriction.

Moving a Derivation Along a Derivation Preserves the Spine in Adhesive Categories

TL;DR

The paper addresses how two basic operations on derivations in graph-transformational systems—moving a derivation along another derivation and restricting a derivation to a start-object monomorphism—interact within adhesive categories using the double-pushout framework. It formalizes forward and backward moving via parallel and sequential independence, introduces accessed parts, and defines the spine as the minimal restriction of a derivation. The main contribution is a rigorous proof that moving a derivation preserves its spine up to isomorphism, enabling stable composition of reductions and transformations, particularly in NP-problem reductions framed as graph derivations. This result provides a robust toolbox for reasoning about complex derivation compositions and suggests broader applicability to adhesive model categories beyond graphs, with potential impact on correctness proofs for reductions between combinatorial problems.

Abstract

In this paper, we investigate the relationship between two elementary operations on derivations in the framework of graph transformation based on adhesive categories: moving a derivation along a derivation based on parallel and sequential independence on one hand and restriction of a derivation with respect to a monomorphism into the start object on the other hand. Intuitively, a restriction clips off parts of the start object that are never matched by a rule application throughout the derivation on the other hand. As main result, it is shown that moving a derivation preserves its spine being the minimal restriction.
Paper Structure (16 sections, 8 theorems, 35 equations, 3 figures)

This paper contains 16 sections, 8 theorems, 35 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Graphs
  4. Categorical Notions and Facts
  5. The Double-Pushout Approach
  6. Local Church-Rosser Properties
  7. Moving derivations along derivations using independence
  8. Moving forward using parallel independence
  9. Moving backward using sequential independence
  10. Accessed Parts, Restrictions and Spines
  11. Accessed Parts
  12. Restrictions
  13. Composition of Restrictions
  14. Spines
  15. Moving Preserves the Spine
  16. ...and 1 more sections

Key Result

Proposition 3.3

Let $(P,\overline{P})$ be a parallel independent pair of sets of rules. Let $d = (G \mathop{\Longrightarrow}\limits^n_P H)$ and $\overline{d} = (G \mathop{\Longrightarrow}\limits^m_{\overline{P}} \overline{H})$ be two derivations. Then the iteration of conflux as long as possible yields two derivati

Figures (3)

  • Figure 1: conflux and interchange
  • Figure 2: Forward and backward moving
  • Figure 3: Diagrams used in the proof of Proposition \ref{['prop:moving']}

Theorems & Definitions (34)

  • Example 2.14
  • Definition 3.1
  • Example 3.2
  • Proposition 3.3
  • proof
  • Remark 3.4
  • Example 3.5
  • Proposition 3.6
  • proof
  • Remark 3.7
  • ...and 24 more