Generalization techniques have many applications, such as template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive-type theories to further develop proof generalization techniques and other transformations. So far, investigations concerned with anti-unification (AU) over lambda terms and similar type theories have focused on developing algorithms for well-studied variants. These variants forbid the nesting of generalization variables, restrict the structure of their arguments, and are unitary. Extending these methods to more expressive variants is important to applications. We consider the case of nested generalization variables and show that the AU problem is nullary (using capture-avoiding substitutions), even when the arguments to free variables are severely restricted.

翻译：通用化技术在众多应用中发挥着重要作用，例如模板构建、参数泛化与索引。现代交互式定理证明器可利用表达性类型理论上通用化方法的进展，进一步开发证明泛化技术及其他变换。目前，针对λ项及类似类型理论的反统一（AU）研究主要集中于为经过充分研究的变体开发算法。这些变体禁止泛化变量的嵌套、限制其参数结构，且为单一解问题。将这些方法扩展至更具表达力的变体对应用至关重要。本文考虑嵌套泛化变量的情形，并证明即使自由变量的参数受到严格限制，反统一问题仍为零解问题（采用避免捕获的替换）。