seesaw: Delta-extended Triple Graph Grammars with Constructive Termination, Irredundant Consolidation, and Non-destructive History

Triple Graph Grammars (TGGs) have long suffered from pathologies under delta propagation: infinite folding towards trivial fixpoints, and delta expansion that amplifies minimal source edits into outsized target mutations. Existing remediations (delta lenses and SAT/SMT solvers) are essentially corrective patches that leave the representational root of the problem untouched. The pathologies are entrenched enough that prominent TGG lines have proposed restricted operational forms that trade expressiveness for adoptability. We present a delta-extended TGG framework in which observer deltas enter as typed Add, Delete, or Change events, while their realisations accumulate as a strictly monotone trace of Create, Delete, and Set operations in a ghost layer. Realised correspondences are symmetric carriers of these realisations rather than passive pointers: their incidence survives materialisation and determines how an explicit Delete propagates. Three novel mechanisms govern the cascade: parent-rooted Merkle-style ghost identity, rank-ordered match selection, and a position-scoped backtracking operator. At cascade termination, a bottom-up fold reduces the trace to an irredundant normal form, yielding a new stable baseline. We prove three main results. First, under a contractivity assumption on the rule set, standard in the TGG literature (layered grammars, NAC-gated rules, well-behaved rule sets), the cascade terminates within a bound given by the progress measure of the start state, and backtracking is bounded. Second, the folded trace is free of all nullification classes and of structural duplicates, and subset-minimal relative to that normal form: structurally identical ghosts receive the same parent-rooted hash identity and are collapsed, so no general isomorphism search (the step previously feared to be NP-hard) arises. Third, non-destructive history (undo, redo, branching over baselines) follows architecturally from the frozen-baseline design without any additional machinery. The Lean 4 development machine-checks 23 verification obligations associated with the formal core: seventeen require no project-specific assumptions, while six depend on three explicitly named interface idealisations. A fourth idealisation, hash collision-freedom, is isolated in a supporting identity lemma. The framework is realised as seesaw, a framework-free Rust engine. Its cascade exhibits flat per-element cost to 10^5 elements and scales into the 10^6 envelope. It passes all 37 of 37 sequential conformance tests of the current Benchmarx Families-to-Persons battery, in a field where published tools measured 0.82–1.00. It completes the initialisation and translation phases of an industrial translation pipeline (504 k rule applications, a 2.6M-node final graph) in 30 seconds single-threaded without rule layering, a configuration in which the published reference approach did not terminate (the pipeline’s refactoring phase, the full backtracking runner, and the nullification fixpoint are so far demonstrated on the 1.x line). It is a purely positive rule system: negative application conditions are eliminated in favour of positive structure rather than forgone, across every case in our suite. On identical workloads, the purely positive 2.x line measured approximately 1.4× faster than the fully optimised 1.x line, which retained NAC, marker, and value-carrying machinery. The implementation-language factor was measured separately for both lines using trace-identical Rust and Java implementations: in the 1.x line, warmed Java measured approximately 1.9× the Rust runtime on the translation workload (rising to approximately 7.7× where garbage collection dominates); in the 2.x line, the Java JAR measured approximately 3.5–4.5× the Rust crate on the industrial translation workload. This answers the tooling lock-in critique empirically. Beyond the released Rust crate and Java JAR, the currently unpublished Janus prototype exercises observer-based EMF/JDT integration without owning the host models; Janus is not part of the artifact evaluated here.