We present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra -- fral -- and a free extension -- frex -- of an algebra by a set of variables. The library's dependently-typed API guarantees simplification modules, even user-defined ones, are terminating, sound, and complete with respect to a well-specified class of equations. Completeness offers intangible benefits in practice -- our main contribution is the novel design. Cleanly separating between the interface and implementation of simplification modules provides two new modularity axes. First, simplification modules share thousands of lines of infrastructure code dealing with term-representation, pretty-printing, certification, and macros/reflection. Second, new simplification modules can reuse existing ones. We demonstrate this design by developing simplification modules for monoid varieties: ordinary, commutative, and involutive. We implemented this design in the new Idris2 dependently-typed programming language, and in Agda.

翻译：我们提出了一种可扩展的、具有数学结构的代数化简库设计。该库基于泛代数概念构建：自由代数（fral）以及通过变量集对代数的自由扩展（frex）。库的依赖类型API保证了化简模块（包括用户自定义模块）对一类明确定义的方程具有终止性、可靠性和完备性。完备性在实践中带来了无形优势——我们的主要贡献在于这一新颖设计。通过清晰分离化简模块的接口与实现，我们获得了两个新的模块化维度。其一，化简模块共享数千行涉及项表示、美观打印、验证及宏/反射的基础设施代码。其二，新的化简模块可复用现有模块。我们通过开发幺半群簇（普通型、交换型、对合型）的化简模块展示了这一设计，并在新的依赖类型编程语言Idris2及Agda中实现了该方案。