A higher-order unification implementation for automated theorem proving

Date

2025

Journal Title

Journal ISSN

Volume Title

Publisher

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.

Description

Keywords

unification, higher-order unification, zig, lambda calculus

Graduation Month

May

Degree

Master of Science

Department

Department of Computer Science

Major Professor

Torben Amtoft

Date

Type

Report

Citation