Q: Using TermInterface to set up Metatheory

[Audrius-St]

Hello,

While I have been using Symbolics and SymbolicUtils for some time now [and greatly appreciate, having switched from Sympy], I am a novice in the use of Metatheory.

My first attempt to set up Metatheory using TermInterface as described in the documentation is the code below. The test expression is part of a much larger expression which I previously simplified using Symbolics.

Several questions regarding implementation regarding which I would appreciate any insights:

1. Does the symbolic expression - Metatheory handle indexed coefficients such as c[0:n]?
2. What does the expression @commutative_monoid (*) 1 mean?
3. In the @theory term-rewriting, does my addition (a / c) + (b / c) --> (a + b) / c make sense?
4. What is the symbolic expression :h in and the [4] correspond to in hcall = MyExpr(:h, [4], "hello")
5. What does [2] correspond to in ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])
6. How do I set up the following code fragment

    hcall = MyExpr(:h, [4], "hello")
    ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])
    g = EGraph(ex; keepmeta = true)

for my use case?

Julia 1.9.4
Metatheory 2.0.2

# test_metatheory.jl

using Metatheory
import Metatheory: @rule
using Metatheory.EGraphs
using Metatheory.Library
using TermInterface
using Test

# Custom Expr type
struct MetaExpr
    head::Any
    args::Vector{Any}
    meta_str::String # additional metadata
end

# Define equality for MetaExpr expression
function Base.:(==)(a::MetaExpr, b::MetaExpr)
    a.head == b.head && a.args == b.args && a.meta_str == b.meta_str
end

# create a term that is in the same closure of types of x
function TermInterface.similarterm(
            x::MetaExpr,
            head,
            args; 
            metadata = nothing,
            exprhead = :call)
    MetaExpr(head, args, isnothing(metadata) ? "" : metadata)
end

# Add metadata information for compatibility with SymbolicUtils.jl
function EGraphs.egraph_reconstruct_expression(
            ::Type{MetaExpr},
            op,
            args;
            metadata = nothing,
            exprhead = nothing)
    MetaExpr(op, args, (isnothing(metadata) ? () : metadata))
end

begin
    MetaExpr(head, args) = MetaExpr(head, args, "")
    MetaExpr(head) = MetaExpr(head, [])

    # Override istree()
    TermInterface.istree(::MetaExpr) = true

    # Specify a node's represented operation
    TermInterface.exprhead(::MetaExpr) = :call

    # Specify how to extract the children nodes
    TermInterface.arguments(e::MetaExpr) = e.args

    # Specify that all expressions of type MetaExpr can be represented (and matched against) 
    # by a pattern that is represented by a :call Expr.
    TermInterface.metadata(e::MetaExpr) = e.meta_str

    cmmttv_monoid = @commutative_monoid (*) 1;
    t = @theory a b c begin
        a + 0 --> a
        a + b --> b + a
        a + inv(a) --> 0 # inverse
        a + (b + c) --> (a + b) + c
        a * (b + c) --> (a * b) + (a * c)
        (a * b) + (a * c) --> a * (b + c)
        a * a --> a^2
        a --> a^1
        a^b * a^c --> a^(b+c)
        (a / c) + (b / c) --> (a + b) / c
        a::Number + b::Number => a + b
        a::Number * b::Number => a * b
    end
    t = cmmttv_monoid ∪ t;   
    
    n = 6
    @variables z
    @variables c[0:n]

    # Test expression - simplify to rational expression
    # Known simplification result:
    # expr = 
    #   (-c[0]*c[1]*c[2]*(c[4]^2)*c[6]*(z^2) + c[0]*c[1]*c[2]*c[4]*(c[5]^2)*(z^2) + c[0]*c[1]*(c[3]^2)*c[4]*c[6]*(z^2)
    #    - c[0]*c[1]*(c[3]^2)*(c[5]^2)*(z^2) + c[0]*(c[2]^2)*c[3]*c[4]*c[6]*(z^2) - c[0]*(c[2]^2)*(c[4]^2)*c[5]*(z^2)
    #    - c[0]*c[2]*(c[3]^3)*c[6]*(z^2) + c[0]*c[2]*c[3]*(c[4]^3)*(z^2) + c[0]*(c[3]^4)*c[5]*(z^2) - c[0]*(c[3]^3)*(c[4]^2)*(z^2))
    # / ((-c[1]*c[3]*c[5] + c[1]*(c[4]^2) + (c[2]^2)*c[5] - 2.0c[2]*c[3]*c[4] + c[3]^3)*c[3])
    expr = 
        :(
            ((((-c[0]*(c[4]^3)) / c[3] + (-c[0]*c[2]*(c[5]^2)) / c[3] + (c[0]*c[2]*(c[4]^2)*c[5]) / (c[3]^2) +
            c[0]*c[4]*c[5])*(z^3)) / (-c[3] + (c[2]*c[4]) / c[3]) + (-c[0]*c[4]*c[5]*(z^3)) / c[3] +
            c[0]*c[6]*(z^3)) / (-c[3] + (c[1]*c[5]) / c[3] + ((c[1]*(c[4]^2)) / c[3] + ((c[2]^2)*c[5]) / c[3] +
            (-c[1]*c[2]*c[4]*c[5]) / (c[3]^2) - c[2]*c[4]) / (-c[3] + (c[2]*c[4]) / c[3]))
        )
    @show expr
    println("")    

    #= How to set up the following code for the above expr?
    hcall = MetaExpr(:h, [4], "hello")
    ex = MetaExpr(:f, [MetaExpr(:z, [2]), hcall])
    g = EGraph(ex; keepmeta = true)
    =#
end

[0x0f0f0f]

Hi! I'm sorry for the late reply, it will take me a while to look at this, as I'm currently slowly working on the internals, I'm focusing on achieving good performance and to solidify the package. Please note that with #177 TermInterface.jl has been temporarily deprecated, and there's no more egraph_reconstruct_expression, and you do not need to specify any method for integrating some expression type with e-graphs.

I'm using an internal version Metatheory.TermInterface as we're actively discussing what can be the future of a shared term interface.

Please keep an eye on the "custom expression types" tutorial page for more developments :)

[Audrius-St]

Hi! I'm sorry for the late reply, it will take me a while to look at this,

No worries.

as I'm currently slowly working on the internals, I'm focusing on achieving good performance and to solidify the package. Please note that with #177 TermInterface.jl has been temporarily deprecated, and there's no more egraph_reconstruct_expression, and you do not need to specify any method for integrating some expression type with e-graphs.

I'm using an internal version Metatheory.TermInterface as we're actively discussing what can be the future of a shared term interface.

Please keep an eye on the "custom expression types" tutorial page for more developments :)

Thank you for your update and detailed explanation. Appreciated.

Will await an announcement of a new Metatheory release.

While you clearly have more than enough to keep you currently busy, I would like to suggest that at some point in the future considering the specific case of Horner optimization with common subexpression elimination for multivariate polynomials. I think that this would be of general interest.

The reference for the method I'm currently using is Why Local Search Excels in Expression Simplification (https://doi.org/10.48550/arXiv.1409.5223)

In my work, I can attain up to an order of magnitude reduction in the number of basic floating point operations. The authors give examples wherein the reductions are multiple orders of magnitude.