Frex: dependently-typed algebraic simplification

TL;DR

This paper introduces Frex, a dependently-typed algebraic simplification library based on universal algebra concepts, ensuring correctness and termination through its type system, with implementations in Idris 2 and Agda.

Contribution

It presents a novel algebraic simplification library design that guarantees termination, soundness, and completeness using dependent types, and demonstrates modular extensibility and proof capabilities.

Findings

Supports modular extension to new theories

Ensures termination, soundness, and completeness

Enables proof extraction and interactive development

Abstract

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.