dxo: A System for Relational Algebra and Differentiation

TL;DR

dxo is a miniKanren-based relational system capable of algebraic manipulation and differentiation of mathematical expressions, supporting forward and backward reasoning for differentiation, integration, simplification, and evaluation.

Contribution

It introduces a novel relational framework for algebra and differentiation implemented in miniKanren, enabling bidirectional reasoning over expressions.

Findings

dxo can differentiate polynomials accurately

dxo can perform symbolic integration by running differentiation backwards

dxo simplifies and reorders expressions effectively

Abstract

We present dxo, a relational system for algebra and differentiation, written in miniKanren. dxo operates over math expressions, represented as s-expressions. dxo supports addition, multiplication, exponentiation, variables (represented as tagged symbols), and natural numbers (represented as little-endian binary lists). We show the full code for dxo, and describe in detail the four main relations that compose dxo. We present example problems dxo can solve by combining the main relations. Our differentiation relation, do, can differentiate polynomials, and by running backwards, can also integrate. Similarly, our simplification relation, simpo, can simplify expressions that include addition, multiplication, exponentiation, variables, and natural numbers, and by running backwards, can complicate any expression in simplified form. Our evaluation relation, evalo, takes the same types of expressions as simpo, along with an environment associating variables with natural numbers. By evaluating the expression with respect to the environment, evalo can produce a natural number; by running backwards, evalo can generate expressions (or the associated environments) that evaluate to a given value. reordero also takes the same types of expressions as simpo, and relates reordered expressions.