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 -
An extensible equality checking algorithm for dependent type theoriesArticle

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

    Consultation statistics

    This page has been seen 1496 times.
    This article's PDF has been downloaded 852 times.