topic 44: e-graphs as a database, and the two testing systems topic 16 only named - #5
Merged
Merged
Conversation
…only named Topic 44 — E-graphs as a Database: Relational E-matching & egglog. The sequel to topic 21, placed here because the fix for equality saturation's bottleneck came out of the database literature: e-matching is 60-90% of its run time (POPL'22 §1) and it is a conjunctive query. Lane 1, provided: on the POPL'22 Figure 2 e-graph (3N e-nodes standing for N²+2N terms), the pattern f(a, g(a)) has N matches and costs a backtracking matcher N²+N+1 units of work while generic join does 5N — 2,561,601 against 8,000 at N=1600, a measured 21.72x. Both counters are closed forms and reproduce exactly. The second table is the honest one: rename the repeated variable, the pattern goes linear, every candidate becomes an answer, and generic join comes out 0.56x — 1.8x slower. Same result POPL'22 reports in Table 1's Worst column (0.76, and 0.03 with index building charged). Theorem 10's O(sqrt(|Q(I)| · prod|Ri|)) predicts both rows: 64,000 against 8,000 measured, and 2,560,000 against 2,561,603 measured, i.e. *at* the bound. Lane 2 prices naive evaluation without implementing the fix: a 24-tuple delta re-derives 20,008 matches with 100,040 probes for 8 new answers. Lane 3's generator keeps the answer size flat at (E/V)³ = 125 while the graph grows 8x, so generic join's probes grow linearly and the binary plan's intermediate — the reader's stub — grows as E²/V. experiments/: a minimal e-graph, egg's Bind/Compare/Scan VM with the op index (so the baseline is a strategy, not a strawman), Figure 8's unnesting, tries, most-constrained-first ordering, generic join. Six provided tests pass; four stub tests are the specification (semi-naive evaluation, and a left-deep binary-join plan for the triangle multi-pattern). Four reading guides. The source guide's finding is that the papers understate the codebase: core-relations is a database, semi-naive evaluation is a binary search on a clustered sort column (table/mod.rs:497-510), the planner does hypertree decomposition with a min-fill heuristic (plan.rs:1-46), and congruence closure is compiled into a rule rather than implemented (egglog-bridge/src/lib.rs:945). egglog's union-find declines union-by-rank for union-by-min-id and says why — the same class of finding as egg's non-compressing find. Topic 16 gains the two guides it had been name-dropping: - reading-hypothesis.md — shrinking the choice sequence rather than the value; shortlex order worked on real indices; the shrink-pass determinism invariant; the DataTree as a trie over executions; and Hypothesis's documented deviation from the swarm-testing paper. find_integer(100) was executed rather than hand-traced: 16 calls. - reading-antithesis.md — read against the open SDK, since the platform is closed. The no-caching contract on get_random only makes sense for a branching simulation, not a replayed one; Sometimes as a coverage property (crash_matrix's None row is the hand-rolled version); the linker-assembled assertion catalog; guidance as Hypothesis's target phase at fleet scale. No Antithesis figure is quoted, because none can be checked from this side. One benchmark bug, caught by the counters disagreeing with the clock: gj allocated a Vec per intersection key, which left every counter identical and doubled the wall clock. Plumbing: PLAN.md §44 and the map, FINDINGS row, verify.sh lane, PROGRESS status + M44, SUMMARY entries, SESSION-LOG entry, topic counts 44 -> 45 and crate count 45 -> 46. Pin table regenerated: adds egglog, hypothesis, antithesis-sdk-rust and y-crdt, and refreshes mention counts that had gone stale since the guides doubled in size. Gates: verify.sh 44 PASS, check-reading-depth.py --check --all 236/236, pin-table.py --check current, mdbook build clean, mermaid validated, no broken relative links. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Topic 44 — E-graphs as a Database: Relational E-matching & egglog
The sequel to topic 21, placed in this repo because the fix for equality saturation's next bottleneck came out of the database literature. E-matching is 60–90% of equality saturation's run time (POPL'22 §1) and it is a conjunctive query: the e-graph is a set of tables, the pattern is a query, and the equality constraint a backtracking matcher checks last is a join key.
The measured headline (
./verify.sh 44, Apple M3 Pro)On the POPL'22 Figure 2 e-graph — 3N e-nodes standing for N²+2N terms — the pattern
f(a, g(a))has N matches:bt visits = N²+N+1,gj probes = 5N. Both are closed forms and reproduce exactly; only the µs columns are hardware-dependent.And the negative result is a column, not a caveat. Rename the repeated variable —
f(a, g(b)), a linear pattern — and every candidate becomes an answer: generic join does the same work through a more expensive instruction and comes out 0.56×, i.e. 1.8× slower. POPL'22 reports its own version (Table 1'sWorstcolumn: 0.76, and 0.03 with index building charged). Theorem 10 predicts both rows.What's in the package
experiments/— a minimal e-graph, egg'sBind/Compare/ScanVM with the op index so the baseline is a real strategy rather than a strawman, Figure 8's unnesting, tries, generic join. 6 provided tests pass, 4 stub tests are the spec (semi-naive evaluation; a left-deep binary-join plan for the triangle multi-pattern).The source guide's finding is that the papers understate the codebase —
core-relationsis a database: semi-naive evaluation is a binary search on a clustered sort column, the planner does hypertree decomposition with a min-fill heuristic, and congruence closure is compiled into a rule rather than implemented. Its union-find declines union-by-rank for union-by-min-id and explains why, which is the same class of finding as egg's non-compressingfind.Topic 16 — the two systems it had only name-dropped
DataTreeas a trie over executions; and Hypothesis's documented deviation from the swarm-testing paper.find_integer(100)was executed rather than hand-traced: 16 calls, not the 17 a trace produced.get_randomonly makes sense for a branching simulation, not a replayed one;Sometimesas a coverage property (this topic'scrash_matrixNonerow is the hand-rolled version); the linker-assembled assertion catalog. No Antithesis figure is quoted, because none can be checked from this side, and the guide says so.Reviewer notes
gjallocated aVecper intersection key, which left every counter identical and doubled the wall clock. Recorded innotes.md.notes.mdsays so.GraphRAG-SDKhad disappeared from~/repos, so the tool dropped it and would have orphaned topic 38's anchors — re-cloned at its pinnedf42ab3d, so no row is lost. Three of the maintainer's own clones have advanced since the table was last written (FalkorDBccb449a9a→aa75821ab,falkordb-py,falkordb-rs-next-gen), so FalkorDB anchors in existing guides now name a newer commit than they were verified against. Easy to pin back if preferred.topics/*/experiments/Cargo.lockfiles (topics 17–32) were left alone as out of scope.Gates
./verify.sh 44— PASScheck-reading-depth.py --check --all— 236/236pin-table.py --check— currentmdbook buildclean; mermaid validated with@mermaid-js/mermaid-cli; 0 broken relative links;-D warningsbuild clean🤖 Generated with Claude Code