Meta-analysis of type theories with an application to the design of formal proofs : doctoral thesis

english

doktorska dela

2021

algebraic theory   dependent type theory   logic   mathematics   proof assistant   type-theoretic elaboration equality checking

Univerza v Ljubljani, Fakulteta za matematiko in fiziko
(Obvezni izvod spletne publikacije)

In this thesis we present a meta-analysis of a wide class of general type theories, focusing on three aspects: transformations of type theories, elaboration of type theories, and a general equality checking algorithm. Type theories provide the mathematical foundations of many proof assistants. We build towards understanding of how they interact by studying their meta-theoretic properties and checking them against an implementation of the flexible proof assistant Andromeda 2, which supports user-specified type theories. Our meta-analysis is built on the definition of finitary type theories. We define syntactic transformations of type theories and prove they form a relative monad for the syntax. To account for the derivability structure, we upgrade the definition to type-theoretic transformations that cover some familiar examples, like propositions as types translation and the definitional extension. Once these definitions are accomplished we prove some meta-theorems. The usefulness of type-theoretic transformations is unveiled in the definition of an elaboration and we prove an elaboration theorem, saying that every finitary type theory has an elaboration. To tackle the implementational side, we design a general and user-extensible equality checking algorithm, applicable to a finitary type theories. The algorithm is composed of a type-directed phase for applying extensionality rules and a normalization phase based on computation rules. Both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We specify sufficient syntactic criteria for recognizing such rules and 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.

12.05.2023