An extensible equality checking algorithm for dependent type theories

TL;DR

This paper introduces a flexible, extensible equality checking algorithm for dependent type theories, combining type-directed rules, normalization, and user-defined rules, with proven soundness and implementation in the Andromeda 2 proof assistant.

Contribution

It presents a novel, general algorithm for equality checking in dependent type theories that is extensible and user-configurable, with formal guarantees and practical implementation.

Findings

Algorithm is sound and adaptable to various type theories.

Implemented in the Andromeda 2 proof assistant with user-defined rules.

Supports different notions of normal forms through parameter variation.

Abstract

We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for recognizing such rules, as well as a simple pattern-matching algorithm for applying them. A third component of the algorithm is a suitable notion of principal arguments, which determines a notion of normal form. By varying these, we obtain known notions, such as weak head-normal and strong normal forms. We prove that our algorithm is sound. We implemented it in the Andromeda 2 proof assistant, which supports user-definable type theories. The user need only provide the equality rules they wish to use, which the algorithm automatically classifies as computation or extensionality rules, and select appropriate principal arguments.