Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation

TL;DR

Metatheory.jl is a Julia framework that simplifies complex metaprogramming tasks by providing a high-performance, extensible equality saturation-based term rewriting system and dynamic AST pattern matching, enhancing symbolic computation capabilities.

Contribution

It introduces a novel, lightweight, and performant framework that integrates equality saturation and dynamic AST pattern matching for Julia, enabling advanced symbolic manipulation and metaprogramming.

Findings

Enables general-purpose symbolic mathematics and manipulation in Julia.

Provides a concise interface for expression analysis and optimization.

Enhances Julia's metaprogramming with a native, extensible rewriting system.

Abstract

We introduce Metatheory.jl: a lightweight and performant general purpose symbolics and metaprogramming framework meant to simplify the act of writing complex Julia metaprograms and to significantly enhance Julia with a native term rewriting system, based on state-of-the-art equality saturation techniques, and a dynamic first class Abstract Syntax Tree (AST) pattern matching system that is dynamically composable in an algebraic fashion, taking full advantage of the language's powerful reflection capabilities. Our contribution allows to perform general purpose symbolic mathematics, manipulation, optimization, synthesis or analysis of syntactically valid Julia expressions with a clean and concise programming interface, both during compilation or execution of programs.