Compiling Set Theory into WebGPU Compute Shaders (Bypassing the AST)

I’ve been working on a compiler for the Monist Engine, a Rust and WebGPU-based logic environment for evaluating Quine’s New Foundations (NF) set theory.

Because NF natively allows for cyclic, self-referential structures (like the Universal Set), evaluating it poses a major architectural problem. If you try to feed non-well-founded sets into traditional AST evaluators or hierarchical type-checkers, they inevitably chase the relation down the substitution chain and hit a stack overflow.

To evaluate these topologies safely without relying on heavy artificial safeguards, I designed the engine to take a fundamentally different approach: compiling away the AST into interaction nets and shifting the evaluation into VRAM.

The Bottleneck: CFGs vs. Relative Typestates
W.V.O. Quine's New Foundations (NF) theory operates on ontological monism. It provides a one-sorted logic where the universal set and transfinite collections exist natively as first-class objects. This contrasts with standard ZFC theory, which relies on infinite axiomatic schemas, or NBG, which awkwardly splits entities into sets and proper classes. To prevent resulting infinite loops as with Russell's Paradox, NF introduces stratification. This grammatical rule dictates that the relative typestates of variables must ascend strictly (e.g., x ∈ y requires the type of y to be exactly x + 1).

When you try to compute these non-well-founded sets, standard hierarchical type-checkers fail terribly. Single-pass compiler front-ends rely on Context-Free Grammars and Pushdown Automata. Because a pushdown automaton uses a single LIFO memory stack, pumping a stratified formula breaks variable level-matching. Any attempt to natively resolve a self-referential loop exhausts the environment's memory and crashes the compiler.

The Geometry Layer: Kosaraju & Bellman-Ford
Instead of a traditional type-checker, the monist-core crate translates the parsed AST into a topographical constraint matrix (GraphArena). Equality (x = y) maps to bidirectional 0-weight edges, while membership (x ∈ y) maps to directed +1/-1 edges.

Before execution, the CPU runs Kosaraju's Strongly Connected Components (SCC) algorithm. It executes a two-pass Depth-First Search (DFS), first calculating the finishing times across the graph, then transposing the entire matrix and running a backward DFS. This mathematically isolates 0-weight equivalence rings without traversing horizontal cross-edges. The engine then contracts these redundant semantic cycles into single representative variables, effectively shrinking the graph in linear time.

Next, the solver runs a Bellman-Ford shortest path traversal to assign an integer potential to every node while satisfying all edge constraints. If the engine encounters a self-referential paradox (like x ∈ x), it forces the vertex to simultaneously hold a +1 and -1 positional weight. Bellman-Ford flags this topologically as a negative-weight cycle. By mapping the Minimum Cycle Mean, the engine intercepts the extensionality collision statically and halts execution before allocating call stack frames, bypassing infinite regression entirely.

Variable Annihilation & Lock-Free Atomics
To actually evaluate the logic, maintaining named variables creates unresolvable bottlenecks. My monist-comb compiler destroys the variables, replacing them with a nameless representation using global De Bruijn indexing, and compiles the logic down into untyped S, K, I combinators.

To prevent these untyped combinators from recursing infinitely into unstratified loops, the compiler extracts the integer typestates generated by the CPU's Bellman-Ford pass and burns them into the physical interaction graph as T-functor wrappers (implemented via Comb::T.app(comb)).

Finally, the WgpuExecutor maps this combinator graph directly into WebGPU storage buffers. It dispatches a reduce.wgsl shader that runs lock-free, atomic Compare-And-Swap loops to collide the nodes in VRAM until interactions == 0. Rather than managing lexical environments or dynamic typestates, the shader evaluates logic as parallel graph transformations.

Topological Recursion Cost as an Observable
What I find a little strange to consider is the measurement outcome. Normally, we measure logical execution either abstractly (big-O time complexity) or chronologically (CPU cycles, which fluctuate wildly due to cache misses and OS interrupts). Self-referential paradoxes are expected to simply run forever or crash the stack.

But because Monist evaluates logic via physical interaction nets, the GPU outputs a deterministic, reproducible integer: the exact count of graph-rewrite collisions required to normalize a non-well-founded topology into a stable fixpoint. This "Topological Recursion Cost" assigns a measurable geometric friction to logical proofs and paradoxes. A self-referential loop that would normally OOM a traditional evaluator might resolve here in exactly 47 physical node collisions.

Getting Started
If you want to see how the compiler handles this translation locally, you can use the CLI REPL to map a constraint down to the combinator graph:

$ monist-cli
> assume id_def: id = { x, y | x = y }
> compile id_def
[Geometry] Kosaraju SCC collapsed 0-weight rings.
[Geometry] Bellman-Ford shortest-path resolved. Typestates validated.
[Compiler] Lexical environment dropped.
[Compiler] Generated Graph: S (K (t_inject 0)) I

The repo and compiler source are available if anyone is interested in how the SCC matrix contraction, the De Bruijn leveling, or the WGSL compute shaders are implemented: https://firstsynth.dev/monist