gargamelle-equational — Equational Logic Institution & Presheaf Double-Pushout (DPO) Rewriting

1. Executive Summary & Problem Framing

Rule-based graph rewriting and equational algebraic laws are fundamental to abstract syntax manipulation, code refactoring, and automated architectural optimization. However, applying syntactic rewrites to interconnected system representations introduces significant correctness hazards:

1. Dangling Edges & Broken References: Blindly deleting an AST node or architectural component without checking incident relations produces invalid graph states and runtime null-pointer crashes.
2. Identification Conflicts: When a pattern match collapses two distinct elements of a rewrite rule into a single host element, naive replacements corrupt untouched context.
3. Non-Algebraic Ad-Hoc Transformations: Without formal pushout semantics, rewrite systems lack sound confluence, termination, and compositionality guarantees.

gargamelle-equational grounds transformation systems in algebraic category theory:

• Equational Institution: Models universal algebraic signatures, term equivalence, and concrete interpretation structures within the Goguen-Burstall institution framework.
• Categorical DPO Rewriting: Implements Double-Pushout graph and presheaf transformations via proarrow's adhesive pushout complement engine.
• Sound Gluing Verification: Rigorously verifies identification and dangling conditions prior to state modification, returning DPOGluingFailed rather than corrupting host structures.

2. Mathematical Foundations & Theoretical Invariants

2.1 Presheaf Double-Pushout (DPO) Rewriting

In algebraic graph rewriting (Ehrig, Pfender, Schneider, 1973), a rewrite rule \(p = (L \stackrel{l}{\leftarrow} K \stackrel{r}{\to} R)\) is an interface span:

• \(L\) is the left-hand pattern matched in host graph \(G\) via morphism \(m : L \to G\).
• \(K\) is the invariant interface representing preserved structure.
• \(R\) is the right-hand replacement pattern containing generated structure.

A DPO rewrite step consists of two categorical pushout squares:

        L ◄───────────── K ─────────────► R
        │      (PO 1)    │      (PO 2)    │
      m │   Pushout      │                │ r*
        │   Complement   │                │
        ▼                ▼                ▼
        G ◄───────────── D ─────────────► H = D ⨿_K R
              context

1. Step 1: Pushout Complement (Context Isolation): Deletes pattern items \((L \setminus l(K))\) from host graph \(G\), yielding context object \(D\).
2. Step 2: Pushout (Gluing): Glues replacement \(R\) to context \(D\) along interface \(K\) to produce the rewritten host object \(H\).

2.2 The Gluing Condition Invariant

In adhesive and presheaf categories, the pushout complement \(D\) exists if and only if match \(m\) satisfies the Gluing Condition:

• Identification Condition: If \(m(x) = m(y)\) for distinct \(x, y \in L\), then both \(x\) and \(y\) must belong to \(l(K)\). (A rule cannot simultaneously delete and preserve the same host item).
• Dangling Edge Condition: No edge in host graph \(G \setminus m(L)\) has an endpoint in a node deleted by \(m(L \setminus l(K))\).

When either condition is violated, applyDPO soundly returns DPOGluingFailed with zero side effects.

3. Module Architecture & Repertoire Breadth

The package exports 2 modules delivering equational institutions and categorical DPO rewrites:

4. Executable Worked Examples

4.1 Constructing and Executing a DPO Rewrite Rule

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

module ExampleDPO where

import Gargamelle.Equational.DPO
import Proarrow.Category.Instance.FinHask (FINHASK(..), Fin, FinHask, fromList)

-- Rewrite span: Fin 2 <- Fin 1 -> Fin 2
-- Preserves item 0, deletes item 1 in L, creates item 1 in R
exampleRewrite :: IO ()
exampleRewrite = do
  let leftLeg :: FinHask (FH (Fin 1)) (FH (Fin 2))
      leftLeg = fromList [(0, 0)]
      rightLeg :: FinHask (FH (Fin 1)) (FH (Fin 2))
      rightLeg = fromList [(0, 1)]
      rule = makeRule leftLeg rightLeg

      -- Injective match on host Fin 2
      match :: FinHask (FH (Fin 2)) (FH (Fin 2))
      match = fromList [(0, 0), (1, 1)]

  case applyDPO rule match of
    DPOSuccess _d2g _d2h _r2h ->
      putStrLn "DPO rewrite succeeded: host transformed cleanly."
    DPOGluingFailed ->
      putStrLn "Rewrite aborted: gluing condition violated."

4.2 Equational Term Evaluation

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}

module ExampleEquational where

import Data.Proxy (Proxy(..))
import qualified Data.Map.Strict as Map
import Equational

-- Define equation: f(c) = c
checkIdentityLaw :: Bool
checkIdentityLaw =
  let c = Const (Proxy @"c")
      fc = FunApp (Proxy @"f") [c]
      _eqn = Equation fc c
      model = EqModel
        { carrier = ["c"]
        , interp  = Map.fromList [("f", \case (x:_) -> x; [] -> "c")]
        }
  in evalTerm model fc == evalTerm model c

5. Integration Points & Subsystem Boundaries

gargamelle-equational acts at Tier 3 (Logic Engine) of the Gargamelle architecture:

┌────────────────────────────────────────────────────────┐
│               Downstream Consumers                     │
│  - gargamelle-workflow: Structural AST Transformations │
│  - gargamelle-sheaf: Cohomological Complex Rewriting   │
└──────────────────────────▲─────────────────────────────┘
                           │
                [gargamelle-equational]
                           │
┌──────────────────────────▼─────────────────────────────┐
│               Upstream Substrates                      │
│  - gargamelle-core: Goguen-Burstall Institutions       │
│  - proarrow (>= 0.2): Adhesive categories, DPO Engine  │
└────────────────────────────────────────────────────────┘

6. Diagnostic & Troubleshooting Guide

6.1 DPOGluingFailed on Application

• Symptom: applyDPO returns DPOGluingFailed instead of DPOSuccess.
• Root Cause: Either the match is non-injective on elements outside the interface span \(K\) (identification conflict), or a deleted node has incident edges in \(G\) not accounted for by rule \(L\) (dangling edge condition).
• Remedy: Ensure the interface \(K\) explicitly includes all nodes that remain incident to context edges, or inspect isDPOApplicable before triggering rewrite chains.

6.2 Undefined Function in evalTerm

• Symptom: Runtime error undefined function: <symbol> during equational evaluation.
• Root Cause: The EqModel interpretation map is missing a mapping for function symbol <symbol>.
• Remedy: Populate interp model with entries for all function symbols declared in syms.

Part of the Gargamelle Verification Suite.