dxo: A System for Relational Algebra and Differentiation
summary
dxo is a miniKanren relational system that manipulates s‑expression math: addition, multiplication, exponentiation, tagged-variable symbols, and natural numbers as little‑endian binary lists. The repository shows full code for four main relations do, simpo, evalo, reordero. do differentiates polynomials (and runs backwards to integrate), simpo simplifies/complicates with very limited rules, evalo evaluates or synthesizes expressions/environments, and reordero permutes sums/products. Demos return 24 derivative pairs, generate 200 complicate-to-x examples, solve 3‑4‑5 when nonzero constrained, and expose divergence and optimization limitations with planned AD and Knuth‑Bendix work.
AI-written summary · about
chapters (9)
- 0:00Intro
- 0:53Expressions dxo can Handle
- 1:274 Main Capabilities
- 1:544 Main Relations
- 2:37demo
- 3:45simpo rules
- 7:17Pythagorean Theorem
- 10:13Problem
- 12:15Future Work
related talks
17mTool Talk: DOOP
27mFrex: indexing modulo equations with free extensions (Extended Abstract)
35mFrex: Free Extensions for Normalization-by-Evaluation
14mHigher-Order Demand-Driven Symbolic Evaluation
22mComputing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
15mEquality Saturation Theory Exploration à la Carte