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.

翻译：我们提出了一种针对确定性高阶模式的完备且可靠的统一过程，这类模式是由Yokoyama等人引入的一类简单类型lambda项，并伴随有确定性匹配问题。我们的统一过程可视为完全高阶统一的一种特例，其中flex-flex对能以最一般的方式求解。此外，我们的方法通过取消Libal和Miller近期提出的函数即构造子高阶统一（FCU）中关于变量参数的全局限制，从而推广了该方法，但这一推广也失去了每个可解问题都具有最一般统一子的性质。实际上，确定性高阶模式的最小完备统一子集可能是无限的，因此该统一问题的可判定性仍是一个开放问题。