Parallelism Theorem and Derived Rules for Parallel Coherent Transformations

TL;DR

This paper proves an Independent Parallelism Theorem within adhesive HLR categories, establishing a bijective link between sequential and parallel derivations using Parallel Coherent Transformations, and shows how to extract derived rules from PCTs.

Contribution

It introduces a new parallelism theorem for adhesive HLR categories and demonstrates how to derive rules from parallel coherent transformations without coproduct assumptions.

Findings

Establishes a bijective correspondence between sequential and parallel derivations.

Shows how to extract derived rules from parallel coherent transformations.

Provides a new framework for parallel transformations in adhesive HLR categories.

Abstract

An Independent Parallelism Theorem is proven in the theory of adhesive HLR categories. It shows the bijective correspondence between sequential independent and parallel independent direct derivations in the Weak Double-Pushout framework, see [2]. The parallel derivations are expressed by means of Parallel Coherent Transformations (PCTs), hence without assuming the existence of coproducts compatible with M as in the standard Parallelism Theorem. It is aslo shown that a derived rule can be extracted from any PCT, in the sense that to any direct derivation of this rule corresponds a valid PCT.