Unification of Rational Trees and Minimal Finite Representation for Them

In classical miniKanren interpreters we always deal with finite terms due to occurs check restrictions, but there are examples when we need to deal with some kinds of infinite terms, more specifically that could be represented in finite form recursively. It can be achieved by erasing occurs check from unification procedure, but it isn't all we need, because interpreter will be unsound. To solve this, Rational tree model was presented before for Prolog interpreters. We study unification algorithms that saves soundness in Relational tree model and algorithms for representation minimization for recursively defined trees.

Author: Eridan Domoratskiy