Specializing anti-unification for interaction models composition via gate connections
Joel Nguetoum, Boutheina Bannour, Pascale Le Gall, Erwan Mahe
TL;DR
The paper tackles the challenge of composing partial interaction views into a global interaction by using a specialized anti-unification framework that preserves designated gates. It introduces a constant-preserving variant of $E$-generalization, supported by a rule-based algorithm with termination, soundness, and completeness proofs, and extends the approach modulo equational theories. The method reframes gate alignment as a generalization problem over terms, enabling composition of local interactions without imposing restrictive structural constraints from prior models. A prototype tool demonstrates how sc-preserving generalization can reconstruct global interactions from partial views, highlighting practical applicability to open-system composition. This work provides a foundation for scalable, semantics-preserving composition of distributed interactions using algebraic reasoning.
Abstract
Interaction models describe distributed systems as algebraic terms, with gates marking interaction points between local views. Composing local models into a coherent global one requires aligning these gates while respecting the algebraic laws of interaction operators. We specialize anti-unification (or generalization) via a special constant-preserving variant, which preserves designated constants while generalizing the remaining structure. We develop a dedicated rule-based procedure for computing these generalizations, prove its termination, soundness, and completeness, extend it modulo equational theories, and integrate it into a standard anti-unification framework. A prototype tool demonstrates the approach's ability to recompose global interactions from partial views.