一句话：提出依赖类型代数化简库 Frex，用泛代数结构保证化简模块终止、可靠且完备。
该论文提出代数化简库 Frex 的新设计，围绕泛代数中的理论、模型、同态以及自由代数及其扩张的泛性质组织化简。其依赖类型接口可保证内置与用户定义的化简模块相对于明确定义的等式类终止、可靠且完备。作者在 Idris 2 和 Agda 中实现该设计，并展示其支持向新理论模块化扩展、证明抽取与认证、通过反射进行目标抽取以及交互式开发。
We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library’s dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.
@article{paperbot3054,
title = {Frex: Dependently Typed Algebraic Simplification},
author = {Guillaume Allais and Edwin Brady and Nathan Corbyn and Ohad Kammar and Jeremy Yallop},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747506}
}