{"article":{"slug":"refinement-e-graphs","title":"Refinement E-Graphs","subtitle":null,"summary":"Philip Zucker sketches refinement e-graphs, which bake a privileged <= refinement relation into an e-graph alongside equality so compiler rewrites from abstract specs to concrete programs can be modeled as one-directional, with a prototype built on microegg, a WASM demo, and notes on related term-rewriting ideas.","content_type":"blog_post","language":"en","canonical_url":"https://www.philipzucker.com/refinement_egraph/","author":{"name":"Philip Zucker","url":"https://www.philipzucker.com/","person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"Hey There Buddo!","url":"https://www.philipzucker.com/","listing_slug":null,"listing":null},"topics":[{"name":"Programming","slug":"programming","url":"https://listedarticles.com/topics/programming"},{"name":"Research","slug":"research","url":"https://listedarticles.com/topics/research"},{"name":"Mathematics","slug":"mathematics","url":"https://listedarticles.com/topics/mathematics"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":5940,"reading_minutes":26,"published_at":"2026-10-04T00:00:00.000Z","added_at":"2026-10-05T08:10:49.894Z","updated_at":"2026-10-05T08:10:49.894Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/refinement-e-graphs","markdown_url":"https://listedarticles.com/articles/refinement-e-graphs.md","example":false,"citation":"Philip Zucker, Hey There Buddo!. \"Refinement E-Graphs.\" 4 Oct 2026. https://www.philipzucker.com/refinement_egraph/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://www.philipzucker.com/refinement_egraph/"},"body_markdown":"# Refinement E-Graphs\n\nOct 4, 2026\n\nThe idea of a refinement [e-graph](https://egraphs.org/) is to add a baked in a `<=` relation that is about as privileged as the e-graph’s native `=`\n\nThere is a story that compiler rewrites are often not bidirectional equalities, but instead are unidirectional refinement rewrites, moving from an abstract or floppy program / spec to a more completely determined one that can run on a concrete machine. It is quite common for the source language to be cagey about the exact order the children of an expression are evaluated, or what is the result of an integer overflow or division by zero. Being cagey may enable more optimization opportunities or ease translation to disparate machines. It is also just a fact of life for these languages.\n\nHere is a prototype of a refinement egraph based on Max Willsey’s microegg . A WASM demo is here . Third verse same as the [second](https://www.philipzucker.com/lambda_miller_egg/)\n\n# Example: Don’t Care Circuits\n\nA nice example is “Don’t Care” in digital circuits , You may say that certain inputs are not supported to a circuit and that the result is a don’t care in that case. An optimizer is free to pick a result that allows for the most optimal circuit. I believe George Constantinides explained a version of this example to me.\n\n```\n%%file /tmp/circuit.sexp\n(fun ite (+ + +)) ; declare if-then-else as covariant in all arguments\n(rewrite (ite ?x true false) ?x) ; ordinary equality rewrite\n(ge dontcare true) ; dontcare refines to true. {True, False} >= {True}\n(ge dontcare false) ; dontcare also refines to false. {True, False} >= {False}\n\n(insert (ite x true dontcare)) ; insert starting term\n(run 5 :expand-le)\n\n(extract-le (ite x true dontcare)) ; can extract x because refining this dontcare to true enables a nice term\n```\n\n```\nWriting /tmp/circuit.sexp\n```\n\n```\n! refinement-microegg /tmp/circuit.sexp\n```\n\n```\nx\n```\n\nThere are also refinement rewrite rules available in the implementation, `rewrite-le` and `rewrite-ge`.\n\nSpiritually, `(rewrite-le lhs rhs)` represents the formula `forall ?a, lhs(?a) <= rhs(?a)`. Because of the form of this formula, we don’t have to match `lhs` on the equality nose. We can find a substitution for any starting `?t <= subst(lhs[?a])` to chain to a discovered inequality assertion `?t <= subst(lhs[?a]) <= subst(rhs[?a])`.\n\n## Don’t Care Semantics\n\nI think semantics is really important and don’t like meaningless syntax manipulation. The intended semantics of this “Don’t Care” example is `Bool -> Set Bool` with `<=` representing pointwise set containment.\n\n| Term | Semantics |\n| --- | --- |\n| `x` | `fun b => {b}` |\n| `ite(c,t,e)` | `fun b => {res for c1 in [[c]] b for res in (if c1 then [[t]] b else [[e]] b)}` |\n| `dontcare` | `fun _ => {True, False}` |\n| `true` | `fun _ => {True}` |\n| `false` | `fun _ => {False}` |\n| `t <= s` | `forall b : Bool, is_subset ([[t]] b) ([[s]] b)` |\n\n`x` could be generalized to have an algebra of more than one dimension, which would bring us back to lifting e-graphs . Refinement and Lambda afaik are orthogonal features that have no issue being bolted together. Maybe something interesting might occur in extraction (some related terms may not exist in some contexts)?\n\nNote that this inequality assertion is distinct from *equating* `dontcare = true = false`. This of course is problematic. But it is also distinct from equating to either of them `dontcare = true` or `dontcare = false`. If we did one of these, then all `dontcare` *everywhere* would be forced to be `true` or `false`, whereas we want the ability to be able to make independent choices at all usages.\nOne could perhaps make `dontcare1` `dontcare2` `dontcare3` etc as fresh constants and then independently equate them. This freshness game always feels like some goofy shell game to me though.\nThere is some intuitive sense that equating an eclass destroys it as a resource, but stating an inequality does not destroy it as a resource.\n\n# Inequality Union Finds\n\nRoughly E-Graph = Union Find + Hash Cons. So a Refinement E-graph = inequality union find + hash cons.\n\nThe interface of the inequality union find is more important than the details of the implementation.\n\n```\nfrom typing import Protocol\ntype Id = int\nclass LE_UnionFind(Protocol):\n # regular union find\n def union(self, a : Id, b : Id) -> None: ...\n def is_eq(self, a : Id, b : Id) -> bool: ...\n def find(self, a : Id) -> Id: ...\n\n # extra inequality features\n def add_le(self, a : Id, b : Id) -> None: ... # the analog of union. union = add_eq\n def is_le(self, a : Id, b : Id) -> bool: ...# analog of is_eq\n def all_le(self, a : Id) -> set[Id]: ... # returns all elements `a` is known less than or equal to. Analog of find.\n def all_ge(self, a : Id) -> set[Id]: ... # returns all elements known `a` is known greater than or equal to. Analog of find.\n```\n\nPrevious discussions of mine on inequality union finds towards refinement e-graphs:\n\n* An Inequality Union Find Inspired by Atomic Asymmetric Completion\n* Inequality Union Finds: Baby Steps to Refinement E-graphs\n\n# What Does A Refinement E-Graph Need on Top of This?\n\nAn (inequality) union find deals in atomic symbols `e4` and atomic equations `e5 = e87` (or inequations `e4 <= e65`).\n\nAn e-graph adds function symbols `f(e4,e4)` to this. These symbols appear in the following processes:\n\n* Refinement-closure\n* Refinement E-matching\n* Refinement extraction\n\nThe e-graph implementation need to be told how the function symbols play with the inequality `<=` by the user. Functions *always* respect equality `=`, but they may be monotone, anti-monotone or neither/unknown in their individual arguments. I like set difference `diff(A,B)` as an example of this. It is monotone in the first argument but anti-monotone/contravariant in the second argument `diff(+,-)`.\n\n## Refinement Closure\n\nInstead of congruence closure, we can perform refinement closure. This basically is applying a theorems like `forall a b c d, a <= b /\\ c >= d -> diff(a,c) <= diff(b,d)` instead of `a = b /\\ c = d -> diff(a,c) = diff(b, d)` which is what congruence closure applies.\n\nRefinement closure isn’t as nice as congruence closure. We can use it both in the form that makes new enodes or the form that only notes relations between pre-existing enodes. In a datalog sense, this is the difference between\n`diff(a,c) <= diff(b,d) :- a <= b, c >= d, diff(a,c)` and the guarded version `diff(a,c) <= diff(b,d) :- a <= b, c >= d, diff(a,c), diff(b,d)`. The first can be useful, but it can also be explosive.\n\n## Refinement E-matching\n\nPattern matching can be modelled as a processing a constraint set `{?p = t}` (see for example section 2.2.3 of https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf or section 4.6 of Term Rewriting and All That ). What makes it pattern matching vs unification is having variable only on one side, which is sometimes easier/more efficient to implement.\n\n![unification rules](https://www.philipzucker.com/assets/traat/unify_rules.png)\n\nFor refinement e-matching, We can be working with a constraint `{?p <= t}` or `{t <= ?p}`. But otherwise really the algorithm doesn’t change that much. You just need to track which “mode” you’re currently in, and change the mode according to the variance of the function symbols.\n\nFor example, this `diff` pattern processes by flipping one of the modes.`{diff(?a, ?b) <= diff(x,y)} ===> {?a <= x, ?b >= y}`\n\nIn the implementation, there is one extra degree of nondeterminism on top of the usual e-matching eclass->enode nondeterminsm, where in the `GE` or `LE` mode, you may traverse an eclass -> eclass `<=` edge.\n\nFrom the flattened relational e-matching perspective, this is the insertion of implicit `(le ?a ?b)` all throughout the pattern. For example the pattern`foo(bar(?x))` becomes flattened to `?e1 = foo(?e2), ?e2 <= ?e3, ?e3 = bar(?e4), ?e4 <= ?x`. `<=` kind of “mediates” between every function symbol relation.\n\n## Refinement Extraction\n\nRegular extraction is actually pretty similar to e-matching in many ways. We are seeking a `?extract = t` but we want the “best” `?extract`. We have a tendency to implement extraction bottom up instead of top down.\n\nIn refinement extraction, we can instead be asking for `?extract <= t` or `?extract >= t`. We might also want to use `<=` in our definition of “best”. Perhaps we want the most refined (which semantically might mean the most concretely implemented or most deterministic entity) and then tie break with smallest size term or vice versa.\n\n# A Toy Python Implementation of a Refinement E-Graph\n\nThis is basically a copy of my python microegg with some inequality smarts put in. There is a refinement closure step `le_cong_step` and `le_cong_step_weak` (which makes no new enodes). Because e-matching can traverse `<=` edges, you might need less materialization than you’d think.\n\nematching and extraction are keyed on `Mode` which says whether you are allowed to search up or down the `<=` or have to use on the nose `=`.\n\nThe variance table `variance : dict[str, tuple[Variance, ...]]` says the variance of each argument of the function symbol. It is kind of the same shape of data one might use for storying types of the symbols, but this implementation is untyped.\n\n```\nfrom dataclasses import dataclass, field\nfrom enum import Enum\nfrom collections import defaultdict\nimport itertools\ntype Id = int\n@dataclass(frozen=True)\nclass Node:\n f : str\n children : tuple[Id,...]\n\nclass Mode(Enum): # Expand all below, all above, or equal only. Ematch, extract, and rebuild can all be keyed on this kind of\n LE = -1\n EQ = 0\n GE = 1\n\nclass Variance(Enum): # Slash Monotonicity\n MONO = 1 # covariant\n ANTI = -1 # contravariant\n UNKNOWN = 0 # \"invariant\"\n #COVARIANT = 1 # monotone\n #CONTRAVARIANT = -1 # antitone\n #INVARIANT = 0 # neither monotone nor antitone\n def act(self, mode: Mode) -> Mode:\n match self:\n case Variance.MONO:\n return mode\n case Variance.ANTI:\n return Mode(-mode.value)\n case Variance.UNKNOWN:\n return Mode.EQ\n\nclass Term: ...\n@dataclass\nclass App(Term):\n f : str\n children : tuple[Term,...]\n def size(self) -> int: # used in extraction\n return 1 + sum(child.size() for child in self.children)\n@dataclass \nclass Var(Term):\n name : str\n\ntype Subst = dict[str, Id]\n\n@dataclass\nclass LE_EGraph():\n parents : list[Id] = field(default_factory=list)\n memo : dict[Node, Id] = field(default_factory=dict)\n uppers : list[set[Id]] = field(default_factory=list)\n lowers : list[set[Id]] = field(default_factory=list)\n variance : dict[str, tuple[Variance, ...]] = field(default_factory=dict)\n\n def get_variance(self, f: str, arity: int) -> tuple[Variance, ...]:\n sig = self.variance.get(f, (Variance.UNKNOWN,) * arity)\n assert len(sig) == arity\n return sig\n\n def find(self, a : Id) -> Id:\n while self.parents[a] != a:\n a = self.parents[a]\n return a\n def union(self, a : Id, b : Id) -> None:\n a,b = self.find(a), self.find(b)\n if a == b:\n return\n self.parents[b] = a\n self.uppers[a] |= self.uppers[b]\n self.lowers[a] |= self.lowers[b]\n def add(self, f, *args : Id) -> Id:\n args = tuple(self.find(a) for a in args)\n node = Node(f, args)\n if node in self.memo:\n return self.find(self.memo[node])\n new_id = len(self.parents)\n self.parents.append(new_id)\n self.uppers.append(set())\n self.lowers.append(set())\n self.memo[node] = new_id\n return new_id\n def is_eq(self, a : Id, b : Id) -> bool:\n return self.find(a) == self.find(b)\n def all_le(self, a : Id) -> set[Id]:\n a = self.find(a)\n u = {self.find(x) for x in self.uppers[a]}\n u.add(a) # reflexive\n todo = list(u)\n while todo:\n x = self.find(todo.pop())\n for y in self.uppers[x]:\n y = self.find(y)\n if y not in u:\n u.add(y)\n todo.append(y)\n return u\n def all_ge(self, a : Id) -> set[Id]:\n a = self.find(a)\n l = {self.find(x) for x in self.lowers[a]}\n l.add(a) # reflexive\n todo = list(l)\n while todo:\n x = self.find(todo.pop())\n for y in self.lowers[x]:\n y = self.find(y)\n if y not in l:\n l.add(y)\n todo.append(y)\n return l\n def add_le(self, a : Id, b : Id) -> None:\n a,b = self.find(a), self.find(b)\n if a == b:\n return\n self.uppers[a].add(b) # could not do so if already found. Help keep uppers sparse\n self.lowers[b].add(a)\n def is_le(self, a : Id, b : Id) -> bool:\n return self.find(b) in self.all_le(a) # We don't have to collect up all_le to compute this but this is easy\n #def cong_step(self, mode : Mode): ...\n # rebuild is applying eq_cong_step in a loop\n def eq_cong_step(self):\n for node, id in list(self.memo.items()):\n children1 = [self.find(a) for a in node.children]\n if children1 == list(node.children):\n continue\n else:\n del self.memo[node] # It is important for e-matching to remove stale nodes.\n id1 = self.add(node.f, *children1)\n self.union(id, id1) # could pollute union find less by giving a variant of self.add id\n def le_cong_step(self):\n for node, id in list(self.memo.items()):\n children = [self.find(a) for a in node.children]\n id1 = self.add(node.f, *children)\n sig = self.get_variance(node.f, len(node.children))\n for c2 in itertools.product(*[self.expand_eclass(a, v.act(Mode.LE)) for a, v in zip(node.children, sig)]):\n id2 = self.add(node.f, *c2)\n self.add_le(id, id2)\n # It is not obvious that le cong should something stale. It probably shouldn't\n def ge_cong_step(self):\n # Just the opposite directin of le_cong_step\n for node, id in list(self.memo.items()):\n children = [self.find(a) for a in node.children]\n id1 = self.add(node.f, *children)\n sig = self.get_variance(node.f, len(node.children))\n for c2 in itertools.product(*[self.expand_eclass(a, v.act(Mode.GE)) for a, v in zip(node.children, sig)]):\n id2 = self.add(node.f, *c2)\n self.add_le(id2, id)\n def le_cong_weak(self): \n # Don't make new enodes. But instead set pre-existing enodes as le\n for node,id in self.memo.items():\n sig = self.get_variance(node.f, len(node.children))\n for c2 in itertools.product(*[self.expand_eclass(a, v.act(Mode.LE)) for a, v in zip(node.children, sig)]):\n id2 = self.memo.get(Node(node.f, c2))\n if id2 is not None:\n self.add_le(id, id2)\n def expand_eclass(self, a : Id, mode : Mode) -> set[Id]:\n a = self.find(a)\n if mode == Mode.LE:\n return self.all_le(a)\n elif mode == Mode.GE:\n return self.all_ge(a)\n else:\n return {a}\n def nodes_in_class(self, id: Id, mode : Mode) -> list[Node]:\n ids = self.expand_eclass(id, mode)\n return [obj for obj, obj_id in self.memo.items() if self.find(obj_id) in ids]\n def ematch_rec(self, id : Id, pat : Term, mode : Mode, subst) -> list[Subst]:\n # perhaps expand_eclass should be pulled up here.\n match pat:\n case Var(name): # should allow Var to expand_eclass? Probably. Ok.\n if name in subst:\n return [subst] if self.find(subst[name]) in self.expand_eclass(id, mode) else []\n else:\n return [{**subst, name: self.find(id)} for id in self.expand_eclass(id, mode)]\n case App(f, args):\n sig = self.get_variance(f, len(args))\n new_modes = [v.act(mode) for v in sig]\n results = []\n # In this style of doing it, the ONLY change to support refinement is the implementation of nodes_in_class\n for node in self.nodes_in_class(id, mode): # nodes_le_class(id) ?\n if node.f == f and len(node.children) == len(args):\n todo = [subst]\n for arg_pattern, arg_id, arg_mode in zip(args, node.children, new_modes):\n todo = [\n subst1\n for subst0 in todo\n for subst1 in self.ematch_rec(\n arg_id, arg_pattern, arg_mode, subst0\n )\n ]\n results.extend(todo)\n return results\n def extract(self, id : Id, mode : Mode) -> set[Id]:\n # Is this top down extraction busted? Is it actually ok to do the None trick or is it possible visitation order matters?\n memo = {}\n def worker(id: Id, mode : Mode) -> Term:\n id = self.find(id) # probably redundant\n key = (id, mode)\n if key in memo:\n return memo[key]\n else:\n memo[key] = None # mark as in progress to avoid infinite loops\n best_cost, best_term = float(\"inf\"), None\n for node in self.nodes_in_class(id, mode):\n variance = self.get_variance(node.f, len(node.children))\n\n args = tuple(worker(arg_id, v.act(mode)) for arg_id, v in zip(node.children, variance))\n if any(arg is None for arg in args):\n continue # subterm hit recursion, skip this node\n term = App(node.f, args)\n cost = term.size() + 1 # You don't want to be recursing down terms like this. Should also memoize cost.\n if cost < best_cost:\n best_cost, best_term = cost, term\n memo[key] = best_term\n return best_term\n return worker(id, mode)\n \n\n \n\n #def rebuild(self) -> None:\n #def ematch(self, mode : Mode): \n #def extract(self, mode : Mode): \n\nE = LE_EGraph()\na, b = E.add(\"a\"), E.add(\"b\")\nfa, fb = E.add(\"f\", a), E.add(\"f\", b)\nE.union(a, b)\nassert not E.is_eq(fa, fb)\nE.eq_cong_step()\nassert E.is_eq(a, b)\nassert E.is_eq(fa, fb)\n```\n\n```\nE = LE_EGraph()\nE.variance[\"f\"] = (Variance.MONO,)\na, b = E.add(\"a\"), E.add(\"b\")\nfa, fb = E.add(\"f\", a), E.add(\"f\", b)\nE.add_le(a, b)\nassert E.is_le(a, b)\nassert E.is_le(a, a)\nassert not E.is_le(b, a)\nE.le_cong_step()\nassert E.is_le(fa, fb)\n```\n\n```\nE = LE_EGraph()\nE.variance[\"diff\"] = (Variance.MONO,Variance.ANTI)\na, b,c,d = E.add(\"a\"), E.add(\"b\"), E.add(\"c\"), E.add(\"d\")\ndiff_ab = E.add(\"diff\", a, b)\nE.add_le(b, c)\nE.add_le(c, d)\n#E.le_cong_step()\n#E.ge_cong_step()\nE.ematch_rec(diff_ab, App(\"diff\", (Var(\"x\"), Var(\"y\"))), Mode.GE, {})\n```\n\n```\n[{'x': 0, 'y': 1}, {'x': 0, 'y': 2}, {'x': 0, 'y': 3}]\n```\n\n# Bits and Bobbles\n\nAll told, I find refinement a shockingly simple extension of the usual egraph concepts and implementation. But it has felt mysterious before so maybe that means I’ve just become incredibly wise?\n\nI think really the thing that makes it shockingly simple is just not believing there is any incredibly clever or nuanced way of doing it. I think the only way to do it is basically the obvious way.\n\nI think that maybe the generalization of all this is an egraph rewriting system that supports multiple relations and annotations of how they push through function symbols, akin to \n\nI remember being at a table at PLDI 2022 and Zach trying to convince / ask John Regehr what he wanted for e-graph to be compelling to him. He said refinement and as a treatment of arbitrary bitwidth bitvectors. These two have stuck with me as things to look for and this is the source of the refinement e-graph line of questioning.\n\nOther applications:\n\n* Logic. `->` as a less than relation\n* Relation algebra\n* Algebra of Programming bird and de Moor, Oliveira, Backhouse, Dijkstra \n* Subtyping\n* Query containment\n* First class lattice analyses\n\nI have debated rather than the mode + variance abstraction to allow specifying what expansion (EQ,GE,LE) you want in the language of the pattern. For example i could use `(foo ?a)`, `[foo ?a]`, `{foo ?a}` if I want to allow EQ, GE, LE respectively. This would allow fine grained ad hoc control of refinement e-matching in the pattern.\n\nAs Graham noted, the upper and lower sets of the Ids do fit operationally somewhat into the egg notion of Analyses. Generically, it makes perfect sense to have things keyed on `Id` that merge when `Id` merge. I am agnostic if that means such things must be Lattices (as many program analyses are), Semigroups (like eclass member counts) or something else. That the upper and lower sets themselves contain more Ids is fine but also defies a simple algebraic characterization of what is going on in my opinion.\n\nThere has been a similar debate if *equality* is “just a lattice of partitions”, trying to subsume the equality relation of the egraph into Lattices as the master concept. Didn’t seem to really work but operationally it kind of makes sense that equalities is implemented as a “merge action” very much akin to a lattice join at least operationally. There is spooky action at a distance through the union find though. Mutable references often enable some kind of spooky tunnelling phenomenon that break simple mathematical models (Oleg Kiselyov had some way of casting types through a ref cell tunnel too?)\n\n| | | |\n| --- | --- | --- |\n| Current mode | Arg polarity | |\n| = | \\_ | = |\n| <= | + | <= |\n| <= | = | = |\n| <= | - | >= |\n\nThe mode extraction kind of says what kind of pattern we are procssing `p <= t` `t <= p` or `t = p`. `Variance` is a property of function symbols that says what we can infer about pushing `<=` through `f`. This is used in the upward direction for refinement closure, but in the downward direction for breaking apart a pattern matching constraint/query into queries on the arguments `{f(?a, ?b) R f(x,y)} ===> {?a R x, ?b R y}`. `R` may be flipped, kept the same, or forced to be equality because `f` isn’t known to be sufficiently monotone. It is always sound to revert an inequality query `?p <= t` to equality `?p = t`.\n\nExtraction also comes in the same modes `t = ?extract` `t <= ?extract` `t >= ?extract`. Extraction is kind of similar to pattern matching in some respects\n\n`[[x]] = fun b => {b}` is the lifted identity function. `ite` is pointwise lifted. `[[dontcare]] = fun _ => {True, False}` `[[true]] = fun _ => {True}` `[[false]] = fun _ => {False}`. Refinement is interpreted as subrelation.\n\nI feel that for an abstract partial order relation, this is about as good as you’re going to do. I don’t think there is a some magic data structure that will make everything all better\n\nBut I do think there is the possibility to do better on two axes\n\n* Partial Orders with extra axioms. Total, linear, Tree-like orders may have more available \n* Proof relevancy. If you can say *the sense* that `r : a <= b` then you can do better. As an example, if you know `a <= b` in the integers, a proof object might be an `n >= 0` such that `a + n == b`. This can be implemented as an offset union find, which is much more efficient. There are other orders where the proof object can help that generalize this. Tree-like orders in particular are interesting in that the tree-like ness of the order can comply nicely with the tree-like ness of the union find forest.\n* Semantics. If we know we’re talking about the integers with `<=`, yeah there might be a bunch of ways of going aobut it. It’s total, yada yada, but we have a lot of games and data structures we can play on the integers. Side car linear programming solvers something something.\n\nA prototype of a refinement egraph based on Max Willsey’s microegg . A WASM demo is here \n\nRefinement e-graphs give you an uninterpreted `<=` that is about as baked in as `=` is.\n\nThis is useful perhaps because as the story goes, many rewrites in compilers are not unoriented equalities, they are oriented refinements.\n\n`<=` is baked in to be transitive, reflexive, and collapses cycles to `=`.\n\nPrevious discussions of mine on refinement e-graphs:\n\n* An Inequality Union Find Inspired by Atomic Asymmetric Completion\n* Inequality Union Finds: Baby Steps to Refinement E-graphs\n\nThe union find tracks upper and lower `<=` sets in a manner similar to an analysis (they are keyed on eclass and merge on union). Tentatively, storing this maximally sparsely rather than fully materializing (DFSing it on demand) as one would in egglog is more performant in memory and time. [Egglog](https://github.com/egraphs-good/egglog) itself is highly engineered though, so I don’t actually know how this shakes out.\n\nA nice example is “don’t care” in boolean circuits . Some inputs are not expected or allowed, so they optimizer is free to pick a behavior on those inputs that helps make a more optimal circuit.\n\nIn either case, I think baking in `<=` rather than having it as a mangled program or macro is conceptually cohesive and pleasant.\n\nNothing involving `<=` is quite as well behaved or as performant as `=`, but it is there as a light sprinkling on top. If *everything* you do is refinement rather than equality, I am not sure the refinement egraph offers much over a hash cons with a stored inequality table.\n\nE-matching, rebuilding, and extraction all have slight tweaks related to `<=`. Rebuilding performs refinement closure.\n\nFunction symbols can be given a variance signature, very similarly to variance of type parameters in subtyping. This is about whether they are monotone `a <= b -> f a <= f b`, anti-monotone `a <= b -> f a >= f b` or neither in particular arguments. This changes patterns and extraction “modes” appropriately as they go through the term.\n\nRefinement rebuilding / closure is no where near as nice as equality (although it is still conceptually simple). It is not obvious that it will terminate if one allows new enode creation, so in that sense it is in the same naughty category as rewrite rules. There is a distinction to be made between materializing and non-materializing refinement closure (only note inequalities between pre-exising enodes).\n\nYou do sometimes want to enumerate your upper or lower set of ids for refinement closure, and for e-matching modulo refinement and extraction modulo refinement.\n\nIt is my belief that a completely generic uninterpreted refinement relation can never be as good as an equality relation and that there probably isn’t an astonishingly good way of implementing such a thing. It will more or less correspond to depth first search enumerations +- some tweaks.\n\nNevertheless, I think it is both nontrivial, interesting, and possibly useful to bake in an inequality relation into the surface language and features.\n\nThe alternative is to macro encode an inequality into something like egglog. I kind of prefer direct operational interpretations than a macro expansion explanation.\n\nIn small micro benchmarks it does appear that maintaining the sparse representation of the inequality relation with on the fly closure is superior to materializing it ahead of time in memory and speed (memory often implies speed since cache whatevers are a dominant concern).\n\nBased on the results in it is my suspicion that ground refinement closure may be undecidable. In this case, full refinement closure should be treated at the same level of suspicion and incompleteness as rules are.\n\n\n\nHmm. Am i crazy? It would be nice is some enodes were subsumed by the inequality relation. But ematching can kind of traverse non materialized nodes? Is there some way we could subsume / del / dematerialize enodes such that ematching could still find them?\nSomething that is pinned between f0 <= f1 <= f2 maybe we could del f1? Asymmetric rewriting still has some deletion character to it.\nMaybe it oculd be the ematcher’s job to materialize stuff a la Max’s suggestion.\n\n# 4/2026\n\nIt’s kind of like knownbits. For BV1 it is all possible sets.\n\n```\nfrom kdrag.all import *\n\nnone = smt.K(smt.BoolSort(), False)\ntrue = smt.Store(none, True,True)\nfalse = smt.Store(none, True, False)\nany = smt.K(smt.BoolSort(), True)\n\ndef SetLift(f : FuncRef)\n ds = smt.domains(f)\n r = smt.range(f)\n def res(*args):\n x = smt.FreshConst(\"x\", smt.BoolSort())\n ps = [smt.FreshConst(\"p\", typ) for typ in ds]\n return smt.Lambda([x], smt.Exists(ps, x == args[0][p], x = f(p)))\n return res\n\ndef And(a, b):\n x = smt.FreshConst(\"x\", smt.BoolSort())\n p,q = smt.Consts(\"p q\", smt.BoolSort())\n return smt.Lambda([x], smt.Exists([p,q], a[p], b[q], x = smt.And(p,q)))\n\ndef Or(a, b): ...\ndef Implies()\n\nobool = kd.inductive(\"inductive obool where | none : obool | lit : Bool -> obool | any : obool\")\n\nobool.lit(True)\nx,y = smt.Consts(\"x y\", obool)\nkd.notation.and_.define([x,y], \n kd.cond(\n (smt.And(x == obool.none, y == obool.none), obool.none),\n ()\n )\n )\n\nrefines(a,b)\n```\n\nlit(True)\n\nGeorge example\n\nsimplify dontcare /\\ x\n\n0 /\\ x = 0 is eq\n\nSemantics is set of\n\nFor total orders there is are speical datastructure. What about one tjat effectively assigns “rationals”\nOr really we have a space with gaps and we incrementally grow the space when it gets too full, or redistrbute if it gets too cluttered in just one section.\n\nFor tree orders, maybe we really could maintain a union find?\n\nk-Width partial orders or approximation by a k-width order?\n\n\n\nUsing partial order special relation to get refinement egraphs.\nNeed to manually order close though.\n\n```\n\n```\n\n\n\npolar types in dolan. Maybe something like this restriction enables ground asym completion to terminate? Separate refinement closure into its polar and non polar components.\n\nlattice and ordered resolution\n respond here once I get it\n\nUnification and Knuth Bendix.\nI consider them to be opposites even if they can be encoded to each other.\nKB is forward reasoning\nunification is backward reasoning from a query or goal\n\nFor speed reasons maybe you’d want to have 3-tuple 4-tuples etc available. Lempel ziv something something? \nword equqation solving also had compression as an idea in there…\n\nstring rewriting is a suffiicnet framework to simplify atomic equational proofs. Maybe overly powerful?\n\nWhy can’t I binarize into a normal form\nweight by original size. Tie break\nabc = df\na b = e1\ne1 c = e2\n\nactual equations:\ne2 = e4\n\noverlaps\na b = e2\nb c = e5\n\na + b = e\\_+1\na *b = e\\_*7\nstructured eids tagged by function symbol and identifier\nOnline extraction?\nidenitfy a term with the eid at time of creation. You can on demand compare\n\n“enodes” + “union find”\nNontrivial enode overlap is impossible. simplification is possible.\nWeighted union find = weighted Atomic KBO\n\n```\nclass UF():\n weight : list[int]\n parents : list[int]\n def union():\n x,y = find(x), find(y)\n if weight[x] <= weight[y]:\n parents[x] = y\n else:\n parents[x]\n```\n\nFor AC enodes, we do need to perform overlap. Term ordering matters (?)\n(X + Y + Z) :- (X + Y), (Y + Z).\nOnline extraction - we do not need to keep anything that\n\nTeitze transformations \ntsetsin\nANF\ndefinitional exte4nsions\nBut would this be crazy for multiset, linear, grobner, etc?\nax + by = z1\nx + by = z1\nz1 = z2\n\nax + by = z1\nwhere a b are coprime\nax + by = z1\na z1 = b z2\n\nbinary form of egraph. Partial application. App form\n(f, x) = fx\n(fx, y) = fxy\n(fxy, z) = fxyz\nLFHOL term orderings. Cody had some spiel\n\nenodes need an overlap api. eids need online extraction / term orderings to figure out winners. Or just online extraction?\nBut why does ordering matter then if the term associated with eclass is fluid.\nf(x,y,z) -> e1 can spontaneously become unoriented in this perspective if x lowers a bunch\nextraction repair f(x,y,z) <- e1\n\nmemo : enode -> eclass\nparents : eclass -> eclass\nenodes : eclass -> Vec // vec?\nweights : eclass -> Int\n\nenodes kind of performs extraction\nIf there are two directions, that’s an overlap / confluence problem. Need to remove stuff from union find?\n\nConservative extension makes sense either in compression or expansive form (decoding). efresh -> term decoding vs term -> egraph compressive\n\nKnuth Bendix + definition extension / teitze, conservative extension\n\n```\nE, R, TermOrder\n--------------define\nE U {efresh = t}, R, TermOrder U {?}\n```\n\nWhy is a careful term ordering seemingly necessary for stuff besides union finds and straight egraphs?\n\nwell ordering surgery. Ordinals (total well orders) have an otion of algebra. They have a uniquer global minimum.\n\nAC egrapha = ground completion +\nmultiple ac symbols.\nACRPO - flatten + use multiset ? No but first we have to consider the exact structure we’ve been given\nRubio a fully syntactic acrpo\n ACKBO\n\nA \\/ C, rpo\n meseguer readonig course. Pretty interesting stuff in here.\n\n Set Theory and Algebra in Computer Science\nA Gentle Introduction to Mathematical Modeling\norder sorted algebras. hmm.\n Algebraic Semantics of Imperative Programs\n Formal Modeling and\nAnalysis of Distributed\nSystems in Maude\n\n\n\n Abstract canonical presentations\nproofs orderings. Good proofs.\n Completion Is an Instance of Abstract Canonical System Inference\n\n\n\n```\nimport maude\nmaude.init()\nnat = maude.getModule('NAT')\nt = nat.parseTerm('1 + 2')\nt.reduce()\nprint(t)\n```\n\n```\n3\n```\n\n```\nt = nat.parseTerm('1 + 2')\nt.symbol()\nlist(t.arguments())\n#maude.Symbol()\nnat.parseTerm(\"X + Y\")\n```\n\n```\n\u001b[31mWarning: \u001b[0m, line 0: bad token \u001b[35mX\u001b[0m.\n\u001b[31mWarning: \u001b[0m, line 0: no parse for term.\n```\n\n```\nmaude.getModules()\n```\n\n```\n(fmod BOOL,\n fmod TRUTH-VALUE,\n fmod BOOL-OPS,\n fmod TRUTH,\n fmod EXT-BOOL,\n fmod INITIAL-EQUALITY-PREDICATE,\n fmod NAT,\n fmod INT,\n fmod RAT,\n fmod FLOAT,\n fmod STRING,\n fmod CONVERSION,\n fmod RANDOM,\n fmod BOUND,\n fmod QID,\n fth TRIV,\n fth STRICT-WEAK-ORDER,\n fth STRICT-TOTAL-ORDER,\n fth TOTAL-PREORDER,\n fth TOTAL-ORDER,\n fth DEFAULT,\n fmod LIST,\n fmod WEAKLY-SORTABLE-LIST,\n fmod SORTABLE-LIST,\n fmod WEAKLY-SORTABLE-LIST',\n fmod SORTABLE-LIST',\n fmod SET,\n fmod LIST-AND-SET,\n fmod SORTABLE-LIST-AND-SET,\n fmod SORTABLE-LIST-AND-SET',\n fmod LIST*,\n fmod SET*,\n fmod MAP,\n fmod ARRAY,\n fmod STRING-OPS,\n fmod NAT-LIST,\n fmod QID-LIST,\n fmod QID-SET,\n fmod META-TERM,\n fmod META-CONDITION,\n fmod META-STRATEGY,\n fmod META-MODULE,\n fmod META-VIEW,\n fmod META-LEVEL,\n fmod LEXICAL,\n mod COUNTER,\n mod LOOP-MODE,\n mod CONFIGURATION)\n```\n\n```\nimport maude\nmaude.init()\n#nat = maude.getModule('NAT')\n#list(nat.getSymbols())\n#maude.input(\"load Nat .\")\n#maude.input(\"vars X Y : Nat .\")\nmod = maude.getCurrentModule()\nlist(mod.getSymbols())\nlist(mod.getSorts())\n\nmaude.input(\"\"\"\nfmod SIMPLE-NAT is \n sort Nat . \n op zero : -> Nat . \n op s_ : Nat -> Nat . \n op _+_ : Nat Nat -> Nat . \n vars N M : Nat . \n eq zero + N = N . \n eq s N + M = s (N + M) . \n endfm\n\"\"\")\nsn = maude.getModule(\"SIMPLE-NAT\")\nsn.parseTerm(\"s s N\")\n\nfrom dataclasses import dataclass, field\ntype Sort = str\n@dataclass\nclass ModuleBuilder():\n name : str\n sorts : set[Sort] = field(default_factory=set)\n vars : dict[str, Sort] = field(default_factory=dict)\n ops : dict[str, tuple[list[Sort], Sort]] = field(default_factory=dict)\n extras : list[str] = field(default_factory=list)\n def build(self) -> str:\n maude.input(str(self))\n return maude.getModule(self.name)\n def add_sort(self, sort: smt.SortRef):\n self.sorts.add(sort.name())\n def add_decl(self, decl: smt.FuncDeclRef):\n\n def __str__(self):\n lines = [f\"fmod {self.name} is\"]\n for s in self.sorts:\n lines.append(f\" sort {s} .\")\n for v, s in self.vars.items():\n lines.append(f\" var {v} : {s} .\")\n for op, (arg_sorts, ret_sort) in self.ops.items():\n arg_str = ' '.join(arg_sorts)\n lines.append(f\" op {op} : {arg_str} -> {ret_sort} .\")\n lines.extend(self.extras)\n lines.append(\"endfm\")\n return '\\n'.join(lines)\n\nModuleBuilder()\n```\n\n```\n\u001b[32mAdvisory: \u001b[0mredefining module \u001b[35mSIMPLE-NAT\u001b[0m.\n```\n\n```\nmaude.__file__\n```\n\n```\n'/home/philip/philzook58.github.io/.venv/lib/python3.12/site-packages/maude/__init__.py'\n```\n\n```\nnat\n```\n\n```\nNAT\n```\n\n```\nmaude.getModule(\"SMT\")\n```\n\n```\nclass StringKB():\n memo : dict[object,int]\n compress : dict[[tuple[int,int], int]]\n # repeat : dict[tuple[EId, int], EId]\n uf : list[int]\n def makeset(self):\n self.uf.append(len(self.uf))\n return len(self.uf) - 1\n def memo_obj(self, x):\n if x in self.memo:\n return self.memo[x]\n else:\n i = self.makeset()\n self.memo[x] = i\n return i\n def add_str(self, xs):\n xs = map(self.memo_obj, xs)\n for i in range(len(xs) - 1):\n a,b = xs[i], xs[i+1]\n if (a,b) in self.compress:\n c = self.compress[(a,b)]\n else:\n c = self.makeset()\n self.compress[(a,b)] = c\n def union(self, a, b):\n ra = self.find(a)\n rb = self.find(b)\n if ra != rb:\n self.uf[ra] = rb\n def rebuild(self):\n for (a,b), c in self.compress.items(): # overlap\n for (d,e), f in self.compress.items():\n if self.find(b) == self.find(d):\n ce, af = self.pair(c,e), self.pair(a,f)\n self.union(ce, af)\n for (a,b), c in self.compress.items(): # congruence\n ra, rb, rc = self.find(a), self.find(b), self.find(c)\n self.union(self.pair(ra,rb), rc)\n```\n\n```\ndef reclen(t1):\n if isinstance(t1, tuple):\n return 1 + sum(map(reclen, t1))\n else:\n return 1\n\nreclen((((1,2),3)))\n```\n\n```\n5\n```\n\n```\ndef lt_kbo(t1, t2):\n # ground kbo is size + tie breaking\n if t1 == t2:\n return False\n elif isinstance(t1, tuple) and isinstance(t2, tuple):\n l1, l2 = reclen(t1), reclen(t2)\n if l1 < l2:\n return True\n elif l1 > l2:\n return False\n else:\n for a,b in zip(t1,t2):\n if a == b:\n continue\n else:\n return lt_kbo(a,b)\n elif not isinstance(t1, tuple) and not isinstance(t2, tuple):\n return t1 < t2\n elif not isinstance(t1, tuple) and isinstance(t2, tuple):\n return True\n else:\n return False\n\nlt_kbo((1,2),(1,3))\nlt_kbo((1,2),(1,2,3))\nlt_kbo((1,2,3),(1,2))\n```\n\n```\nFalse\n```\n\na lambda egraph. (but only alpha)\nWhy not?\n\ndid I ever do a KB egraph?\n\n```\ndef replace(t, lhs, rhs):\n if t == lhs:\n return rhs\n elif isinstance(t, tuple):\n return tuple(lambda x: replace(x, lhs, rhs) for x in t)\n else:\n return t\n```\n\n```\nclass EGraph():\n rules : dict\n\n def union(self, t1, t2):\n t1,t2 = self.canon(t1), self.canon(t2)\n def find(self, t): ...\n def rebuild(self, t):\n foself.rules.keys():\n```\n\n```\ndef lt_kbo(t1, t2):\n # ground kbo is size + tie breaking\n if reclen(t1) < reclen(t2):\n return True\n else:\n \ndef rw(t, lhs, rhs):\n if t == lhs:\n return rhs\n elif isinstance(t, tuple):\n return tuple(map(rw(lhs,rhs), t))\n else:\n return t\n\nclass AsymComplete():\n```\n","body_html":"

Refinement E-Graphs

\n

Oct 4, 2026

\n

The idea of a refinement e-graph is to add a baked in a <= relation that is about as privileged as the e-graph’s native =

\n

There is a story that compiler rewrites are often not bidirectional equalities, but instead are unidirectional refinement rewrites, moving from an abstract or floppy program / spec to a more completely determined one that can run on a concrete machine. It is quite common for the source language to be cagey about the exact order the children of an expression are evaluated, or what is the result of an integer overflow or division by zero. Being cagey may enable more optimization opportunities or ease translation to disparate machines. It is also just a fact of life for these languages.

\n

Here is a prototype https://github.com/philzook58/refinement-microegg of a refinement egraph based on Max Willsey’s microegg https://github.com/mwillsey/microegg. A WASM demo is here https://www.philipzucker.com/refinement-microegg. Third verse same as the second

\n

Example: Don’t Care Circuits

\n

A nice example is “Don’t Care” in digital circuits https://en.wikipedia.org/wiki/Don%27t-care_term , You may say that certain inputs are not supported to a circuit and that the result is a don’t care in that case. An optimizer is free to pick a result that allows for the most optimal circuit. I believe George Constantinides explained a version of this example to me.

\n
%%file /tmp/circuit.sexp\n(fun ite (+ + +)) ; declare if-then-else as covariant in all arguments\n(rewrite (ite ?x true false) ?x)  ; ordinary equality rewrite\n(ge dontcare true)    ; dontcare refines to true. {True, False} >= {True}\n(ge dontcare false)   ; dontcare also refines to false. {True, False} >= {False}\n\n(insert (ite x true dontcare)) ; insert starting term\n(run 5 :expand-le)\n\n(extract-le (ite x true dontcare))  ; can extract x because refining this dontcare to true enables a nice term
\n
Writing /tmp/circuit.sexp
\n
! refinement-microegg /tmp/circuit.sexp
\n
x
\n

There are also refinement rewrite rules available in the implementation, rewrite-le and rewrite-ge.

\n

Spiritually, (rewrite-le lhs rhs) represents the formula forall ?a, lhs(?a) <= rhs(?a). Because of the form of this formula, we don’t have to match lhs on the equality nose. We can find a substitution for any starting ?t <= subst(lhs[?a]) to chain to a discovered inequality assertion ?t <= subst(lhs[?a]) <= subst(rhs[?a]).

\n

Don’t Care Semantics

\n

I think semantics is really important and don’t like meaningless syntax manipulation. The intended semantics of this “Don’t Care” example is Bool -> Set Bool with <= representing pointwise set containment.

\n
TermSemantics
xfun b => {b}
ite(c,t,e)fun b => {res for c1 in [[c]] b for res in (if c1 then [[t]] b else [[e]] b)}
dontcarefun _ => {True, False}
truefun _ => {True}
falsefun _ => {False}
t <= sforall b : Bool, is_subset ([[t]] b) ([[s]] b)
\n

x could be generalized to have an algebra of more than one dimension, which would bring us back to lifting e-graphs https://www.philipzucker.com/lambda_miller_egg/ https://www.youtube.com/watch?v=h1CzZguA6DE . Refinement and Lambda afaik are orthogonal features that have no issue being bolted together. Maybe something interesting might occur in extraction (some related terms may not exist in some contexts)?

\n

Note that this inequality assertion is distinct from equating dontcare = true = false. This of course is problematic. But it is also distinct from equating to either of them dontcare = true or dontcare = false. If we did one of these, then all dontcare everywhere would be forced to be true or false, whereas we want the ability to be able to make independent choices at all usages.\nOne could perhaps make dontcare1 dontcare2 dontcare3 etc as fresh constants and then independently equate them. This freshness game always feels like some goofy shell game to me though.\nThere is some intuitive sense that equating an eclass destroys it as a resource, but stating an inequality does not destroy it as a resource.

\n

Inequality Union Finds

\n

Roughly E-Graph = Union Find + Hash Cons. So a Refinement E-graph = inequality union find + hash cons.

\n

The interface of the inequality union find is more important than the details of the implementation.

\n
from typing import Protocol\ntype Id = int\nclass LE_UnionFind(Protocol):\n    # regular union find\n    def union(self, a : Id, b : Id) -> None: ...\n    def is_eq(self, a : Id, b : Id) -> bool: ...\n    def find(self, a : Id) -> Id: ...\n\n    # extra inequality features\n    def add_le(self, a : Id, b : Id) -> None: ... # the analog of union. union = add_eq\n    def is_le(self, a : Id, b : Id) -> bool: ...# analog of is_eq\n    def all_le(self, a : Id) -> set[Id]: ... # returns all elements `a` is known less than or equal to. Analog of find.\n    def all_ge(self, a : Id) -> set[Id]: ... # returns all elements known `a` is known greater than or equal to. Analog of find.
\n

Previous discussions of mine on inequality union finds towards refinement e-graphs:

\n\n

What Does A Refinement E-Graph Need on Top of This?

\n

An (inequality) union find deals in atomic symbols e4 and atomic equations e5 = e87 (or inequations e4 <= e65).

\n

An e-graph adds function symbols f(e4,e4) to this. These symbols appear in the following processes:

\n
  • Refinement-closure
  • Refinement E-matching
  • Refinement extraction
\n

The e-graph implementation need to be told how the function symbols play with the inequality <= by the user. Functions always respect equality =, but they may be monotone, anti-monotone or neither/unknown in their individual arguments. I like set difference diff(A,B) as an example of this. It is monotone in the first argument but anti-monotone/contravariant in the second argument diff(+,-).

\n

Refinement Closure

\n

Instead of congruence closure, we can perform refinement closure. This basically is applying a theorems like forall a b c d, a <= b /\\ c >= d -> diff(a,c) <= diff(b,d) instead of a = b /\\ c = d -> diff(a,c) = diff(b, d) which is what congruence closure applies.

\n

Refinement closure isn’t as nice as congruence closure. We can use it both in the form that makes new enodes or the form that only notes relations between pre-existing enodes. In a datalog sense, this is the difference between\ndiff(a,c) <= diff(b,d) :- a <= b, c >= d, diff(a,c) and the guarded version diff(a,c) <= diff(b,d) :- a <= b, c >= d, diff(a,c), diff(b,d). The first can be useful, but it can also be explosive.

\n

Refinement E-matching

\n

Pattern matching can be modelled as a processing a constraint set {?p = t} (see for example section 2.2.3 of https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf or section 4.6 of Term Rewriting and All That ). What makes it pattern matching vs unification is having variable only on one side, which is sometimes easier/more efficient to implement.

\n
\"unification
\n

For refinement e-matching, We can be working with a constraint {?p <= t} or {t <= ?p}. But otherwise really the algorithm doesn’t change that much. You just need to track which “mode” you’re currently in, and change the mode according to the variance of the function symbols.

\n

For example, this diff pattern processes by flipping one of the modes.{diff(?a, ?b) <= diff(x,y)} ===> {?a <= x, ?b >= y}

\n

In the implementation, there is one extra degree of nondeterminism on top of the usual e-matching eclass->enode nondeterminsm, where in the GE or LE mode, you may traverse an eclass -> eclass <= edge.

\n

From the flattened relational e-matching perspective, this is the insertion of implicit (le ?a ?b) all throughout the pattern. For example the patternfoo(bar(?x)) becomes flattened to ?e1 = foo(?e2), ?e2 <= ?e3, ?e3 = bar(?e4), ?e4 <= ?x. <= kind of “mediates” between every function symbol relation.

\n

Refinement Extraction

\n

Regular extraction is actually pretty similar to e-matching in many ways. We are seeking a ?extract = t but we want the “best” ?extract. We have a tendency to implement extraction bottom up instead of top down.

\n

In refinement extraction, we can instead be asking for ?extract <= t or ?extract >= t. We might also want to use <= in our definition of “best”. Perhaps we want the most refined (which semantically might mean the most concretely implemented or most deterministic entity) and then tie break with smallest size term or vice versa.

\n

A Toy Python Implementation of a Refinement E-Graph

\n

This is basically a copy of my python microegg with some inequality smarts put in. There is a refinement closure step le_cong_step and le_cong_step_weak (which makes no new enodes). Because e-matching can traverse <= edges, you might need less materialization than you’d think.

\n

ematching and extraction are keyed on Mode which says whether you are allowed to search up or down the <= or have to use on the nose =.

\n

The variance table variance : dict[str, tuple[Variance, ...]] says the variance of each argument of the function symbol. It is kind of the same shape of data one might use for storying types of the symbols, but this implementation is untyped.

\n
from dataclasses import dataclass, field\nfrom enum import Enum\nfrom collections import defaultdict\nimport itertools\ntype Id = int\n@dataclass(frozen=True)\nclass Node:\n    f : str\n    children : tuple[Id,...]\n\nclass Mode(Enum): # Expand all below, all above, or equal only. Ematch, extract, and rebuild can all be keyed on this kind of\n    LE = -1\n    EQ = 0\n    GE = 1\n\nclass Variance(Enum): # Slash Monotonicity\n    MONO = 1    # covariant\n    ANTI = -1   # contravariant\n    UNKNOWN = 0 # "invariant"\n    #COVARIANT = 1   # monotone\n    #CONTRAVARIANT = -1 # antitone\n    #INVARIANT = 0   # neither monotone nor antitone\n    def act(self, mode: Mode) -> Mode:\n        match self:\n            case Variance.MONO:\n                return mode\n            case Variance.ANTI:\n                return Mode(-mode.value)\n            case Variance.UNKNOWN:\n                return Mode.EQ\n\nclass Term: ...\n@dataclass\nclass App(Term):\n    f : str\n    children : tuple[Term,...]\n    def size(self) -> int: # used in extraction\n        return 1 + sum(child.size() for child in self.children)\n@dataclass \nclass Var(Term):\n    name : str\n\ntype Subst = dict[str, Id]\n\n@dataclass\nclass LE_EGraph():\n    parents : list[Id] = field(default_factory=list)\n    memo : dict[Node, Id] = field(default_factory=dict)\n    uppers : list[set[Id]] = field(default_factory=list)\n    lowers : list[set[Id]] = field(default_factory=list)\n    variance : dict[str, tuple[Variance, ...]] = field(default_factory=dict)\n\n    def get_variance(self, f: str, arity: int) -> tuple[Variance, ...]:\n        sig = self.variance.get(f, (Variance.UNKNOWN,) * arity)\n        assert len(sig) == arity\n        return sig\n\n    def find(self, a : Id) -> Id:\n        while self.parents[a] != a:\n            a = self.parents[a]\n        return a\n    def union(self, a : Id, b : Id) -> None:\n        a,b = self.find(a), self.find(b)\n        if a == b:\n            return\n        self.parents[b] = a\n        self.uppers[a] |= self.uppers[b]\n        self.lowers[a] |= self.lowers[b]\n    def add(self, f, *args : Id) -> Id:\n        args = tuple(self.find(a) for a in args)\n        node = Node(f, args)\n        if node in self.memo:\n            return self.find(self.memo[node])\n        new_id = len(self.parents)\n        self.parents.append(new_id)\n        self.uppers.append(set())\n        self.lowers.append(set())\n        self.memo[node] = new_id\n        return new_id\n    def is_eq(self, a : Id, b : Id) -> bool:\n        return self.find(a) == self.find(b)\n    def all_le(self, a : Id) -> set[Id]:\n        a = self.find(a)\n        u = {self.find(x) for x in self.uppers[a]}\n        u.add(a) # reflexive\n        todo = list(u)\n        while todo:\n            x = self.find(todo.pop())\n            for y in self.uppers[x]:\n                y = self.find(y)\n                if y not in u:\n                    u.add(y)\n                    todo.append(y)\n        return u\n    def all_ge(self, a : Id) -> set[Id]:\n        a = self.find(a)\n        l = {self.find(x) for x in self.lowers[a]}\n        l.add(a) # reflexive\n        todo = list(l)\n        while todo:\n            x = self.find(todo.pop())\n            for y in self.lowers[x]:\n                y = self.find(y)\n                if y not in l:\n                    l.add(y)\n                    todo.append(y)\n        return l\n    def add_le(self, a : Id, b : Id) -> None:\n        a,b = self.find(a), self.find(b)\n        if a == b:\n            return\n        self.uppers[a].add(b) # could not do so if already found. Help keep uppers sparse\n        self.lowers[b].add(a)\n    def is_le(self, a : Id, b : Id) -> bool:\n        return self.find(b) in self.all_le(a) # We don't have to collect up all_le to compute this but this is easy\n    #def cong_step(self, mode : Mode): ...\n    # rebuild is applying eq_cong_step in a loop\n    def eq_cong_step(self):\n        for node, id in list(self.memo.items()):\n            children1 = [self.find(a) for a in node.children]\n            if children1 == list(node.children):\n                continue\n            else:\n                del self.memo[node] # It is important for e-matching to remove stale nodes.\n                id1 = self.add(node.f, *children1)\n                self.union(id, id1) # could pollute union find less by giving a variant of self.add id\n    def le_cong_step(self):\n        for node, id in list(self.memo.items()):\n            children = [self.find(a) for a in node.children]\n            id1 = self.add(node.f, *children)\n            sig = self.get_variance(node.f, len(node.children))\n            for c2 in itertools.product(*[self.expand_eclass(a, v.act(Mode.LE)) for a, v in zip(node.children, sig)]):\n                id2 = self.add(node.f, *c2)\n                self.add_le(id, id2)\n        # It is not obvious that le cong should something stale. It probably shouldn't\n    def ge_cong_step(self):\n        # Just the opposite directin of le_cong_step\n        for node, id in list(self.memo.items()):\n            children = [self.find(a) for a in node.children]\n            id1 = self.add(node.f, *children)\n            sig = self.get_variance(node.f, len(node.children))\n            for c2 in itertools.product(*[self.expand_eclass(a, v.act(Mode.GE)) for a, v in zip(node.children, sig)]):\n                id2 = self.add(node.f, *c2)\n                self.add_le(id2, id)\n    def le_cong_weak(self): \n        # Don't make new enodes. But instead set pre-existing enodes as le\n        for node,id in self.memo.items():\n            sig = self.get_variance(node.f, len(node.children))\n            for c2 in itertools.product(*[self.expand_eclass(a, v.act(Mode.LE)) for a, v in zip(node.children, sig)]):\n                id2 = self.memo.get(Node(node.f, c2))\n                if id2 is not None:\n                    self.add_le(id, id2)\n    def expand_eclass(self, a : Id, mode : Mode) -> set[Id]:\n        a = self.find(a)\n        if mode == Mode.LE:\n            return self.all_le(a)\n        elif mode == Mode.GE:\n            return self.all_ge(a)\n        else:\n            return {a}\n    def nodes_in_class(self, id: Id, mode : Mode) -> list[Node]:\n        ids = self.expand_eclass(id, mode)\n        return [obj for obj, obj_id in self.memo.items() if self.find(obj_id) in ids]\n    def ematch_rec(self, id : Id, pat : Term, mode : Mode, subst) -> list[Subst]:\n        # perhaps expand_eclass should be pulled up here.\n        match pat:\n            case Var(name): # should allow Var to expand_eclass? Probably. Ok.\n                if name in subst:\n                    return [subst] if self.find(subst[name]) in self.expand_eclass(id, mode) else []\n                else:\n                    return [{**subst, name: self.find(id)} for id in self.expand_eclass(id, mode)]\n            case App(f, args):\n                sig = self.get_variance(f, len(args))\n                new_modes = [v.act(mode) for v in sig]\n                results = []\n                # In this style of doing it, the ONLY change to support refinement is the implementation of nodes_in_class\n                for node in self.nodes_in_class(id, mode): # nodes_le_class(id) ?\n                    if node.f == f and len(node.children) == len(args):\n                        todo = [subst]\n                        for arg_pattern, arg_id, arg_mode in zip(args, node.children, new_modes):\n                            todo = [\n                                subst1\n                                for subst0 in todo\n                                for subst1 in self.ematch_rec(\n                                    arg_id, arg_pattern, arg_mode, subst0\n                                )\n                            ]\n                        results.extend(todo)\n                return results\n    def extract(self, id : Id, mode : Mode) -> set[Id]:\n        # Is this top down extraction busted? Is it actually ok to do the None trick or is it possible visitation order matters?\n        memo = {}\n        def worker(id: Id, mode : Mode) -> Term:\n            id = self.find(id)  # probably redundant\n            key = (id, mode)\n            if key in memo:\n                return memo[key]\n            else:\n                memo[key] = None  # mark as in progress to avoid infinite loops\n                best_cost, best_term = float("inf"), None\n                for node in self.nodes_in_class(id, mode):\n                    variance = self.get_variance(node.f, len(node.children))\n\n                    args = tuple(worker(arg_id, v.act(mode)) for arg_id, v in zip(node.children, variance))\n                    if any(arg is None for arg in args):\n                        continue  # subterm hit recursion, skip this node\n                    term = App(node.f, args)\n                    cost = term.size() + 1 # You don't want to be recursing down terms like this. Should also memoize cost.\n                    if cost < best_cost:\n                        best_cost, best_term = cost, term\n                memo[key] = best_term\n                return best_term\n        return worker(id, mode)\n                \n\n        \n\n    #def rebuild(self) -> None:\n    #def ematch(self, mode : Mode): \n    #def extract(self, mode : Mode): \n\nE = LE_EGraph()\na, b = E.add("a"), E.add("b")\nfa, fb = E.add("f", a), E.add("f", b)\nE.union(a, b)\nassert not E.is_eq(fa, fb)\nE.eq_cong_step()\nassert E.is_eq(a, b)\nassert E.is_eq(fa, fb)
\n
E = LE_EGraph()\nE.variance["f"] = (Variance.MONO,)\na, b = E.add("a"), E.add("b")\nfa, fb = E.add("f", a), E.add("f", b)\nE.add_le(a, b)\nassert E.is_le(a, b)\nassert E.is_le(a, a)\nassert not E.is_le(b, a)\nE.le_cong_step()\nassert E.is_le(fa, fb)
\n
E = LE_EGraph()\nE.variance["diff"] = (Variance.MONO,Variance.ANTI)\na, b,c,d = E.add("a"), E.add("b"), E.add("c"), E.add("d")\ndiff_ab = E.add("diff", a, b)\nE.add_le(b, c)\nE.add_le(c, d)\n#E.le_cong_step()\n#E.ge_cong_step()\nE.ematch_rec(diff_ab, App("diff", (Var("x"), Var("y"))), Mode.GE, {})
\n
[{'x': 0, 'y': 1}, {'x': 0, 'y': 2}, {'x': 0, 'y': 3}]
\n

Bits and Bobbles

\n

All told, I find refinement a shockingly simple extension of the usual egraph concepts and implementation. But it has felt mysterious before so maybe that means I’ve just become incredibly wise?

\n

I think really the thing that makes it shockingly simple is just not believing there is any incredibly clever or nuanced way of doing it. I think the only way to do it is basically the obvious way.

\n

I think that maybe the generalization of all this is an egraph rewriting system that supports multiple relations and annotations of how they push through function symbols, akin to https://rocq-prover.org/doc/V9.2.0/refman/addendum/generalized-rewriting.html

\n

I remember being at a table at PLDI 2022 and Zach trying to convince / ask John Regehr what he wanted for e-graph to be compelling to him. He said refinement and as a treatment of arbitrary bitwidth bitvectors. These two have stuck with me as things to look for and this is the source of the refinement e-graph line of questioning.

\n

Other applications:

\n\n

I have debated rather than the mode + variance abstraction to allow specifying what expansion (EQ,GE,LE) you want in the language of the pattern. For example i could use (foo ?a), [foo ?a], {foo ?a} if I want to allow EQ, GE, LE respectively. This would allow fine grained ad hoc control of refinement e-matching in the pattern.

\n

As Graham noted, the upper and lower sets of the Ids do fit operationally somewhat into the egg notion of Analyses. Generically, it makes perfect sense to have things keyed on Id that merge when Id merge. I am agnostic if that means such things must be Lattices (as many program analyses are), Semigroups (like eclass member counts) or something else. That the upper and lower sets themselves contain more Ids is fine but also defies a simple algebraic characterization of what is going on in my opinion.

\n

There has been a similar debate if equality is “just a lattice of partitions”, trying to subsume the equality relation of the egraph into Lattices as the master concept. Didn’t seem to really work but operationally it kind of makes sense that equalities is implemented as a “merge action” very much akin to a lattice join at least operationally. There is spooky action at a distance through the union find though. Mutable references often enable some kind of spooky tunnelling phenomenon that break simple mathematical models https://counterexamples.org/polymorphic-references.html https://en.wikipedia.org/wiki/Value_restriction (Oleg Kiselyov had some way of casting types through a ref cell tunnel too?)

\n
Current modeArg polarity
=_=
<=+<=
<===
<=->=
\n

The mode extraction kind of says what kind of pattern we are procssing p <= t t <= p or t = p. Variance is a property of function symbols that says what we can infer about pushing <= through f. This is used in the upward direction for refinement closure, but in the downward direction for breaking apart a pattern matching constraint/query into queries on the arguments {f(?a, ?b) R f(x,y)} ===> {?a R x, ?b R y}. R may be flipped, kept the same, or forced to be equality because f isn’t known to be sufficiently monotone. It is always sound to revert an inequality query ?p <= t to equality ?p = t.

\n

Extraction also comes in the same modes t = ?extract t <= ?extract t >= ?extract. Extraction is kind of similar to pattern matching in some respects

\n

[[x]] = fun b => {b} is the lifted identity function. ite is pointwise lifted. [[dontcare]] = fun _ => {True, False} [[true]] = fun _ => {True} [[false]] = fun _ => {False}. Refinement is interpreted as subrelation.

\n

I feel that for an abstract partial order relation, this is about as good as you’re going to do. I don’t think there is a some magic data structure that will make everything all better

\n

But I do think there is the possibility to do better on two axes

\n
  • Partial Orders with extra axioms. Total, linear, Tree-like orders may have more available https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/
  • Proof relevancy. If you can say the sense that r : a <= b then you can do better. As an example, if you know a <= b in the integers, a proof object might be an n >= 0 such that a + n == b. This can be implemented as an offset union find, which is much more efficient. There are other orders where the proof object can help that generalize this. Tree-like orders in particular are interesting in that the tree-like ness of the order can comply nicely with the tree-like ness of the union find forest.
  • Semantics. If we know we’re talking about the integers with <=, yeah there might be a bunch of ways of going aobut it. It’s total, yada yada, but we have a lot of games and data structures we can play on the integers. Side car linear programming solvers something something.
\n

A prototype of a refinement egraph based on Max Willsey’s microegg https://github.com/mwillsey/microegg. A WASM demo is here https://www.philipzucker.com/refinement-microegg

\n

Refinement e-graphs give you an uninterpreted <= that is about as baked in as = is.

\n

This is useful perhaps because as the story goes, many rewrites in compilers are not unoriented equalities, they are oriented refinements.

\n

<= is baked in to be transitive, reflexive, and collapses cycles to =.

\n

Previous discussions of mine on refinement e-graphs:

\n\n

The union find tracks upper and lower <= sets in a manner similar to an analysis (they are keyed on eclass and merge on union). Tentatively, storing this maximally sparsely rather than fully materializing (DFSing it on demand) as one would in egglog is more performant in memory and time. Egglog itself is highly engineered though, so I don’t actually know how this shakes out.

\n

A nice example is “don’t care” in boolean circuits . Some inputs are not expected or allowed, so they optimizer is free to pick a behavior on those inputs that helps make a more optimal circuit.

\n

In either case, I think baking in <= rather than having it as a mangled program or macro is conceptually cohesive and pleasant.

\n

Nothing involving <= is quite as well behaved or as performant as =, but it is there as a light sprinkling on top. If everything you do is refinement rather than equality, I am not sure the refinement egraph offers much over a hash cons with a stored inequality table.

\n

E-matching, rebuilding, and extraction all have slight tweaks related to <=. Rebuilding performs refinement closure.

\n

Function symbols can be given a variance signature, very similarly to variance of type parameters in subtyping. This is about whether they are monotone a <= b -> f a <= f b, anti-monotone a <= b -> f a >= f b or neither in particular arguments. This changes patterns and extraction “modes” appropriately as they go through the term.

\n

Refinement rebuilding / closure is no where near as nice as equality (although it is still conceptually simple). It is not obvious that it will terminate if one allows new enode creation, so in that sense it is in the same naughty category as rewrite rules. There is a distinction to be made between materializing and non-materializing refinement closure (only note inequalities between pre-exising enodes).

\n

You do sometimes want to enumerate your upper or lower set of ids for refinement closure, and for e-matching modulo refinement and extraction modulo refinement.

\n

It is my belief that a completely generic uninterpreted refinement relation can never be as good as an equality relation and that there probably isn’t an astonishingly good way of implementing such a thing. It will more or less correspond to depth first search enumerations +- some tweaks.

\n

Nevertheless, I think it is both nontrivial, interesting, and possibly useful to bake in an inequality relation into the surface language and features.

\n

The alternative is to macro encode an inequality into something like egglog. I kind of prefer direct operational interpretations than a macro expansion explanation.

\n

In small micro benchmarks it does appear that maintaining the sparse representation of the inequality relation with on the fly closure is superior to materializing it ahead of time in memory and speed (memory often implies speed since cache whatevers are a dominant concern).

\n

Based on the results in https://www.sciencedirect.com/science/article/pii/S1571066104002968 it is my suspicion that ground refinement closure may be undecidable. In this case, full refinement closure should be treated at the same level of suspicion and incompleteness as rules are.

\n

https://www.philipzucker.com/asymmetric_complete/

\n

Hmm. Am i crazy? It would be nice is some enodes were subsumed by the inequality relation. But ematching can kind of traverse non materialized nodes? Is there some way we could subsume / del / dematerialize enodes such that ematching could still find them?\nSomething that is pinned between f0 <= f1 <= f2 maybe we could del f1? Asymmetric rewriting still has some deletion character to it.\nMaybe it oculd be the ematcher’s job to materialize stuff a la Max’s suggestion.

\n

4/2026

\n

It’s kind of like knownbits. For BV1 it is all possible sets.

\n
from kdrag.all import *\n\nnone = smt.K(smt.BoolSort(), False)\ntrue = smt.Store(none, True,True)\nfalse = smt.Store(none, True, False)\nany = smt.K(smt.BoolSort(), True)\n\ndef SetLift(f : FuncRef)\n    ds = smt.domains(f)\n    r = smt.range(f)\n    def res(*args):\n        x = smt.FreshConst("x", smt.BoolSort())\n        ps = [smt.FreshConst("p", typ) for typ in ds]\n        return smt.Lambda([x], smt.Exists(ps, x == args[0][p], x = f(p)))\n    return res\n\ndef And(a, b):\n    x = smt.FreshConst("x", smt.BoolSort())\n    p,q = smt.Consts("p q", smt.BoolSort())\n    return smt.Lambda([x], smt.Exists([p,q], a[p], b[q], x = smt.And(p,q)))\n\ndef Or(a, b): ...\ndef Implies()\n\nobool = kd.inductive("inductive obool where | none : obool | lit : Bool -> obool | any : obool")\n\nobool.lit(True)\nx,y = smt.Consts("x y", obool)\nkd.notation.and_.define([x,y], \n                        kd.cond(\n                            (smt.And(x == obool.none, y == obool.none), obool.none),\n                            ()\n                        )\n                        )\n\nrefines(a,b)
\n

lit(True)

\n

George example

\n

simplify dontcare /\\ x

\n

0 /\\ x = 0 is eq

\n

Semantics is set of

\n

For total orders there is are speical datastructure. What about one tjat effectively assigns “rationals”\nOr really we have a space with gaps and we incrementally grow the space when it gets too full, or redistrbute if it gets too cluttered in just one section.

\n

For tree orders, maybe we really could maintain a union find?

\n

k-Width partial orders or approximation by a k-width order?

\n

https://microsoft.github.io/z3guide/docs/theories/Special%20Relations/

\n

Using partial order special relation to get refinement egraphs.\nNeed to manually order close though.

\n
\n

https://docs.google.com/document/d/15amCalh9CSOWbbZ3d_haNad0Pw_jJ7vYcjMLkp7r-AA/edit?tab=t.0

\n

polar types in dolan. Maybe something like this restriction enables ground asym completion to terminate? Separate refinement closure into its polar and non polar components.

\n

lattice and ordered resolution\nhttps://cstheory.stackexchange.com/questions/12326/unification-and-gaussian-elimination respond here once I get it

\n

Unification and Knuth Bendix.\nI consider them to be opposites even if they can be encoded to each other.\nKB is forward reasoning\nunification is backward reasoning from a query or goal

\n

For speed reasons maybe you’d want to have 3-tuple 4-tuples etc available. Lempel ziv something something? https://en.wikipedia.org/wiki/Lempel%E2%80%93Ziv%E2%80%93Welch\nword equqation solving also had compression as an idea in there…

\n

string rewriting is a suffiicnet framework to simplify atomic equational proofs. Maybe overly powerful?

\n

Why can’t I binarize into a normal form\nweight by original size. Tie break\nabc = df\na b = e1\ne1 c = e2

\n

actual equations:\ne2 = e4

\n

overlaps\na b = e2\nb c = e5

\n

a + b = e_+1\na b = e_7\nstructured eids tagged by function symbol and identifier\nOnline extraction?\nidenitfy a term with the eid at time of creation. You can on demand compare

\n

“enodes” + “union find”\nNontrivial enode overlap is impossible. simplification is possible.\nWeighted union find = weighted Atomic KBO

\n
class UF():\n    weight : list[int]\n    parents : list[int]\n    def union():\n        x,y = find(x), find(y)\n        if weight[x] <= weight[y]:\n            parents[x] = y\n        else:\n            parents[x]
\n

For AC enodes, we do need to perform overlap. Term ordering matters (?)\n(X + Y + Z) :- (X + Y), (Y + Z).\nOnline extraction - we do not need to keep anything that

\n

Teitze transformations https://en.wikipedia.org/wiki/Tietze_transformations\ntsetsin\nANF\ndefinitional exte4nsions\nBut would this be crazy for multiset, linear, grobner, etc?\nax + by = z1\nx + by = z1\nz1 = z2

\n

ax + by = z1\nwhere a b are coprime\nax + by = z1\na z1 = b z2

\n

binary form of egraph. Partial application. App form\n(f, x) = fx\n(fx, y) = fxy\n(fxy, z) = fxyz\nLFHOL term orderings. Cody had some spiel

\n

enodes need an overlap api. eids need online extraction / term orderings to figure out winners. Or just online extraction?\nBut why does ordering matter then if the term associated with eclass is fluid.\nf(x,y,z) -> e1 can spontaneously become unoriented in this perspective if x lowers a bunch\nextraction repair f(x,y,z) <- e1

\n

memo : enode -> eclass\nparents : eclass -> eclass\nenodes : eclass -> Vec // vec?\nweights : eclass -> Int

\n

enodes kind of performs extraction\nIf there are two directions, that’s an overlap / confluence problem. Need to remove stuff from union find?

\n

Conservative extension makes sense either in compression or expansive form (decoding). efresh -> term decoding vs term -> egraph compressive

\n

Knuth Bendix + definition extension / teitze, conservative extension

\n
E, R, TermOrder\n--------------define\nE U {efresh = t}, R, TermOrder U {?}
\n

Why is a careful term ordering seemingly necessary for stuff besides union finds and straight egraphs?

\n

well ordering surgery. Ordinals (total well orders) have an otion of algebra. They have a uniquer global minimum.

\n

AC egrapha = ground completion +\nmultiple ac symbols.\nACRPO - flatten + use multiset ? No but first we have to consider the exact structure we’ve been given\nRubio https://courses.grainger.illinois.edu/cs576/sp2017/readings/18-mar-9/rubio-ac-rpo-long.pdf a fully syntactic acrpo\nhttps://arxiv.org/pdf/1403.0406 ACKBO\nhttps://courses.grainger.illinois.edu/cs576/sp2017/readings/18-mar-9/narendran-rusinowitz-ground-AC-compl.pdf\nA \\/ C, rpo\nhttps://courses.grainger.illinois.edu/cs576/sp2017/ meseguer readonig course. Pretty interesting stuff in here.\nhttps://courses.grainger.illinois.edu/CS476/fa2022/\nhttps://courses.grainger.illinois.edu/CS476/fa2022/readings/meseguer-set-theory-algebra-computer-science.pdf Set Theory and Algebra in Computer Science\nA Gentle Introduction to Mathematical Modeling\norder sorted algebras. hmm.\nhttps://dl.acm.org/doi/book/10.5555/547173 Algebraic Semantics of Imperative Programs\nhttps://courses.grainger.illinois.edu/cs476/sp2012/hw/lecture-notes-peter.pdf Formal Modeling and\nAnalysis of Distributed\nSystems in Maude

\n

https://www.lix.polytechnique.fr/~jouannaud/articles/acrvf.pdf

\n

https://www.sciencedirect.com/science/article/pii/S0304397506002647 Abstract canonical presentations\nproofs orderings. Good proofs.\nhttps://link.springer.com/chapter/10.1007/11780274_26 Completion Is an Instance of Abstract Canonical System Inference

\n

https://github.com/postechsv/maude-se

\n
import maude\nmaude.init()\nnat = maude.getModule('NAT')\nt = nat.parseTerm('1 + 2')\nt.reduce()\nprint(t)
\n
3
\n
t = nat.parseTerm('1 + 2')\nt.symbol()\nlist(t.arguments())\n#maude.Symbol()\nnat.parseTerm("X + Y")
\n
\u001b[31mWarning: \u001b[0m<standard input>, line 0: bad token \u001b[35mX\u001b[0m.\n\u001b[31mWarning: \u001b[0m<standard input>, line 0: no parse for term.
\n
maude.getModules()
\n
(fmod BOOL,\n fmod TRUTH-VALUE,\n fmod BOOL-OPS,\n fmod TRUTH,\n fmod EXT-BOOL,\n fmod INITIAL-EQUALITY-PREDICATE,\n fmod NAT,\n fmod INT,\n fmod RAT,\n fmod FLOAT,\n fmod STRING,\n fmod CONVERSION,\n fmod RANDOM,\n fmod BOUND,\n fmod QID,\n fth TRIV,\n fth STRICT-WEAK-ORDER,\n fth STRICT-TOTAL-ORDER,\n fth TOTAL-PREORDER,\n fth TOTAL-ORDER,\n fth DEFAULT,\n fmod LIST,\n fmod WEAKLY-SORTABLE-LIST,\n fmod SORTABLE-LIST,\n fmod WEAKLY-SORTABLE-LIST',\n fmod SORTABLE-LIST',\n fmod SET,\n fmod LIST-AND-SET,\n fmod SORTABLE-LIST-AND-SET,\n fmod SORTABLE-LIST-AND-SET',\n fmod LIST*,\n fmod SET*,\n fmod MAP,\n fmod ARRAY,\n fmod STRING-OPS,\n fmod NAT-LIST,\n fmod QID-LIST,\n fmod QID-SET,\n fmod META-TERM,\n fmod META-CONDITION,\n fmod META-STRATEGY,\n fmod META-MODULE,\n fmod META-VIEW,\n fmod META-LEVEL,\n fmod LEXICAL,\n mod COUNTER,\n mod LOOP-MODE,\n mod CONFIGURATION)
\n
import maude\nmaude.init()\n#nat = maude.getModule('NAT')\n#list(nat.getSymbols())\n#maude.input("load Nat .")\n#maude.input("vars X Y : Nat .")\nmod = maude.getCurrentModule()\nlist(mod.getSymbols())\nlist(mod.getSorts())\n\nmaude.input("""\nfmod SIMPLE-NAT is \n       sort Nat . \n       op zero : -> Nat . \n       op s_ : Nat -> Nat . \n       op _+_ : Nat Nat -> Nat . \n       vars N M : Nat . \n       eq zero + N = N . \n       eq s N + M = s (N + M) . \n      endfm\n""")\nsn = maude.getModule("SIMPLE-NAT")\nsn.parseTerm("s s N")\n\nfrom dataclasses import dataclass, field\ntype Sort = str\n@dataclass\nclass ModuleBuilder():\n    name : str\n    sorts : set[Sort] = field(default_factory=set)\n    vars : dict[str, Sort] = field(default_factory=dict)\n    ops : dict[str, tuple[list[Sort], Sort]] = field(default_factory=dict)\n    extras : list[str] = field(default_factory=list)\n    def build(self) -> str:\n        maude.input(str(self))\n        return maude.getModule(self.name)\n    def add_sort(self, sort: smt.SortRef):\n        self.sorts.add(sort.name())\n    def add_decl(self, decl: smt.FuncDeclRef):\n\n    def __str__(self):\n        lines = [f"fmod {self.name} is"]\n        for s in self.sorts:\n            lines.append(f"  sort {s} .")\n        for v, s in self.vars.items():\n            lines.append(f"  var {v} : {s} .")\n        for op, (arg_sorts, ret_sort) in self.ops.items():\n            arg_str = ' '.join(arg_sorts)\n            lines.append(f"  op {op} : {arg_str} -> {ret_sort} .")\n        lines.extend(self.extras)\n        lines.append("endfm")\n        return '\\n'.join(lines)\n\nModuleBuilder()
\n
\u001b[32mAdvisory: \u001b[0mredefining module \u001b[35mSIMPLE-NAT\u001b[0m.
\n
maude.__file__
\n
'/home/philip/philzook58.github.io/.venv/lib/python3.12/site-packages/maude/__init__.py'
\n
nat
\n
NAT
\n
maude.getModule("SMT")
\n
class StringKB():\n    memo : dict[object,int]\n    compress : dict[[tuple[int,int], int]]\n    # repeat : dict[tuple[EId, int], EId]\n    uf : list[int]\n    def makeset(self):\n        self.uf.append(len(self.uf))\n        return len(self.uf) - 1\n    def memo_obj(self, x):\n        if x in self.memo:\n            return self.memo[x]\n        else:\n            i = self.makeset()\n            self.memo[x] = i\n            return i\n    def add_str(self, xs):\n        xs = map(self.memo_obj, xs)\n        for i in range(len(xs) - 1):\n            a,b = xs[i], xs[i+1]\n            if (a,b) in self.compress:\n                c = self.compress[(a,b)]\n            else:\n                c = self.makeset()\n                self.compress[(a,b)] = c\n    def union(self, a, b):\n        ra = self.find(a)\n        rb = self.find(b)\n        if ra != rb:\n            self.uf[ra] = rb\n    def rebuild(self):\n        for (a,b), c in self.compress.items(): # overlap\n            for (d,e), f in self.compress.items():\n                if self.find(b) == self.find(d):\n                    ce, af = self.pair(c,e), self.pair(a,f)\n                    self.union(ce, af)\n        for (a,b), c in self.compress.items(): # congruence\n            ra, rb, rc = self.find(a), self.find(b), self.find(c)\n            self.union(self.pair(ra,rb), rc)
\n
def reclen(t1):\n    if isinstance(t1, tuple):\n        return 1 + sum(map(reclen, t1))\n    else:\n        return 1\n\nreclen((((1,2),3)))
\n
5
\n
def lt_kbo(t1, t2):\n    # ground kbo is size + tie breaking\n    if t1 == t2:\n        return False\n    elif isinstance(t1, tuple) and isinstance(t2, tuple):\n        l1, l2 = reclen(t1), reclen(t2)\n        if l1 < l2:\n            return True\n        elif l1 > l2:\n            return False\n        else:\n            for a,b in zip(t1,t2):\n                if a == b:\n                    continue\n                else:\n                    return lt_kbo(a,b)\n    elif not isinstance(t1, tuple) and not isinstance(t2, tuple):\n        return t1 < t2\n    elif not isinstance(t1, tuple) and isinstance(t2, tuple):\n        return True\n    else:\n        return False\n\nlt_kbo((1,2),(1,3))\nlt_kbo((1,2),(1,2,3))\nlt_kbo((1,2,3),(1,2))
\n
False
\n

a lambda egraph. (but only alpha)\nWhy not?

\n

did I ever do a KB egraph?

\n
def replace(t, lhs, rhs):\n    if t == lhs:\n        return rhs\n    elif isinstance(t, tuple):\n        return tuple(lambda x: replace(x, lhs, rhs) for x in t)\n    else:\n        return t
\n
class EGraph():\n    rules : dict\n\n    def union(self, t1, t2):\n        t1,t2 = self.canon(t1), self.canon(t2)\n    def find(self, t): ...\n    def rebuild(self, t):\n        foself.rules.keys():
\n
def lt_kbo(t1, t2):\n    # ground kbo is size + tie breaking\n    if reclen(t1) < reclen(t2):\n        return True\n    else:\n        \ndef rw(t, lhs, rhs):\n    if t == lhs:\n        return rhs\n    elif isinstance(t, tuple):\n        return tuple(map(rw(lhs,rhs), t))\n    else:\n        return t\n\nclass AsymComplete():
","headings":[{"level":1,"text":"Refinement E-Graphs","id":"refinement-e-graphs"},{"level":1,"text":"Example: Don’t Care Circuits","id":"example-don-t-care-circuits"},{"level":2,"text":"Don’t Care Semantics","id":"don-t-care-semantics"},{"level":1,"text":"Inequality Union Finds","id":"inequality-union-finds"},{"level":1,"text":"What Does A Refinement E-Graph Need on Top of This?","id":"what-does-a-refinement-e-graph-need-on-top-of-this"},{"level":2,"text":"Refinement Closure","id":"refinement-closure"},{"level":2,"text":"Refinement E-matching","id":"refinement-e-matching"},{"level":2,"text":"Refinement Extraction","id":"refinement-extraction"},{"level":1,"text":"A Toy Python Implementation of a Refinement E-Graph","id":"a-toy-python-implementation-of-a-refinement-e-graph"},{"level":1,"text":"Bits and Bobbles","id":"bits-and-bobbles"},{"level":1,"text":"4/2026","id":"4-2026"}]}}