# `gargamelle-equational` — Equational Logic Institution & Presheaf Double-Pushout (DPO) Rewriting
[](https://haskell.org)
[](https://spdx.org/licenses/EUPL-1.2.html)
[](../../README.md#architectural-tier-map)
---
## 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.
<!-- See Note [Presheaf Double-Pushout Gluing Conditions] [ref:note-dpo-gluing-conditions] -->
---
## 3. Module Architecture & Repertoire Breadth
The package exports 2 modules delivering equational institutions and categorical DPO rewrites:
| Module | Primary Types & Typeclasses | Architectural Purpose |
| :--- | :--- | :--- |
| [`Gargamelle.Equational.DPO`](src/Gargamelle/Equational/DPO.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Gargamelle-Equational-DPO.html)) | [`Rule`](src/Gargamelle/Equational/DPO.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Gargamelle-Equational-DPO.html#t:Rule)), [`DPOStepResult`](src/Gargamelle/Equational/DPO.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Gargamelle-Equational-DPO.html#t:DPOStepResult)), [`applyDPO`](src/Gargamelle/Equational/DPO.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Gargamelle-Equational-DPO.html#v:applyDPO)), [`isDPOApplicable`](src/Gargamelle/Equational/DPO.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Gargamelle-Equational-DPO.html#v:isDPOApplicable)), [`makeRule`](src/Gargamelle/Equational/DPO.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Gargamelle-Equational-DPO.html#v:makeRule)) | Double-Pushout graph rewriting, pushout complement factorization, and gluing validation. |
| [`Equational`](src/Equational.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Equational.html)) | [`EGSym`](src/Equational.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Equational.html#t:EGSym)), [`Term`](src/Equational.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Equational.html#t:Term)), [`Equation`](src/Equational.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Equational.html#t:Equation)), [`EqModel`](src/Equational.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Equational.html#t:EqModel)), [`evalTerm`](src/Equational.hs) ([Hackage](https://hackage.haskell.org/package/gargamelle-equational/docs/Equational.html#v:evalTerm)) | First-order equational signatures, algebraic equations, and carrier interpretation models. |
---
## 4. Executable Worked Examples
### 4.1 Constructing and Executing a DPO Rewrite Rule
```haskell
{-# 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
```haskell
{-# 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](../../README.md).*