Scope of classic @rule matcher

[Audrius-St]

Same issue as reported in SymbolicUtils.jl: reversing the order of two differential operators

# test_simple_rewrite.jl

using Symbolics, Metatheory.Rewriters

begin
    @variables x, t, f(x, t)
    Dx = Differential(x)
    Dt = Differential(t)
    rule = @rule Dt(Dx(~g)) => Dx(Dt(~g))
    rewriter = Chain([rule])
    func = Symbolics.unwrap(Dt(Dx(f)))
    rewriter(func)
end

returns the correct reorder Differential(x)(Differential(t)(f(x, t)))

However, inserting the above code into a function

# test_simple_rewrite_main.jl

using Symbolics, Metatheory.Rewriters

function main()
    @variables x, t, f(x, t)
    Dx = Differential(x)
    Dt = Differential(t)
    rule = @rule Dt(Dx(~g)) => Dx(Dt(~g))
    rewriter = Chain([rule])
    func = Symbolics.unwrap(Dt(Dx(f)))
    rewriter(func)

end

begin
    main()
end

returns the incorrect Differential(t)(Differential(x)(f(x, t))). The differential operators Dt and Dx are not reordered.

As noted by bowenszhu, placing the construction of the differential operators outside of the function

# test_simple_rewrite_main.jl

using Symbolics, Metatheory.Rewriters

@variables x, t, f(x, t)
Dx = Differential(x)
Dt = Differential(t)

function main()
    rule = @rule Dt(Dx(~g)) => Dx(Dt(~g))
    rewriter = Chain([rule])
    func = Symbolics.unwrap(Dt(Dx(f)))
    rewriter(func)

end

begin
    main()

end

again returns the correct reorder Differential(x)(Differential(t)(f(x, t)))

Julia 1.8.0 Symbolics.jl 4.10.4 Metatheory.jl 1.3.4

[willow-ahrens]

Perhaps this is https://github.com/JuliaSymbolics/Metatheory.jl/issues/87?

[0x0f0f0f]

Solving in #144

[0x0f0f0f]

cc @shashi

[0x0f0f0f]

Releasing 2.0 . Closing

[Audrius-St]

Thank you for your update.

It seems that I misunderstood as to what package is being called in the above code example.

# test_simple_rewrite_main.jl

using Symbolics, Metatheory.Rewriters

function main()
    @variables x, t, f(x, t)
    Dx = Differential(x)
    Dt = Differential(t)
    rule = @rule Dt(Dx(~g)) => Dx(Dt(~g))
    rewriter = @show Chain([rule])
    func = Symbolics.unwrap(Dt(Dx(f)))
    rewriter(func)

end

begin
    main()
end

rewriter = @show Chain([rule]) calls SymbolicUtils

Chain([rule]) = Chain(SymbolicUtils.Rule{SymbolicUtils.BasicSymbolic{Any}, . . .

not Metatheory.Rewriters

Out of curiosity I tried

rewriter = @show Metatheory.Rewriters.Chain([rule])

which requires Metatheory. Including Metatheory generates an error message

WARNING: both Metatheory and Symbolics export "@rule"; uses of it in module Main must be qualified
ERROR: LoadError: UndefVarError: @rule not defined

So

rule = Metatheory.@rule Dt(Dx(~g)) => Dx(Dt(~g))

which gives the incorrect result

Metatheory.Rewriters.Chain([rule]) = Chain(DynamicRule[Differential(Differential(~g)) => Dx(Dt(g))])

Differential(t)(Differential(x)(f(x, t)))

whereas

rule = Symbolics.@rule Dt(Dx(~g)) => Dx(Dt(~g))

does gives the correct result

Metatheory.Rewriters.Chain([rule]) = Chain(SymbolicUtils.Rule{SymbolicUtils.BasicSymbolic{Any},  . . .

Differential(x)(Differential(t)(f(x, t)))

as bowenszhu reported in #460

Is the syntax I'm using for

rule = Metatheory.@rule Dt(Dx(~g)) => Dx(Dt(~g))

incorrect?

[0x0f0f0f]

SymbolicUtils 1.0 no longer depends on Metatheory.jl

[Audrius-St]

I see. Thanks for solving the issue in SymbolicUtils.