Mechanizing Operads with Event-B
Christian Attiogbé
TL;DR
This work tackles the challenge of using operads to model and reason about complex, component-based systems by presenting a complete refinement-based mechanisation in Event-B. It defines an abstract operad structure, introduces a robust composition mechanism, and proves consistency properties SP1–SP3 within a Rodin/ProB-enabled workflow. The authors implement a two-stage refinement that adds concrete data and ties abstract and concrete representations, and demonstrate the approach through simulation and model checking. The results provide a practical, extensible foundation for symbolic computation questions and for building libraries of operad-based reasoning in formal engineering contexts.
Abstract
Rigorous modelling of natural and industrial systems still conveys various challenges related to abstractions, methods to proceed with and easy-to-use tools to build, compose and reason on models. Operads are mathematical structures that provide such abstractions to compose various objects and garanteeing well-formedness. Concrete implementations of operads will offer practical means to exploit operads and to use them for various technical applications. Going from the mathematical structures, we develop with Event-B a complete refinement chain that implements algebraic operads and their basic operations. The result of this work, can be used from the methodological point of view to handle similar implementations for symbolic computation questions, and also to reason on symbolic computation applications supported by operads structures.