Effective metatheory for type theory : PhD thesis

angleški

doktorska dela

2021

algebrajska teorija   Disertacije   dokazovalni pomočnik   Matematična logika   matematika   metajezik   odvisna teorija tipov   računski učinki

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

V disertaciji definiram končne teorije tipov kot širok razred teorij tipov v stilu Martina-Löfa in oblikujem programski jezik za izpeljevanje sodb v splošnih teorijah tipov. Sodobne računalniške implementacije teorije tipov se zanašajo na njeno računsko interpretacijo bodisi preko rezultatov o odločljivosti ali realizabilnosti. Takšni rezultati pa niso na voljo za vse teorije tipov, ki jih srečamo v literaturi, zato njihova implementacija predstavlja izziv. Radi bi implementirali fleksibilen dokazovalni pomočnik, ki omogoča, da uporabnik sam določi teorijo tipov. Za to pa potrebujemo splošno definicijo teorije tipov, ki oriše njeno strukturo. V disertaciji podam matematično natančno definicijo razreda končnih teorij tipov, ki pokrije znane primere, vključno z ekstenzionalno teorijo tipov, računom konstrukcij in homotopsko teorijo tipov. Najprej se osredotočim na matematični razvoj končnih teorij tipov, preden se posvetim njihovi implementaciji v dokazovalnih pomočnikih. Definicija je zgrajena po stopnjah. Začnemo s surovo sintakso, surovimi pravili in surovimi teorijami tipov, nato razmejimo končna pravila in teorije tipov ter na koncu opredelimo standardne teorije tipov. S temi definicijami lahko dokažemo tudi metateoretične rezultate kot sta izrek o enoličnosti tipov in izrek o eliminaciji rezov. Da bi končne teorije tipov lažje implementirali v dokazovalnem pomočniku, jih preoblikujem v kontekstno neodvisne teorije tipov, ki omogočajo pravilno ravnanje s prostimi spremenljivkami. Definicija kontekstno neodvisnih teorij tipov je ponovno zgrajena po stopnjah. Za vsako stopnjo dokažem primerne metaizreke. Formalizma končnih torij tipov in kontekstno neodvisnih teorij tipov sta povezana preko izrekov prevedbe. Uvedem metajezik Andromeda (AML), učinkovni programski jezik, ki omogoča priročno ravnanje s sodbami in pravili v kontekstno neodvisnih teorijah tipov, ki jih uporabnik lahko sam določi. Jezik tudi podpira običajne tehnike za razvoj dokazov. AML izkoristi algebrajske učinke in poganjalce, da na modularen način z lokalnimi hipotezami razširi algoritme v dokazovalnih pomočnikih. Operacijska semantika jezika AML se naslanja na dvosmerno tipiziranje in pomaga uporabniku unovčiti informacije o kontekstu. S tem pokaže uspešno interakcijo z operacijami učinkov. AML je implementiran v dokazovalnem pomočniku Andromeda. Opišem tudi prve poskuse razvoja kontekstno neodvisnih teorij tipov z računalniško pomočjo v AML.

12.05.2023