Unification of Deterministic Higher-Order Patterns

TL;DR

The paper addresses unification for deterministic higher-order patterns (DHPs), a class with deterministic matching but potentially infinitary minimal complete sets of unifiers. It defines DHPs in a $\beta\eta$-long normal form and presents a nondeterministic inference system that computes complete sets of unifiers $\mathsf{CSU}(E)$, with proofs of soundness and nondeterministic completeness. A central finding is that minimal complete sets $\mathsf{MCSU}(E)$ can be infinite, so decidability of DHP unification remains open, and the work contrasts DHPs with FCU and DSPs. A prototype implementation demonstrates practical applicability and discusses strategy choices to manage nontermination, indicating potential impact for program transformation and higher-order reasoning.

Abstract

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.