Frex: dependently-typed algebraic simplification

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-06
Main Authors: Allais, Guillaume, Brady, Edwin, Corbyn, Nathan, Kammar, Ohad, Yallop, Jeremy
Format: Article
Language:English
Subjects:
Algebra
Libraries
Mathematical analysis
Modularity
Modules
Monoids
Programming languages
Simplification
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422