# Q: Using TermInterface to set up Metatheory

**URL:** <https://discourse.julialang.org/t/q-using-terminterface-to-set-up-metatheory/106480>\
**Category:** Modelling & Simulations\
**Tags:** question, metatheory, terminterface\
**Created:** [November 20, 2023, 6:22pm UTC](https://discourse.julialang.org/t/q-using-terminterface-to-set-up-metatheory/106480 "2023-11-20T18:22:43Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![Audrius-St](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/audrius-st/32/24175_2.png) [@Audrius-St](https://discourse.julialang.org/u/Audrius-St)\
**Post date:** [November 20, 2023, 6:22pm UTC](https://discourse.julialang.org/t/q-using-terminterface-to-set-up-metatheory/106480/1 "2023-11-20T18:22:43Z")

</div>

While I have been using Symbolics and SymbolicUtils for some time now , I am a novice in the use of Metatheory.

My first attempt to set up Metatheory using TermInterface as described in the [documentation](https://juliasymbolics.github.io/Metatheory.jl/stable/tutorials/custom_types/#Interfacing-with-Metatheory.jl) is opened as an Issue in Metatheory:

> <https://github.com/JuliaSymbolics/Metatheory.jl/issues/173>
>
> 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\](https://juliasymbolics.github.io/Metatheory.jl/stable/tutorials/custom\_types/#Interfacing-with-Metatheory.jl) 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
> \`\`\`

I am having difficulty understanding the following code fragment in the documentation:

With

```julia
t = @theory a begin
  f(z(2), a) --> f(a)
end

```

in the code fragment

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

```

1. What is the symbolic expression `:h` in and the `[4]` correspond to in `hcall = MyExpr(:h, [4], "hello")`
2. What does `[2]` correspond to in `ex = MyExpr(:f, [MyExpr(:z, [2]), hcall])`
3. How do I convert this code fragment to my use case?

Any insight would be appreciated.