Efficient Rational Unification for miniKanren
2026-07-27 • Logic in Computer Science
Logic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors developed a new method to combine logical pieces called rational term unification that works well when the data is kept over time (persistent settings). Their method performs similarly to a well-known existing approach called miniKanren unification. They based their algorithm on a classic technique by Martelli and Rossi but made some changes to fit common practices better. They also used a formal proof tool, Rocq, to verify their method's key properties and tested how well it performs.
rational term unificationpersistent settingsminiKanrentriangular substitutionHerbrand termsMartelli-Rossi algorithmformal proofRocq proof assistantalgorithm performance
Authors
Eridan Domoratskiy, Dmitry Boulytchev
Abstract
We present an efficient algorithm for rational term unification in persistent settings which demonstrates a comparable performance w.r.t. the conventional miniKanren unification with triangular substitution for Herbrand terms. Our algorithm is based on existing Martelli-Rossi approach and uses some adjustments to make the implementation more conventional. We provide certified proofs of principal algorithm properties in the Rocq proof assistant and showcase the results of a comprehensive performance evaluation.