Recursive First-order Syntactic Unification Modulo Variable Classes

We present a generalization of first-order syntactic unification to a term algebra where variables belong to disjoint, total, linearly ordered sets referred to as variable classes. Unlike First-order syntactic unification, the number of variables within a given problem is not finitely bound as some variable classes are associated with self-referencing recursive substitutions allowing the construction of infinitely deep terms containing infinitely many variables, what we refer to as arithmetic progressive terms. Such constructions are related to inductive reasoning. We show that unifiability is decidable for so-called simple linear loops and conjecture decidability for less restrictive classes.