Higher-Order Unification from E-Unification with Second-Order Equations and Parametrised Metavariables

EasyChair Preprint 8680

Abstract

Type checking and, to a larger extent, type and term inference in programming languages and proof assistants can be implemented by means of unification. In presence of dependent types, variations of higher-order unification are often used, such as higher-order pattern unification. In practice, there are often several mechanisms for abstraction and application, as well as other eliminators (such as projections from pairs) that have to be accounted for in the implementation of higher-order unification for a particular language. In this work, we study the possibility of representing various higher-order unification problems as a special case of E-unification for second-order algebra of terms. This allows us to present $\beta$-reduction rules for various application terms, and some other eliminators as equations, and reformulate higher-order unification problems as $E$-unification problems with second-order equations. We then present a procedure for deciding such problems, introducing second-order \emph{mutate} rule (inspired by one-sided paramodulation) and generic versions of \emph{imitate} and \emph{project} rules. We also provide a prototype Haskell implementation for syntax-generic higher-order unification based on these ideas in Haskell programming language.

Keyphrases: E-unification, dependent types, higher-order unification, paramodulation, second-order equations, type inference, unification

@booklet{EasyChair:8680,
  author    = {Nikolai Kudasov},
  title     = {Higher-Order Unification from E-Unification with Second-Order Equations and Parametrised Metavariables},
  howpublished = {EasyChair Preprint 8680},
  year      = {EasyChair, 2022}}