Mechanizing Operads with Event-B

TL;DR

This paper develops a formal implementation of operads using Event-B, enabling rigorous modeling and reasoning on systems with compositional structures, bridging abstract algebraic concepts with practical tool support.

Contribution

It introduces a complete refinement chain in Event-B for implementing algebraic operads, facilitating their practical use in symbolic computation and system modeling.

Findings

Successfully implemented operads in Event-B

Provides a framework for reasoning on symbolic computation

Enables rigorous modeling of compositional systems

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.