Slotted E-Graphs: Lambda Calculus with Quail

Mix.install([
  {:quail, path: "/Users/quinn/dev/beam_box/quail"}
])

Overview

Quail is a pedagogical egglog implementation in Elixir — e-graphs plus equality saturation. This notebook demonstrates slotted e-graphs, an extension that gives the e-graph first-class knowledge of variable binding.

With slotted e-graphs:

• Alpha-equivalence is automatic — λx. x and λy. y are identified as the same term
• Beta-reduction becomes a rewrite rule — (λx. body) arg → body[x := arg]
• Capture-avoiding substitution is built in — no de Bruijn indices needed

The key idea (from PLDI 2025): e-classes are parameterized by slots (abstract variable names). Each child reference carries a slot map recording how the parent’s variable context maps to the child’s. Binder nodes introduce slots that are internal to the class. Alpha-equivalent terms hash to the same e-node.

The API

Three new primitives extend the Quail API for working with variable binding:

These compose with the existing v(:name) pattern variables and Rewrite.rewrite/3 to express binding-aware rewrite rules.

Alpha-Equivalence

The most fundamental property of slotted e-graphs: terms that differ only in bound variable names are automatically identified. No explicit alpha-conversion rules needed.

import Quail, only: [v: 1, bind: 2, slot: 1, subst: 3]
alias Quail.Rewrite

db = Quail.new()

# lambda x. x  and  lambda y. y — same term, different bound variable names
{lam_x, db} = Quail.add_term(db, {:lam, bind(:x, slot(:x))})
{lam_y, db} = Quail.add_term(db, {:lam, bind(:y, slot(:y))})

IO.puts("lambda x. x  =>  class #{lam_x}")
IO.puts("lambda y. y  =>  class #{lam_y}")
IO.puts("Same class?  #{lam_x == lam_y}")

Both terms land in the same e-class. The slot names :x and :y are internal — once the binder captures them, the e-graph only sees the structure (a lambda that returns its argument). This is exactly how a mathematician treats bound variables: they’re placeholders, not identities.

Free vs Bound Slots

A slot is free if no enclosing binder captures it, and bound otherwise. The e-graph tracks this per class:

db = Quail.new()

# A free variable reference
{free_id, db} = Quail.add_term(db, {:var, slot(:x)})
IO.puts("Free slot in {:var, slot(:x)}?  #{Quail.slot_free_in?(db, :x, free_id)}")

# A bound variable — the binder captures the slot
{bound_id, db} = Quail.add_term(db, bind(:x, {:var, slot(:x)}))
IO.puts("Free slot in bind(:x, {:var, slot(:x)})?  #{Quail.slot_free_in?(db, :x, bound_id)}")

Beta-Reduction

The classic computation rule of lambda calculus: (lambda x. body) arg -> body[x := arg]. With slotted quail, this is a one-line rewrite rule:

beta = Rewrite.rewrite(:beta,
  {:app, {:lam, bind(:x, v(:body))}, v(:arg)},
  subst(v(:body), :x, v(:arg))
)

The key pieces:

• bind(:x, v(:body)) — pattern matches a binder, capturing the body
• v(:arg) — captures the argument
• subst(v(:body), :x, v(:arg)) — replaces slot :x in the body with the argument

Let’s apply it to (lambda x. x) 5 — the identity function applied to 5:

db = Quail.new()

# (lambda x. x) 5
{root, db} = Quail.add_term(db, {:app, {:lam, bind(:x, slot(:x))}, {:num, 5}})

result = Quail.run(db, [beta], iter_limit: 10)
{:ok, extracted} = Quail.extract(result.database, root)

IO.inspect(extracted, label: "(lambda x. x) 5")

The substitution correctly replaces the slot reference with the argument, yielding {:num, 5}.

Beta with Compound Bodies

The real power shows when the lambda body is more complex. Here (lambda x. x + 1) 5:

db = Quail.new()

{root, db} = Quail.add_term(db,
  {:app,
   {:lam, bind(:x, {:add, slot(:x), {:num, 1}})},
   {:num, 5}}
)

result = Quail.run(db, [beta], iter_limit: 10)
{:ok, extracted} = Quail.extract(result.database, root)

IO.inspect(extracted, label: "(lambda x. x + 1) 5")

The substitution walks through the :add node, replacing only the slot reference to :x with {:num, 5}, leaving {:num, 1} untouched.

Composing Rules: Beta + Arithmetic

Equality saturation shines when multiple rewrite rules compose. Let’s add a constant-folding rule alongside beta:

const_add = Rewrite.rewrite(:const_add,
  {:add, {:num, v(:a)}, {:num, v(:b)}},
  {:num, v(:c)},
  when: fn %{a: a, b: b}, _db -> %{c: a + b} end
)

db = Quail.new()

# (lambda x. x + 1) 5
{root, db} = Quail.add_term(db,
  {:app,
   {:lam, bind(:x, {:add, slot(:x), {:num, 1}})},
   {:num, 5}}
)

result = Quail.run(db, [beta, const_add], iter_limit: 20)
{:ok, extracted} = Quail.extract(result.database, root)

IO.puts("(lambda x. x + 1) 5")
IO.puts("  beta:  {:add, {:num, 5}, {:num, 1}}")
IO.puts("  fold:  #{inspect(extracted)}")
IO.puts("")
IO.puts("Saturated in #{result.iterations} iterations (#{result.stop_reason})")

The e-graph discovers (lambda x. x + 1) 5 = 5 + 1 = 6 through two composed rewrites — beta-reduction followed by constant folding. The cost-based extractor picks {:num, 6} as the cheapest equivalent term.

How It Works Internally

Under the hood, slotted e-graphs represent variable binding through three mechanisms:

1. Slot normalization — When an e-node is added, its slot names are normalized to canonical form (:s0, :s1, …). This means bind(:x, slot(:x)) and bind(:y, slot(:y)) produce identical normalized e-nodes and hash to the same entry.

2. Slot maps on children — Each child reference {child_id, slot_map} carries a mapping from the child’s canonical slot names to the parent’s. This lets the parent distinguish which variable each child slot represents, even though the child doesn’t know its own name.

3. Substitution builds new nodes — do_subst walks the body’s e-nodes, finds child references whose slot maps point to the target variable, and builds new e-nodes with the argument spliced in. It never merges the shared slot class (which would corrupt all variable references).

db = Quail.new()

# Inspect the e-graph structure for bind(:x, slot(:x))
{id, db} = Quail.add_term(db, {:lam, bind(:x, slot(:x))})

# The class has no free slots — the binder captures the only variable
free = Quail.EGraph.class_slots(db.egraph, id)
IO.puts("Free slots in (lambda x. x): #{inspect(MapSet.to_list(free))}")

# But the body (inside the binder) does have a free slot
nodes = Quail.EGraph.class_nodes(db.egraph, id) |> MapSet.to_list()
IO.puts("E-nodes in class: #{inspect(nodes, pretty: true)}")

What’s Next

With slotted e-graphs as a foundation, the rewrite rule language can express the full spectrum of binding-aware transformations:

• Eta-reduction: lambda x. f x -> f (when x not free in f)
• Let-floating: f(let x = e in body) -> let x = e in f(body)
• Function composition fusion: map(map(xs, f), g) -> map(xs, g . f)

These all require capture-avoiding substitution through binders — exactly what slotted e-graphs provide.