Other than e-graphs rewriting, Metatheory.jl still offers some features that overlap with SymbolicUtils.jl features. Those features are rule creation and manipulation and classical rewriting/pattern matching. In SU classical rewriting is battle tested, in MT its used very few times and sucks.
The purpose of classical rewriting is basically the same in both MT and SU. By now, in Metatheory v0.5 I've removed the dependency to the MatchCore.jl pattern matching system because it was a metaprogramming mess and did not bring any particular benefit over other approaches, and built from scratch a crappy pattern matcher that just works but is truly naive.
Most importantly, making those components shared will allow for seamless integration and interoperability between the two rewriting systems. A primary goal of this RFC is to make MT and SU accept the same systems of rules in both egraphs and classical rewriting, and to make MT use the already existing, excellent SU backend for classical rewriting without re-implementing the entire rule pattern matcher stack. The best goal would be having the same (abstract?) types for rules in both systems, and even better having a RewriteRules.jl package defining an interface to allow users to define their own rules semantics and pattern matchers, without being specifically tied to MT data structures or SU symbolic types , just to TermInterface.jl, to maintain generality without losing the specific optimizations of SU or the MT virtual machine egraph pattern matcher.
(Yes, I'd like to remove classical rewriting from MT and leave it to this shared component).
The steps may be the following:
Separate the rule definition eDSL and make it shared with the same consistent, specified syntax. Separate the rule type hierarchy and make it shared. Separate the pattern matching system and make it shared, separate the pattern definition and type hierarchy and make it shared.
Rules and Pattern Matching
SU rules build from exprs, construct symbolics terms and then build a staged pattern matching RGF function. MT used to do this at first. Now it has got some useful types: Patterns. MT rules are part of a hierarchy <:AbstractRule with BidirectionalRule and SymbolicRule as the main types. SU does not yet have any BidirectionalRule system, while SU.Rule is nothing else than MT's DynamicRule. MT does not have yet knowledge of ACRule but that would be really cool to have.
Ideas:
Split Metatheory.Patterns to Patterns.jl, make it support TermInterface.jl only
Split Metatheory.Rules, split SymbolicUtils rules system and merge them into RewriteRules.jl, relying only on TermInterface.jl and Patterns.jl
Rewriters.jl can now work out of the box with TermInterface.jl supporting types, and RewriteRules.jl systems without users having to install SU or MT if they want to rewrite on Expr or other simple types.
SymbolicUtils.jl still will provide all its cool features and optimization for tracing, symtypes, constructor level optimization and will work on top of RewriteRules.jl, Patterns.jl and TermInterface.jl
MT will provide egraphs rewriting on top of those 3 packages.
Profit. MT and SU integration can be finalized and the packages can share the best out of each other at any time, and also one can do funky metaprogramming stuff from the future like rewrite systems creating other rewrite systems since Patterns.jl should support TermInterface.jl
Benefits SU -> MT
The pattern matcher in SU is cool, fast, staged, stable and inspired by a Sussman's work. The current pattern matcher in MT for classical rewriting sucks and is a slow naive pattern matcher that is still missing some features such as slot variables.
MT would really benefit from a predicate system like SU's.
MT could benefit from the already existing rule systems in SU
MT could be able to handle ACRule if the core of rewriting was shared between packages.
Benefits MT -> SU
SU could use egraphs rewriting and analysis out of the box with its already defined SU rule systems.
SU or any package could build rules system programmatically by using the Pattern type hierarchy from MT, which should be decoupled from the rewrite systems and the syntax used.
SU's predicate system could be improved with simple type tagging from MT. (may dispatch on both ~x::SomeType and ~x::(y->somepredicate(y))
Inconsistencies
The rule syntax, although semantics are similar, is different between SU and MT. MT has fewer dependants and could be changed easily.
Design choices. The MT pattern system, especially PatTerm used to build the egraphs VM pattern matcher programs and for classical patt. matching via dispatch, is based on the design of Expr. This means that common head symbols are used like this: PatTerm(:call, :f, 1, :a). This falls again to the problem of rewriting on Expr in SU with TermInterface.jl. If such a shared classical rewriting backend exists, it should be able to rewrite on any type satisfying at least the core of TermInterface. SU patterns and expressions, on the other hand, are built off SU symbolic types which implicitly handle :call-like patterns. To circumnavigate this issue i've added a temporary solution to MT, iscall(x::<:Symbolic) = true such that symbolic Terms where operation is not :call can still match against PatExpr(:call, .... This is a temporary hack that has to be formalized, tested and documented, but it works for the Symbolics optimization PR. I believe that both egraph rewrite systems and classical rewrite systems should be able to handle both kind of types with the same pattern matching syntax and systems, and can be used interchangeably.
*We don't know how SU behaves when fed with symbolic expression types that do not support symtype or metadata. This is because it was not built to rewrite on types such as Expr, and users should not attempt to do this by now until we find a solution.
Out of the box, SU pattern matchers and rules cannot handle symbolic types where operation is :call or :ref or other non-function-typed operators, could this be changed to be as general as possible? In SU, rules are only dynamic. It means that the operators that appear on the right hand side have to be defined for the symbolic types. It means that in order to rewrite Julia code itself with SU, the user has to override all the methods that the RHSs of rules reference, to dispatch against Symbol and Expr. This may be annoying if an user is trying to use classical rewriting to change a very large julia program with a very large rewrite system. Sometimes, symbolic only behaviour where the RHS pattern variables are just dictionary-substituted is desirable. It may not be a problem by now for the current scope of SU, but if we'd like to make the rewriting and rule definition systems shared and decoupled both kinds of behavior should be supported.
0x0f0f0f
commented
3 years ago
Other than e-graphs rewriting, Metatheory.jl still offers some features that overlap with SymbolicUtils.jl features. Those features are rule creation and manipulation and classical rewriting/pattern matching. In SU classical rewriting is battle tested, in MT its used very few times and sucks. The purpose of classical rewriting is basically the same in both MT and SU. By now, in Metatheory v0.5 I've removed the dependency to the MatchCore.jl pattern matching system because it was a metaprogramming mess and did not bring any particular benefit over other approaches, and built from scratch a crappy pattern matcher that just works but is truly naive.
Most importantly, making those components shared will allow for seamless integration and interoperability between the two rewriting systems. A primary goal of this RFC is to make MT and SU accept the same systems of rules in both egraphs and classical rewriting, and to make MT use the already existing, excellent SU backend for classical rewriting without re-implementing the entire rule pattern matcher stack. The best goal would be having the same (abstract?) types for rules in both systems, and even better having a
RewriteRules.jlpackage defining an interface to allow users to define their own rules semantics and pattern matchers, without being specifically tied to MT data structures or SU symbolic types , just to TermInterface.jl, to maintain generality without losing the specific optimizations of SU or the MT virtual machine egraph pattern matcher.(Yes, I'd like to remove classical rewriting from MT and leave it to this shared component).
The steps may be the following: Separate the rule definition eDSL and make it shared with the same consistent, specified syntax. Separate the rule type hierarchy and make it shared. Separate the pattern matching system and make it shared, separate the pattern definition and type hierarchy and make it shared.
Rules and Pattern Matching
SU rules build from exprs, construct symbolics terms and then build a staged pattern matching RGF function. MT used to do this at first. Now it has got some useful types:
Patterns. MT rules are part of a hierarchy<:AbstractRulewith BidirectionalRule and SymbolicRule as the main types. SU does not yet have any BidirectionalRule system, while SU.Rule is nothing else than MT's DynamicRule. MT does not have yet knowledge of ACRule but that would be really cool to have. Ideas:Benefits SU -> MT
Benefits MT -> SU
Patterntype hierarchy from MT, which should be decoupled from the rewrite systems and the syntax used.~x::SomeTypeand~x::(y->somepredicate(y))Inconsistencies
PatTermused to build the egraphs VM pattern matcher programs and for classical patt. matching via dispatch, is based on the design ofExpr. This means that common head symbols are used like this:PatTerm(:call, :f, 1, :a). This falls again to the problem of rewriting onExprin SU with TermInterface.jl. If such a shared classical rewriting backend exists, it should be able to rewrite on any type satisfying at least the core of TermInterface. SU patterns and expressions, on the other hand, are built off SU symbolic types which implicitly handle:call-like patterns. To circumnavigate this issue i've added a temporary solution to MT,iscall(x::<:Symbolic) = truesuch that symbolic Terms where operation is not:callcan still match againstPatExpr(:call, .... This is a temporary hack that has to be formalized, tested and documented, but it works for the Symbolics optimization PR. I believe that both egraph rewrite systems and classical rewrite systems should be able to handle both kind of types with the same pattern matching syntax and systems, and can be used interchangeably. *We don't know how SU behaves when fed with symbolic expression types that do not support symtype or metadata. This is because it was not built to rewrite on types such asExpr, and users should not attempt to do this by now until we find a solution.operationis :call or :ref or other non-function-typed operators, could this be changed to be as general as possible? In SU, rules are only dynamic. It means that the operators that appear on the right hand side have to be defined for the symbolic types. It means that in order to rewrite Julia code itself with SU, the user has to override all the methods that the RHSs of rules reference, to dispatch against Symbol and Expr. This may be annoying if an user is trying to use classical rewriting to change a very large julia program with a very large rewrite system. Sometimes, symbolic only behaviour where the RHS pattern variables are just dictionary-substituted is desirable. It may not be a problem by now for the current scope of SU, but if we'd like to make the rewriting and rule definition systems shared and decoupled both kinds of behavior should be supported.