If you want to use Metatheory.jl, please use the ale/3.0 branch.
It's a lot more stable, and up to ~200x faster than 2.0
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 TermInterface.jl.
Metatheory.jl provides:
- An eDSL (embedded 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) engine, based on the egg library, supporting a backtracking pattern matcher 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.
@capturemacro for flexible metaprogramming.
Intuitively, Metatheory.jl transforms Julia expressions in other Julia expressions at both compile and run time.
This allows 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.
- Rewrite integration test files in Literate.jl format, becoming narrative tutorials available in the docs.
- Proof production algorithm: explanations.
- Using new TermInterface.
- Performance optimization: use vectors of UInt to internally represent terms in e-graphs.
- Comprehensive suite of benchmarks that are run automatically on PR.
- Complete overhaul of the rebuilding algorithm.
There's lot of room for improvement for Metatheory.jl, by making it more performant and by extending its features. Any contribution is welcome!
Performance:
- Improving the speed of the e-graph pattern matcher. (Useful paper)
- Reducing allocations used by Equality Saturation.
- #50 - Goal-informed rule schedulers: develop heuristic algorithms that choose what rules to apply at each equality saturation iteration to prune space of possible rewrites.
Features:
- #111 Introduce proof production capabilities for e-graphs. This can be based on the egg implementation.
- Common Subexpression Elimination when extracting from an e-graph #158
- Integer Linear Programming extraction of expressions.
- Pattern matcher enhancements: #43 Better parsing of blocks, #3 Support
...variables in e-graphs, #89 syntax for vectors - #75 E-Graph intersection algorithm
Documentation:
- Port more integration tests to tutorials that are rendered with Literate.jl
- Document Functional Rewrite Combinators and add a tutorial.
Most importantly, there are many practical real world applications where Metatheory.jl could be used. Let's work together to turn this list into some new Julia packages:
Many features of this package, such as the classical rewriting system, have been ported from SymbolicUtils.jl, and are technically the same. Integration between Metatheory.jl with Symbolics.jl is currently in-development, as we recently released a new version of TermInterface.jl.
An integration between Metatheory.jl and Symbolics.jl is possible and has previously been shown in the "High-performance symbolic-numerics via multiple dispatch" paper. Once we reach consensus for a shared symbolic term interface, Metatheory.jl can be used to:
- Rewrite Symbolics.jl expressions with bi-directional equations instead of simple directed rewrite rules.
- Search for the space of mathematically equivalent Symbolics.jl expressions for more computationally efficient forms to speed various packages like ModelingToolkit.jl that numerically evaluate Symbolics.jl expressions.
- When proof production is introduced in Metatheory.jl, automatically search the space of a domain-specific equational theory to prove that Symbolics.jl expressions are equal in that theory.
- Other scientific domains extending Symbolics.jl for system modeling.
QuantumCumulants.jl automates the symbolic derivation of mean-field equations in quantum mechanics, expanding them in cumulants and generating numerical solutions using state-of-the-art solvers like ModelingToolkit.jl and DifferentialEquations.jl. A potential application for Metatheory.jl is domain-specific code optimization for QuantumCumulants.jl, aiming to be the first symbolic simplification engine for Fock algebras.
Herbie is a tool using equality saturation to automatically rewrites mathematical expressions to enhance
floating-point accuracy. Recently, Herbie's core has been rewritten using
egg, with the tool originally implemented in
a mix of Racket, Scheme, and Rust. While effective, its usage involves multiple
languages, making it impractical for non-experts. The text suggests the theoretical
possibility of porting this technique to a pure Julia solution, seamlessly
integrating with the language, in a single macro @fp_optimize that fixes
floating-point errors in expressions just before code compilation and execution.
Metatheory.jl can be used to make a pure Julia Automated Theorem Prover (ATP) inspired by the use of E-graphs in existing ATP environments like Z3, Simplify and CVC4, in the context of Satisfiability Modulo Theories (SMT).
The two-language problem in program verification can be addressed by allowing users to define high-level theories about their code, that are statically verified before executing the program. This holds potential for various applications in software verification, offering a flexible and generic environment for proving formulae in different logics, and statically verifying such constraints on Julia code before it gets compiled (see Mixtape.jl).
To develop such a package, Metatheory.jl needs:
- Introduction of Proof Production in equality saturation.
- SMT in conjunction with a SAT solver like PicoSAT.jl
- Experiments with various logic theories and software verification applications.
Many projects that could potentially be ported to Julia are listed on the egg website. A simple search for "equality saturation" on Google Scholar shows many new articles that leverage the techniques used in this packages.
PLDI is a premier academic forum in the field of programming languages and programming systems research, which organizes an e-graph symposium where many interesting research and projects have been presented.
There's also lots of room for theoretical improvements to the e-graph data structure and equality saturation rewriting.
In classical rewriting SymbolicUtils.jl offers a mechanism for matching expressions with associative and commutative operations: @acrule - a special kind of rule that considers all permutations and combinations of arguments. In e-graph rewriting in Metatheory.jl, associativity and commutativity have to be explicitly defined as rules. However, the presence of such rules, together with distributivity, will likely cause equality saturation to loop infinitely. See "Why reasonable rules can create infinite loops" for an explanation.
Some workaround exists for ensuring termination of equality saturation: bounding the depth of search, or merge-only rewriting without introducing new terms (see "Ensuring the Termination of EqSat over a Terminating Term Rewriting System").
There's a few theoretical questions left:
- What kind of rewrite systems terminate in equality saturation?
- Can associative-commutative matching be applied efficiently to e-graphs while avoiding combinatory explosion?
- Can e-graphs be extended to include nodes with special algebraic properties, in order to mitigate the downsides of non-terminating systems?
- The Metatheory.jl manual
- OUT OF DATE: The Metatheory.jl introductory paper gives a brief high level overview on the library and its functionalities.
- The Julia Manual metaprogramming section is fundamental to understand what homoiconic expression manipulation is and how it happens in Julia.
- An introductory blog post on SIGPLAN about
eggand e-graphs rewriting. - egg: Fast and Extensible Equality Saturation contains the definition of E-Graphs on which Metatheory.jl's equality saturation rewriting backend is based. This is a strongly recommended reading.
- High-performance symbolic-numerics via multiple dispatch: a paper about how we used Metatheory.jl to optimize code generation in Symbolics.jl
- Automated Code Optimization with E-Graphs. Alessandro Cheli's Thesis on Metatheory.jl
If you'd like to give us a hand and contribute to this repository you can:
- Find a high level description of the project architecture in ARCHITECTURE.md
- Read the contribution guidelines in CONTRIBUTING.md
You can install the stable version:
julia> using Pkg; Pkg.add("Metatheory")Or you can install the development version (recommended by now for latest bugfixes)
julia> using Pkg; Pkg.add(url="https://github.com/JuliaSymbolics/Metatheory.jl")Extensive Metatheory.jl is available here
If you use Metatheory.jl in your research, please cite our works.
If you enjoyed Metatheory.jl and would like to help, you can donate a coffee or choose place your logo and name in this page. See 0x0f0f0f's Github Sponsors page!
