Andrej Bauer ; Anja Petković Komel - An extensible equality checking algorithm for dependent type theories

lmcs:7268 - Logical Methods in Computer Science, January 19, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:17)2022
An extensible equality checking algorithm for dependent type theories

Authors: Andrej Bauer ; Anja Petković Komel

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.


Volume: Volume 18, Issue 1
Published on: January 19, 2022
Accepted on: December 13, 2021
Submitted on: March 15, 2021
Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03B38 (Primary), 68Q42 (Secondary),F.4.1


Share

Consultation statistics

This page has been seen 490 times.
This article's PDF has been downloaded 655 times.