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.

翻译：我们提出将一阶句法合一推广到一种项代数结构，其中变量属于互不相交的、全序的线性集合集合，称为变量类。与一阶句法合一不同，给定问题中的变量数量并非有限受控，因为某些变量类与自指递归替换相关联，允许构造包含无穷多个变量的无穷深层项，我们称之为算术递进项。此类构造与归纳推理相关。我们证明，对于所谓简单线性循环，可合一性是可判定的，并推测在限制较少的类中该性质依然可判定。