| Autor: |
Andrej Bauer, Anja Petković Komel |
| Jazyk: |
angličtina |
| Rok vydání: |
2022 |
| Předmět: |
|
| Zdroj: |
Logical Methods in Computer Science, Vol Volume 18, Issue 1 (2022) |
| Druh dokumentu: |
article |
| ISSN: |
1860-5974 |
| DOI: |
10.46298/lmcs-18(1:17)2022 |
| Popis: |
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. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
