arXiv subjects

Eridan Domoratskiy

Publications and source records attributed to Eridan Domoratskiy.

3 recordsLinked to original sources

arXiv2026

Efficient Rational Unification for miniKanren

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.

cs.LO↗

arXiv2025

An Empirical Study of Rational Tree Unification for miniKanren

We present a study of unification for rational trees in the context of miniKanren. We give the definition of rational trees, specify the unification algorithm and prove some of its properties. We also introduce a number of heuristic optimizations and evaluate them for a number of relevant benchmarks. Finally we discuss the relations between rational and conventional unification algorithms and possible scenarios of their coexistence in the context of relational programming.

cs.LO↗

arXiv2024

A Relational Solver for Constraint-based Type Inference

We present a miniKanren-based type inferencer for an educational programming language with first-class functions, S-expressions, and pattern-matching. The language itself is untyped which adds a certain specificity to the problem and requires the employment of techniques conventionally used in implicit/gradual typing settings. The presence of polymorphic and recursive types poses a certain challenge when implementing the inferencer in miniKanren and requires a number of tricks, optimizations, and extensions to be used; we report on those as well.

cs.PL↗