We present a sound and complete unification procedure for deterministic higher-order patterns, a class of simply-typed lambda terms introduced by Yokoyama et al. which comes with a deterministic matching problem. Our unification procedure can be seen as a special case of full higher-order unification where flex-flex pairs can be solved in a most general way. Moreover, our method generalizes Libal and Miller's recent functions-as-constructors higher-order unification (FCU) by dropping their global restriction on variable arguments, thereby losing the property that every solvable problem has a most general unifier. In fact, minimal complete sets of unifiers of deterministic higher-order patterns may be infinite, so decidability of the unification problem remains an open question. Nevertheless, our method can be more useful than FCU in practice.

翻译：我们提出了一种针对确定性高阶模式的可靠且完备的统一化过程，这类简单类型lambda项由Yokoyama等人提出，具有确定性匹配特性。我们的统一化过程可视为完整高阶统一化的特例，其中柔性-柔性对能以最一般方式求解。此外，本方法推广了Libal与Miller近期提出的函数作为构造器高阶统一化（FCU）方法，通过取消其对变量参数的全局限制，从而丧失了"每个可解问题都存在最一般合一子"的性质。实际上，确定性高阶模式的最小完备合一子集可能是无限的，因此该统一化问题的可判定性仍是开放问题。尽管如此，本方法在实践中比FCU更具实用性。