Unification of Deterministic Higher-Order Patterns (Full Version)

TL;DR

This paper introduces a sound and complete unification procedure for deterministic higher-order patterns, expanding previous methods and addressing their limitations in solving higher-order unification problems.

Contribution

It presents a novel unification algorithm that generalizes existing approaches, handling flex-flex pairs and dropping certain restrictions, though decidability remains open.

Findings

The unification procedure is sound and complete for deterministic higher-order patterns.

It generalizes Libal and Miller's FCU by removing global restrictions.

Decidability of the unification problem remains unresolved.

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 (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.