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 by dropping their global condition 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项，其匹配问题具有确定性。我们的合一化程序可视为完全高阶合一化的一个特例，其中柔性-柔性对能以最一般的方式求解。此外，我们的方法推广了Libal和Miller近期提出的函数作为构造子的高阶合一化，通过取消其对变量参数的全局约束条件，从而丧失了每个可解问题都存在最一般合一子的性质。事实上，确定性高阶模式的最小完备合一子集可能是无限的，因此该合一化问题的可判定性仍是一个开放性问题。