Metatheory.jl 1.0

Docs Docs CI codecov arXiv status Zulip

Metatheory.jl is a general purpose term rewriting, metaprogramming and algebraic computation library for the Julia programming language, designed to take advantage of the powerful reflection capabilities to bridge the gap between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic pattern matching features. The core features of Metatheory.jl are a powerful rewrite rule definition language, a vast library of functional combinators for classical term rewriting and an e-graph rewriting, a fresh approach to term rewriting achieved through an equality saturation algorithm. Metatheory.jl can manipulate any kind of Julia symbolic expression type, as long as it satisfies the TermInterface.jl.

Metatheory.jl provides:

  • An eDSL (domain specific language) to define different kinds of symbolic rewrite rules.
  • A classical rewriting backend, derived from the SymbolicUtils.jl pattern matcher, supporting associative-commutative rules. It is based on the pattern matcher in the SICM book.
  • A flexible library of rewriter combinators.
  • An e-graph rewriting (equality saturation) backend and pattern matcher, based on the egg library, supporting backtracking and non-deterministic term rewriting by using a data structure called e-graph, efficiently incorporating the notion of equivalence in order to reduce the amount of user effort required to achieve optimization tasks and equational reasoning.
  • @capture macro for flexible metaprogramming.

Intuitively, Metatheory.jl transforms Julia expressions in other Julia expressions and can achieve such at both compile and run time. This allows Metatheory.jl users to perform customized and composable compiler optimizations specifically tailored to single, arbitrary Julia packages. Our library provides a simple, algebraically composable interface to help scientists in implementing and reasoning about semantics and all kinds of formal systems, by defining concise rewriting rules in pure, syntactically valid Julia on a high level of abstraction. Our implementation of equality saturation on e-graphs is based on the excellent, state-of-the-art technique implemented in the egg library, reimplemented in pure Julia.

1.0 is out!

The first stable version of Metatheory.jl is out! The goal of this release is to unify the symbolic manipulation ecosystem of Julia packages. Many features have been ported from SymbolicUtils.jl. Now, Metatheory.jl can be used in place of SymbolicUtils.jl when you have no need of manipulating mathematical expressions. SymbolicUtils.jl can now completely leverage on the generic stack of rewriting features provided by Metatheory.jl, highly decoupled from the symbolic term representation thanks to TermInterface.jl. Read more in NEWS.md.

Contributing

If you'd like to give us a hand and contribute to this repository you can:

If you enjoyed Metatheory.jl and would like to help, please also consider a tiny donation 💕!

Installation

You can install the stable version:

julia> using Pkg; Pkg.add("Metatheory")

Or you can install the developer version (recommended by now for latest bugfixes)

julia> using Pkg; Pkg.add(url="https://github.com/JuliaSymbolics/Metatheory.jl")

Documentation

Extensive Metatheory.jl is available here

Citing

If you use Metatheory.jl in your research, please cite our works.