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

Petković Komel, Anja (author), Bauer, Andrej (mentor)

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.

• Language: English
• Keywords: dependent type theory, algebraic theory, proof assistant, type-theoretic elaboration equality checking
• Work type: Doctoral dissertation
• Typology: 2.08 - Doctoral Dissertation
• Organization: FMF - Faculty of Mathematics and Physics
• Year: 2021
• PID: 20.500.12556/RUL-134058
• UDC: 510.6
• COBISS.SI-ID: 91931395
• Publication date in RUL: 23.12.2021

Secondary language

• Language: Slovenian
• Title: Meta-analiza teorij tipov z uporabo v oblikovanju formalnih dokazov

Abstract

V doktorski disertaciji predstavimo meta-analizo širokega razreda splošnih teorij tipov. Osredotočimo se na tri vidike: transformacije teorij tipov, dopolnitev teorij tipov in splošen algoritem za preverjanje enakosti. Teorije tipov zagotavljajo matematično osnovo za mnoge dokazovalne pomočnike. Da bi lažje razumeli interakcije med teorijami, študiramo njihove meta-teoretične lastnosti in jih preverjamo z implementacijo fleksibilnega dokazovalnega pomočnika Andromeda 2, ki omogoča, da uporabnik sam poda teorijo tipov. Naša meta-analiza je zgrajena na definiciji končnih teorij tipov. Definiramo sintaktične transformacije teorij tipov in dokažemo, da tvorijo relativno monado za sintakso. Da bi vključili strukturo izpeljivosti nadgradimo definicijo v transformacije teorij tipov, ki pokrije nekatere znane primere, kot sta Curry-Howardova korespondenca in razširitev z definicijo. Nato dokažemo nekaj meta-izrekov o transformacijah. Uporabnost transformacij teorij tipov se pokaže v definiciji dopolnitve. Dokažemo izrek o dopolnitvi, ki pravi, da ima vsaka končna teorija tipov dopolnitev. Na strani implementacije oblikujemo splošen algoritem za preverjanje enakosti, ki ga lahko uporabimo na končnih teorijah tipov. Algoritem je sestavljen iz faze ekstenzionalnosti, kjer uporabljamo pravila ekstenzionalnosti, in faze normalizacije, ki temelji na pravilih za izračun. Obe vrsti pravil sta definirani s pomočjo pogoja objektne obrnljivosti. Podamo tudi zadosten sintaktični kriterij za prepoznavanje teh pravil in algoritem s preprostimi vzorci, ki pravila uporablja. Tretja komponenta algoritma je primeren pojem glavnih argumentov, ki določa normalno obliko. S spreminjanjem glavnih argumentov dobimo znane pojme, kot sta šibka in močna normalna oblika. Dokažemo, da algoritem zadošča izreku skladnosti. Algoritem je implementiran v dokazovalnem pomočniku Andromeda 2.

• Keywords: odvisna teorija tipov, algebrajska teorija, dokazovalni pomočnik, dopolnitev teorij tipov, preverjanje enakosti