# 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:
```bash
cargo --version
rustc --version
dot -V
```
If Cargo is installed through rustup, make sure Livebook sees it:
```bash
export PATH="$HOME/.cargo/bin:$PATH"
livebook server
```
When using the published package, replace the dependency with `{:egglog_elixir, "~> 0.1"}`.
```elixir
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.
```elixir
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.
```elixir
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.
```elixir
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.
```elixir
snapshot = Egglog.snapshot!(math, input)
GettingStarted.snapshot_summary(
Egglog.snapshot!(math, input, render: :json)
)
```
```elixir
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.
```elixir
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.
```elixir
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`.
```elixir
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)
```
```elixir
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.
```elixir
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.
```elixir
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.
```elixir
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.
```elixir
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.
```elixir
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)
```
```elixir
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.
```elixir
{:ok, egraph} =
Egglog.EGraph.new("""
(datatype Math
(Num i64)
(Add Math Math))
""")
```
Each successful `run/3` mutates this one native session.
```elixir
{: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.
```elixir
{:ok, true} = Egglog.EGraph.check(egraph, "(= x (Num 1))")
{:ok, "(Num 1)"} = Egglog.EGraph.extract(egraph, "x")
```
```elixir
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.