Metatheory.jl
Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation - Published in JOSS (2021)
Science Score: 77.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
✓DOI references
Found 2 DOI reference(s) in README -
✓Academic publication links
Links to: arxiv.org, acm.org, joss.theoj.org -
✓Committers with academic emails
2 of 31 committers (6.5%) from academic institutions -
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (12.4%) to scientific vocabulary
Keywords
Keywords from Contributors
Repository
Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.
Basic Info
- Host: GitHub
- Owner: JuliaSymbolics
- License: mit
- Language: Julia
- Default Branch: master
- Homepage: https://juliasymbolics.github.io/Metatheory.jl/dev/
- Size: 3.34 MB
Statistics
- Stars: 381
- Watchers: 13
- Forks: 46
- Open Issues: 55
- Releases: 24
Topics
Metadata Files
README.md
Metatheory.jl
The 3.0 version is in-development and close to release!
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 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.
2.0 is out!
Second stable version is out:
- New e-graph pattern matching system, relies on functional programming and closures, and is much more extensible than 1.0's virtual machine.
- No longer dispatch against types, but instead dispatch against objects.
- Faster E-Graph Analysis
- Better library macros
- Updated TermInterface to 0.3.3
- New interface for e-graph extraction using
EGraphs.egraph_reconstruct_expression - Simplify E-Graph Analysis Interface. Use Symbols or functions for identifying Analyses.
- Remove duplicates in E-Graph analyses data.
Many features have been ported from SymbolicUtils.jl. Metatheory.jl can be used in place of SymbolicUtils.jl when you have no need of manipulating mathematical expressions. The introduction of TermInterface.jl has allowed for large potential in generalization of term rewriting and symbolic analysis and manipulation features. Integration between Metatheory.jl with Symbolics.jl, as it has been shown in the "High-performance symbolic-numerics via multiple dispatch" paper.
Recommended Readings - Selected Publications
- 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
Contributing
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
Installation
You can install the stable version:
julia
julia> using Pkg; Pkg.add("Metatheory")
Or you can install the developer version (recommended by now for latest bugfixes)
julia
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.
Sponsors
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!
Owner
- Name: JuliaSymbolics
- Login: JuliaSymbolics
- Kind: organization
- Website: JuliaSymbolics.org
- Repositories: 8
- Profile: https://github.com/JuliaSymbolics
A fast and modern CAS for a fast and modern language
Citation (CITATION.bib)
@article{Cheli2021,
doi = {10.21105/joss.03078},
url = {https://doi.org/10.21105/joss.03078},
year = {2021},
publisher = {The Open Journal},
volume = {6},
number = {59},
pages = {3078},
author = {Alessandro Cheli},
title = {Metatheory.jl: Fast and Elegant Algebraic Computation in Julia with Extensible Equality Saturation},
journal = {Journal of Open Source Software}
}
@misc{cheli2021automated,
title={Automated Code Optimization with E-Graphs},
author={Alessandro Cheli},
year={2021},
eprint={2112.14714},
archivePrefix={arXiv},
primaryClass={cs.PL}
}
GitHub Events
Total
- Issues event: 15
- Watch event: 17
- Delete event: 2
- Issue comment event: 79
- Push event: 38
- Pull request event: 15
- Pull request review comment event: 41
- Pull request review event: 48
- Fork event: 2
- Create event: 10
Last Year
- Issues event: 15
- Watch event: 17
- Delete event: 2
- Issue comment event: 79
- Push event: 38
- Pull request event: 15
- Pull request review comment event: 41
- Pull request review event: 48
- Fork event: 2
- Create event: 10
Committers
Last synced: 5 months ago
Top Committers
| Name | Commits | |
|---|---|---|
| 0x0f0f0f | s****3@p****m | 302 |
| Alessandro | n****e | 172 |
| a | a@a****a | 53 |
| dependabot[bot] | 4****] | 10 |
| Wilkenfeld | r****4@g****m | 9 |
| ale | a****n@a****m | 7 |
| Jiayi Wei | M****e@g****m | 6 |
| Will Kimmerer | k****r@m****u | 5 |
| Dani Pinyol | d****i@a****m | 4 |
| Christopher Rackauckas | a****s@c****m | 4 |
| Chen Zhao | z****7@m****n | 4 |
| Shashi Gowda | g****a@m****u | 3 |
| jump | j****p@j****p | 2 |
| Philip Zucker | p****8@g****m | 2 |
| David P. Sanders | d****s@g****m | 1 |
| Greg Peairs | p****r@g****m | 1 |
| Hendrik Ranocha | r****a | 1 |
| Jesse Perla | j****a@g****m | 1 |
| CompatHelper Julia | c****y@j****g | 1 |
| fairbanks | f****j@C****e | 1 |
| Kyle Deeds | k****9@g****m | 1 |
| McCoy Becker | m****r@g****m | 1 |
| Mingze Feng | f****e@h****m | 1 |
| Mosè Giordano | m****e@g****g | 1 |
| NumHack | 7****k | 1 |
| Pietro Monticone | 3****e | 1 |
| Willow Ahrens | w****s@g****m | 1 |
| Yingbo Ma | m****5@g****m | 1 |
| chriselrod | e****c@g****m | 1 |
| herrgahr | 3****r | 1 |
| and 1 more... | ||
Committer Domains (Top 20 + Academic)
Issues and Pull Requests
Last synced: 4 months ago
All Time
- Total issues: 103
- Total pull requests: 132
- Average time to close issues: 8 months
- Average time to close pull requests: 25 days
- Total issue authors: 40
- Total pull request authors: 26
- Average comments per issue: 3.47
- Average comments per pull request: 2.15
- Merged pull requests: 80
- Bot issues: 0
- Bot pull requests: 29
Past Year
- Issues: 16
- Pull requests: 30
- Average time to close issues: 21 days
- Average time to close pull requests: 24 days
- Issue authors: 8
- Pull request authors: 5
- Average comments per issue: 0.69
- Average comments per pull request: 4.2
- Merged pull requests: 14
- Bot issues: 0
- Bot pull requests: 1
Top Authors
Issue Authors
- 0x0f0f0f (29)
- overshiki (7)
- gkronber (6)
- ViciousDoormat (6)
- willow-ahrens (4)
- vitrun (4)
- shashi (4)
- Audrius-St (3)
- MrVPlusOne (2)
- THinnerichs (2)
- jariji (2)
- Byurdyzo (2)
- HectorPeeters (2)
- jakevossen5 (2)
- schrauf (1)
Pull Request Authors
- 0x0f0f0f (48)
- gkronber (32)
- github-actions[bot] (28)
- nmheim (17)
- dependabot[bot] (17)
- olynch (12)
- Wilkenfeld (6)
- spaette (4)
- jumerckx (4)
- MrVPlusOne (3)
- gkronber-machine (2)
- shashi (2)
- ranocha (1)
- dpinol (1)
- kylebd99 (1)
Top Labels
Issue Labels
Pull Request Labels
Packages
- Total packages: 1
-
Total downloads:
- julia 123 total
- Total dependent packages: 3
- Total dependent repositories: 0
- Total versions: 24
juliahub.com: Metatheory
Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.
- Homepage: https://juliasymbolics.github.io/Metatheory.jl/dev/
- Documentation: https://docs.juliahub.com/General/Metatheory/stable/
- License: MIT
-
Latest release: 2.0.2
published about 2 years ago
Rankings
Dependencies
- julia-actions/setup-julia latest composite
- actions/checkout v2 composite
- julia-actions/julia-buildpkg latest composite
- julia-actions/setup-julia v1 composite
- JuliaRegistries/TagBot v1 composite
- actions/cache v1 composite
- actions/checkout v2 composite
- codecov/codecov-action v1 composite
- julia-actions/julia-buildpkg v1 composite
- julia-actions/julia-processcoverage v1 composite
- julia-actions/julia-runtest v1 composite
- julia-actions/setup-julia v1 composite
- actions/checkout v2 composite
- julia-actions/julia-buildpkg latest composite
- julia-actions/julia-docdeploy latest composite