Getting Started With Egglog Elixir

Prerequisites

This notebook uses egglog_elixir, which includes a Rustler NIF. Rustler compiles a small native Rust library the first time Livebook evaluates Mix.install/1.

The Livebook runtime must have:

• Rust installed
• cargo available on PATH
• Graphviz installed, with dot available on PATH, if you want SVG e-graph pictures

Check this in the same shell or container that starts Livebook:

cargo --version
rustc --version
dot -V

If Cargo is installed through rustup, make sure Livebook sees it:

export PATH="$HOME/.cargo/bin:$PATH"
livebook server

When using the published package, replace the dependency with {:egglog_elixir, "~> 0.1"}.

Mix.install([
  {:egglog_elixir, path: Path.expand("..", __DIR__)},
  {:kino, "~> 0.19.0"}
])

What This Notebook Teaches

This is a first-pass tour of the wrapper. It keeps the egglog language visible and uses Elixir only to load theories, submit problems, print outputs, and render snapshots.

The examples are a small "best of" from the first three upstream egglog tutorial chapters:

• equality saturation over symbolic arithmetic
• congruence closure through constructors
• Datalog-style reachability
• analysis facts used as guards for rewrites
• the difference between Egglog.Program and Egglog.EGraph

The important boundary is:

• egglog does parsing, e-matching, congruence closure, Datalog evaluation, rebuilding, scheduling, and extraction
• Elixir submits source/input and receives outputs
• snapshots come from native egglog serialization, not from an Elixir graph reconstruction

Tiny Helpers

These helpers are display-only. They do not run egglog.

defmodule GettingStarted do
  def print_output(result, type) do
    result.outputs
    |> Enum.filter(&(&1.type == type))
    |> Enum.map(& &1.text)
    |> Enum.reject(&is_nil/1)
    |> Enum.map(&String.trim_trailing/1)
    |> Enum.reject(&(&1 == ""))
    |> Enum.each(&IO.puts/1)
  end

  def print_outputs(result) do
    result.outputs
    |> Enum.map(& &1.text)
    |> Enum.reject(&is_nil/1)
    |> Enum.map(&String.trim_trailing/1)
    |> Enum.reject(&(&1 == ""))
    |> Enum.each(&IO.puts/1)
  end

  def show_run(result) do
    %{
      status: result.status,
      stats: result.stats
    }
  end

  def render_snapshot(%{format: :svg, svg: svg}) when is_binary(svg) do
    kino_html = Module.concat(Kino, HTML)

    if Code.ensure_loaded?(kino_html) do
      apply(kino_html, :new, [svg])
    else
      svg
    end
  end

  def render_snapshot(%{text: text}), do: text

  def snapshot_summary(snapshot) do
    summary = Egglog.Snapshot.summary(snapshot)

    %{
      e_nodes: summary.nodes,
      e_classes: summary.classes,
      by_operator: summary.operators,
      omitted: summary.omitted
    }
  end
end

1. A Loaded Program

Use Egglog.Program when you have a reusable theory and want each query to be isolated from the others.

The theory below declares a tiny arithmetic language and a few equations. In universal-algebra terms, the datatype gives us a finite signature; the rewrite rules generate equalities in the quotient term algebra.

math_theory = """
(datatype Math
  (Num i64)
  (Var String)
  (Add Math Math)
  (Mul Math Math))

(rewrite (Add (Num a) (Num b)) (Num (+ a b)))
(rewrite (Mul (Num a) (Num b)) (Num (* a b)))
(rewrite (Add (Mul a x) (Mul b x)) (Mul (Add a b) x))
(rewrite (Add x (Num 0)) x)
(rewrite (Mul x (Num 1)) x)
"""

math = Egglog.Program.load!(math_theory)

Now submit one query-local term and ask for extraction.

input = %{
  terms: %{
    "goal" => "(Add (Mul (Num 3) (Var \"x\")) (Mul (Num 4) (Var \"x\")))"
  },
  budget: %{rounds: 5},
  requests: [%{type: :extract, expr: "goal"}]
}

result = Egglog.Program.run!(math, input)

GettingStarted.print_output(result, :extract)
GettingStarted.show_run(result)

The extracted term is the representative chosen by egglog after saturation. Elixir did not simplify the expression. Native egglog matched the rewrite schemas, added equalities, rebuilt congruence closure, and extracted a cheap representative.

2. Looking Inside

Most egglog commands are quiet when they succeed. A snapshot lets us inspect what native egglog built.

snapshot = Egglog.snapshot!(math, input)

GettingStarted.snapshot_summary(
  Egglog.snapshot!(math, input, render: :json)
)

GettingStarted.render_snapshot(snapshot)

The picture is not a rewrite trace. Equality saturation keeps several equivalent syntactic forms in one e-class and postpones the choice of a concrete representative until extraction.

3. Checks And Congruence Closure

Checks are assertions about the current e-graph. With Egglog.Program, we can add query-local unions without mutating the loaded base.

congruence_theory = """
(datatype Term
  (A)
  (B)
  (Wrap Term)
  (Pair Term Term))
"""

cc = Egglog.Program.load!(congruence_theory)

First, without an equality between A and B, the two context terms are distinct.

before_union =
  Egglog.Program.run!(cc, %{
    terms: %{
      "left" => "(Pair (Wrap (A)) (A))",
      "right" => "(Pair (Wrap (B)) (B))"
    },
    requests: [
      %{type: :extract, expr: "left"},
      %{type: :extract, expr: "right"}
    ]
  })

GettingStarted.print_outputs(before_union)

Now assert A = B for this query. Congruence closure propagates that equality through Wrap and Pair.

after_union_input = %{
  terms: %{
    "left" => "(Pair (Wrap (A)) (A))",
    "right" => "(Pair (Wrap (B)) (B))"
  },
  unions: [{"(A)", "(B)"}],
  budget: %{rounds: 1},
  requests: [
    "(check (= left right))",
    %{type: :extract, expr: "left"}
  ]
}

after_union = Egglog.Program.run!(cc, after_union_input)

GettingStarted.print_output(after_union, :extract)
GettingStarted.show_run(after_union)

Egglog.snapshot!(cc, after_union_input)
|> GettingStarted.render_snapshot()

The equality was asserted only at the leaves, but native rebuild maintains the congruence invariant: equal children imply equal parent applications.

4. Datalog Facts

Egglog is also a Datalog-style engine. Relations are represented as unit-valued functions, and rules derive new rows.

This example computes transitive reachability.

reachability_theory = """
(relation edge (i64 i64))
(relation path (i64 i64))

(rule ((edge x y))
      ((path x y)))

(rule ((path x y) (edge y z))
      ((path x z)))
"""

reach = Egglog.Program.load!(reachability_theory)

Submit a small graph as query-local facts.

reach_input = %{
  facts: [
    "(edge 1 2)",
    "(edge 2 3)",
    "(edge 3 4)"
  ],
  budget: %{rounds: 5},
  requests: [
    "(check (path 1 4))",
    %{type: :print_function, name: "path", limit: 20}
  ]
}

reach_result = Egglog.Program.run!(reach, reach_input)

GettingStarted.print_output(reach_result, :print_function)
GettingStarted.show_run(reach_result)

The interesting point is that the same native runtime is maintaining both relations and equality. We will use that combination in the next example.

5. Analysis Facts Guard Rewrites

Many equations are valid only under hypotheses. Instead of writing an Elixir callback, keep the hypothesis in egglog as a relation.

Here (Div x x) = 1 is allowed only when x is known to be non-zero.

guarded_theory = """
(datatype Math
  (Num i64)
  (Div Math Math))

(relation non-zero (Math))

(rewrite (Div x x) (Num 1)
  :when ((non-zero x)))
"""

guarded = Egglog.Program.load!(guarded_theory)

Without the fact, extraction returns the original division.

without_guard_input = %{
  terms: %{"x" => "(Div (Num 2) (Num 2))"},
  budget: %{rounds: 2},
  requests: [%{type: :extract, expr: "x"}]
}

without_guard = Egglog.Program.run!(guarded, without_guard_input)

GettingStarted.print_output(without_guard, :extract)

With the fact, the guarded rewrite fires.

with_guard_input = %{
  terms: %{"x" => "(Div (Num 2) (Num 2))"},
  facts: ["(non-zero (Num 2))"],
  budget: %{rounds: 2},
  requests: [%{type: :extract, expr: "x"}]
}

with_guard = Egglog.Program.run!(guarded, with_guard_input)

GettingStarted.print_output(with_guard, :extract)

Egglog.snapshot!(guarded, with_guard_input)
|> GettingStarted.render_snapshot()

The relation non-zero is an analysis fact. Once it is present, egglog can justify the equality between the division term and (Num 1).

6. Stateful Sessions

Egglog.Program is query-local: every run clones the loaded base and temporary facts do not accumulate. For interactive work, use Egglog.EGraph instead.

{:ok, egraph} =
  Egglog.EGraph.new("""
  (datatype Math
    (Num i64)
    (Add Math Math))
  """)

Each successful run/3 mutates this one native session.

{:ok, _} = Egglog.EGraph.run(egraph, "(let x (Add (Num 1) (Num 0)))")
{:ok, _} = Egglog.EGraph.run(egraph, "(rewrite (Add a (Num 0)) a)")

{:ok, egraph_result} =
  Egglog.EGraph.run(egraph, """
  (run 2)
  (check (= x (Num 1)))
  (extract x)
  """)

GettingStarted.print_output(egraph_result, :extract)

Because the state persists, later calls can inspect what earlier calls inserted.

{:ok, true} = Egglog.EGraph.check(egraph, "(= x (Num 1))")
{:ok, "(Num 1)"} = Egglog.EGraph.extract(egraph, "x")

Egglog.EGraph.snapshot!(egraph)
|> GettingStarted.render_snapshot()

Use the two models deliberately:

• Egglog.Program for reproducible, isolated queries against a loaded theory.
• Egglog.EGraph for REPL/Livebook sessions where state should accumulate.

What To Try Next

Natural next steps:

• Open livebooks/egglog-tutorial/01-basics.livemd for a deeper equality saturation walkthrough.
• Open livebooks/egglog-tutorial/02-datalog.livemd for more relational examples.
• Open livebooks/egglog-tutorial/03-analysis.livemd for richer analysis facts and guarded rewrites.
• Change the arithmetic rules above and watch how the snapshot changes.