A higher-order unification implementation for automated theorem proving

Abstract

Higher-Order Unification is the process for algorithmically establishing equality between typed lambda expressions. This methodology serves as a foundation for numerous automated theorem provers such as Isabelle, λProlog and Carnap. However, Higher-Order Unification is inherently undecidable, with the most state-of-the-art solution being Gérard Huet's semi-decidable higher-order unification algorithm from 1975.

This report is an implementation of Huet's Algorithm for higher-order unification. The methodology involves parsing lambda expressions and converting them into De Bruijn index notation to eliminate the need for α-conversion. A β-reduction algorithm then reduces the lambda terms to beta-normal form. A matching tree for the two expressions is created to attempt to unify them through pattern matching and simplification. This implementation, written in the Zig programming language, uses its fast performance and memory optimization to create a performant abstract machine and to leverage the capability of Zig to compile into Webassembly.