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.

翻译：本文在miniKanren框架下对理性树的合一性进行了研究。我们给出了理性树的定义，详细说明了合一算法并证明了其若干性质。同时，我们引入了多种启发式优化方法，并在多个相关基准测试中对其进行了评估。最后，我们探讨了理性合一算法与传统合一算法之间的关系，以及它们在关系式编程中共存的可能场景。