Teorie homotopických typů

Homotopy type theory ( HoTT , z anglického homotopy type theory ) je matematická teorie, speciální verze teorie typů , vybavená pojmy z teorie kategorií , algebraické topologie , homologické algebry ; je založena na vztahu mezi pojmy homotopický typ prostoru, vyšší kategorie a typy v logice a programovacích jazycích .

Univalent Foundations of Mathematics je program pro konstrukci univerzálního formálního jazyka pomocí teorie homotopických typů, který je konstruktivním základem pro moderní odvětví matematiky a poskytuje možnost automatické kontroly správnosti důkazů na počítači . Inicioval Vladimir Voevodsky v pozdních 2000s; podnětem k širšímu zájmu o univalentní základy byla knihovna formalizované matematiky „Foundations“ napsaná Voevodským, která se stala součástí knihovny UniMath v polovině 10. let a sloužila jako základ pro mnoho dalších knihoven ; v rámci programu byla velkým týmem matematiků napsána kniha .

Matematický důkaz v teorii homotopických typů spočívá ve stanovení „obyvatelnosti“ požadovaného typu, tedy v konstrukci výrazu odpovídajícího typu. Použití automatických důkazních systémů pro teorii využívá myšlenku Curry-Howardova izomorfismu a díky matematickému obsahu zakotvenému v typově teoretických konceptech, ve formálním jazyce teorie, je možné vyjádřit a ověřit spíše komplexní výsledky z abstraktních částí matematiky, které byly dříve považovány za neformalizovatelné softwarem.

Klíčovou myšlenkou teorie je axiom univalence , který postuluje rovnost objektů, mezi nimiž lze stanovit ekvivalenci, to znamená, že v teorii homotopických typů jsou izomorfní, homeomorfní, homotopicky ekvivalentní struktury považovány za rovnocenné; tento axiom zachycuje důležité vlastnosti interpretace vyšší kategorie a také poskytuje technické zjednodušení formálního jazyka.

Historie

Myšlenka použití intuicionistické teorie typů Pera Martina-Löfa k formalizaci vyšších kategorií sahá až k práci Mihaie Makkai ( maď. Makkai Mihály ), ve které byl vybudován systém FOLDS ( logika prvního řádu se závislými druhy ) . [1] . Klíčovým rozdílem mezi univalentními bázemi a Mackayovými myšlenkami je princip, že základními objekty matematiky nejsou vyšší kategorie, ale vyšší grupoidy. Protože vyšší grupoidy odpovídají Grothendieckově korespondenci s homotopickými typy , lze říci, že matematika, pokud jde o univalentní báze, studuje struktury na homotopických typech. Možnost přímého použití Martin-Löfovy teorie typů k popisu struktur na homotopických typech je důsledkem Voevodského konstrukce univalentního modelu teorie typů. Konstrukce tohoto modelu si vyžádala řešení četných technických problémů spojených s tzv. koherenčními vlastnostmi, a přestože hlavní myšlenky univalentních bází formuloval v letech 2005–2006, kompletní univalentní model v kategorii simpliciálních množin se objevil až v roce 2009 . Ve stejných letech jako tyto Voevodského studie byly provedeny další práce ke studiu různých souvislostí mezi teorií typů a teorií homotopie, zejména jednou z historicky důležitých událostí, která svedla dohromady vědce pracující v tomto směru, byl seminář v Uppsale v listopadu 2006 let [2] .

V únoru 2010 začal Voevodsky vytvářet knihovnu na Coq , která se následně rozrostla v „knihovnu univalentních bází“ společně vyvinutou širokým spektrem vědců .

Z iniciativy Voevodského byl akademický rok 2012–2013 na Institutu pro pokročilé studium vyhlášen „rokem univalentních základů“, byl otevřen speciální výzkumný program ve spolupráci s Audi a Kokan a v jeho rámci skupina matematiků a počítačoví vědci pracovali na vývoji teorie. Jedním z výsledků roku bylo společné vytvoření šestisetstránkové knihy „ Homotopic Type Theory: Univalent Foundations of Mathematics “, kterou účastníci vytvořili na webových stránkách programu zdarma pod licencí CC-SA ; ke spolupráci na knize byl vytvořen projekt na GitHubu [3] .

Účastníci programu, prezentovaného v úvodu knihy [4] :

Thorsten Altenkirch ( anglicky Thorsten Altenkirch )
Benedikt Ahrens ( Benedikt Ahrens )
Steve Audi _ _ _
Bruno Barras ( Bruno Barras )
Andrej Bauer ( slovinsky Andrej Bauer )
Marc Bezem ( Marc Bezem )
Yves Bertot ( Yves Bertot )
Benno van den Berg
Vladimír Voevodskij
Daniel Grayson ( Daniel Grayson , tvůrce systému počítačové algebry Macaulay2 )
André Joyal ( francouzsky André Joyal )
Thierry Cocan
Dan Licata ( Dan Licata )
Peter Lumsdaine ( Peter Lumsdaine )
Podle Martina-Löfa
Assia Mahboubi ( Assia Mahboubi )
Sergej Melikhov
Alvaro Pelayo ( Alvaro Pelayo )
Andrew Polonsky _ _
Matthieu Sozeau _ _
Bas Spitters ( Bas Spitters )
Michael Warren ( Michael Warren )
Eric Finster ( Eric Finster )
Noam Zeilberger ( Noam Zeilberger )
Michael Shulman _ _ _
Peter Aczel _ _ _
Hugo Herbelin , manažer vývojového projektu Coq

Úvod navíc naznačuje, že významným způsobem přispělo i šest studentů, a také si všímá příspěvku více než 20 vědců a praktiků, kteří v „roku univalentních základů“ navštívili Ústav pro vyšší studia (včetně tvůrce sémantiky λ-kalkul Dana Scott a vývojářské formalizace na Coq důkazů čtyřbarevného problému a Feit-Thompsonova teorému ( Georges Gontier ). Kniha se skládá ze dvou částí - "Základy" a "Matematika", v první části jsou uvedena hlavní ustanovení a definovány nástroje, ve druhé jsou implementace teorie homotopie, teorie kategorií , teorie množin , reálná čísla . postavený pomocí zavedených prostředků .

Základy

Teorie je založena na intenzionální variantě intuicionistické teorie typů Martina-Löfa a využívá interpretaci typů jako objektů teorie homotopie a vyšších kategorií. Z tohoto hlediska je tedy vztah příslušnosti bodu k prostoru považován za termín odpovídajícího typu: , svazek s bází - jako závislý typ . V tomto případě není potřeba reprezentovat prostory ve formě množin bodů vybavených topologií a reprezentovat spojitá zobrazení mezi prostory jako funkce, které zachovávají nebo odrážejí odpovídající bodové vlastnosti prostorů. Teorie homotopických typů považuje typové prostory a termíny těchto typů (body) za elementární pojmy a konstrukce nad prostory, jako jsou homotopie a svazky, za závislé typy. $v A$ $a:A$ $X$ $Sekera)$

Ve formální konstrukci teorie typů se používá typ-vesmír , jehož termíny jsou všechny ostatní neuniverzální („malé“) typy, typy jsou pak konstruovány tak, že navíc všechny termíny typu jsou také termíny. typu . Závislé typy (rodiny typů) jsou definovány jako funkce, jejichž kodoménou je nějaký typový vesmír. ${\mathcal U}_{0}$ ${\mathcal U}_{1},{\mathcal U}_{2},\tečky$ $U_{i}:U_{{i+1}}$ ${\mathcal U}_{i}$ ${\mathcal U}_{{i+1}}$ $B:A\to {\mathcal U}$

V teorii homotopických typů existuje několik způsobů, jak konstruovat nové typy z existujících. Základními příklady tohoto druhu jsou -types (závislé funkční typy, typy produktů ) a -types (závislé typy součtů ). Pro daný typ a rodinu lze zkonstruovat typ, jehož členy jsou funkce, jejichž kodoména závisí na prvku definičního oboru (geometricky lze takové funkce reprezentovat jako sekce nějakého svazku), stejně jako typ, jehož členy geometricky odpovídají prvkům celkového prostoru svazku. ${\boldsymbol \Pi }$ ${\boldsymbol \Sigma }$ $A:{\mathcal U}$ $B:A\to {\mathcal U}$ ${\boldsymbol \Pi }_{{x:A}}B(x)$ ${\boldsymbol \Sigma }_{{x:A}}B(x)$

Rovnost termínů stejného typu v teorii homotopických typů může být buď rovností „z definice“ ( ) nebo výrokovou rovností. Rovnost z definice implikuje výrokovou rovnost, ale ne naopak. Obecně je výroková rovnost termínů a typu reprezentována jako neprázdný typ , který se nazývá typ identity; termíny tohoto posledního typu jsou cesty pohledu v prostoru ; na typ identity je tedy nahlíženo jako na prostor cest (tj. souvislá mapování segmentu jednotky do ) z bodu do bodu . $a_{1}:=a_{2}$ $a_{1}$ $a_{2}$ $A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $p:a_{1}\rightsquigarrow a_{2}$ $A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $\mathbb {I}$ $A$ $a_{1}$ $a_{2}$

Axiom univalence

Intuicionistická teorie typů nám umožňuje definovat koncept ekvivalence typu (pro typy patřící do stejného vesmíru) a konstruovat funkci kanonickým způsobem od typu identity k typu ekvivalence : $A=B$ $A\simeq B$

(A=B)\to (A\simeq B)

Axiom univalence , formulovaný Voevodským, říká, že tato funkce je také ekvivalence:

(A=B)\simeq (A\simeq B)

to znamená, že typ identity dvou daných typů je ekvivalentní typu ekvivalence těchto typů. Jestliže a jsou výrokové typy, má axiom zvláště transparentní význam a scvrkává se na to, čemu se někdy říká Churchův princip extenzionality: rovnost výroků je logicky ekvivalentní jejich logické ekvivalenci; použití tohoto principu znamená, že se berou v úvahu pouze pravdivostní hodnoty výroků, nikoli však jejich význam. Důsledkem axiomu je funkční extenzialita , tedy tvrzení, že funkce, jejichž hodnoty jsou stejné pro všechny stejné hodnoty jejich argumentů, jsou si navzájem rovné. Tato vlastnost funkcí je důležitá v informatice. $A$ $B$

Axiom je některými filozofy matematiky považován za přesnou matematickou formulaci hlavní teze filozofie matematického strukturalismu , která vychází z běžné praxe matematického uvažování „až do izomorfismu “ nebo „do ekvivalence “ [ 5] .

Logika, množiny, grupoidy

Propozice ( pouhá propozice , „ holá propozice “) v teorii homotopických typů je definována jako typ , který je buď prázdný, nebo obsahuje jediný termín ; takové typy se nazývají propoziční. Pokud je typ prázdný, pak je odpovídající tvrzení nepravdivé, pokud obsahuje termín (symbolicky - ), pak je odpovídající výrok pravdivý a termín je považován za jeho důkaz. Teorie tedy používá intuicionistický koncept pravdy, podle kterého je pravdivost tvrzení chápána jako možnost předložení důkazu tohoto tvrzení. $P$ $p$ $P$ $P$ $p$ $p:P$ $P$ $p$

Fragment teorie homotopických typů, který se omezuje na operace s výrokovými typy, tedy s výroky, lze označit za logický fragment (logiku) této teorie. Logická disjunkce ve výrokovém fragmentu odpovídá typu sum-type , konjunkci typu součinu , implikaci funkčnímu typu , negaci typu , kde je prázdný typ (typ null). Logika odpovídající takovým konstrukcím je variantou intuicionistické logiky , zejména se v ní nekonají výroky jako zákon dvojité negace nebo vyloučeného středu . $A\vee B$ $A+B$ $A\wedge B$ $A\krát B$ $A\Šipka doprava B$ $A až B$ $\lne A$ $A\to \mathbf {0}$ ${\mathbf 0}$

Jakýkoli typ , který obsahuje dva nebo více odlišných členů , lze dát do vzájemné korespondence s výrokovým typem, který se získá identifikací všech členů typu , taková operace se nazývá výrokové zkrácení ( výrokové zkrácení ). To umožňuje rozlišovat mezi „výrokovou úrovní“ (výrokovou úrovní) teorie a homotopickou hierarchií jejích „vyšších“ nepropozičních úrovní. $X$ $x,y,\dots$ $X$

Za úrovní propozic následuje úroveň sestav . Množina v teorii homotopických typů je definována jako prostor (typ) s diskrétní topologií . Ekvivalentně lze množinu teoreticky popsat jako typ tak, že pro kterýkoli z jejích členů je typem výrok, to znamená buď prázdný (případ, kdy a jsou různé prvky množiny ), nebo obsahuje jediný prvek (tzv. případ, kdy a jsou stejným prvkem). Po úrovni množin následuje úroveň grupoidů (množina bodů a množina cest mezi každou dvojicí bodů) a úrovně -grupoidů všech řádů. $A$ $a_{1},a_{2}:A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $a_{1}$ $a_{2}$ $A$ $a_{1}$ $a_{2}$

Různé interpretace typově teoretických konceptů

Knihovny a implementace HoTT

Knihovny HoTT je několik projektů hostovaných na GitHubu (ve stejném úložišti, kde je umístěn zdrojový kód knihy), které vytvářejí formální popisy různých odvětví matematiky pomocí systémů automatického důkazu využívajících konstrukcí teorie homotopických typů.

V projektu Vladimíra Voevodského, nazvaném „Knihovna univalentních bází“ [6] , je použita speciálně vyvinutá minimální bezpečná podmnožina Coq , která zajišťuje ideologickou čistotu a spolehlivost konstrukcí v souladu s teorií. Projekt HoTT [7] je veden standardními nástroji Coq, implementovanými v rámci výzkumného programu Institute for Advanced Study a obecně se řídí knihou , od roku 2020 se na projektu podílí 48 vývojářů, nejvíce aktivními jsou Jason Gross, Michael Shulman, Ali Kaglayan a Andrey Bauer [8] . Paralelní projekt existuje také v Agdě [9] .

Existuje několik experimentálních interaktivních důkazních systémů založených výhradně na HoTT: Arend , RedPRL, redtt, cooltt a ve verzi Agda 2.6.0 byl přidán tzv. „kubický režim“, který umožňuje plné využití typů homotopie.

Poznámky

↑ Makkai Mihaly. Logika prvního řádu se závislými druhy, s aplikacemi na teorii kategorií (anglicky) (1995). Získáno 5. prosince 2014. Archivováno z originálu 10. října 2015.
↑ Typy identit – topologická a kategorická struktura . Workshop, Uppsala, 13.-14. listopadu 2006 (2006) . Datum přístupu: 5. prosince 2013. Archivováno z originálu 18. prosince 2014. (neurčitý)
↑ Homotopy Type Theory: Univalent Foundations of Mathematics Project Source Codes on GitHub
↑ HoTT, 2013 , str. iii.
↑ Steve Avodey. Strukturalismus, neměnnost a univalence // Philosophia Mathematica . - Oxford University Press , 2014. - V. 22 , č. 1 . — ISSN 0031-8019 . - doi : 10.1093/philmat/nkt030 .
↑ Projekt Univalent Base Library na GitHubu
↑ Projekt Homotopy Type Theory na GitHubu
↑ HoTT 20. března 2011 — 02. října 2020 Příspěvky do hlavního serveru, kromě sloučení commitů .
↑ Projekt knihovny Agda HoTT na GitHubu

Literatura

Teorie homotopických typů: Univalentní základy matematiky . - Princeton : Institute for Advanced Study , 2013. - 603 s.
Steve Awodey, Álvaro Pelayo, Michael A. Warren. Voevodského Univalence Axiom in Homotopy Type Theory (anglicky) // Notices of the AMS . - 2013. - Sv. 60 , č. 9 . - S. 1164-1167 .
Hannes Hummel. Předefinují počítače kořeny matematiky? . Když legendární matematik našel chybu ve své vlastní práci, pustil se do počítačem podporovaného pátrání po odstranění lidské chyby. Musí přepsat staletí stará pravidla, která jsou základem celé matematiky . Quanta Magazine (19. května 2015) . Staženo: 31. prosince 2017.
Don Monroe. Nový typ matematiky? (anglicky) // Komunikace ACM . - 2014. - Sv. 57 , č. 2 . - str. 13-15 . - doi : 10.1145/2557446 .
Andrej Rodin. Logický a geometrický atomismus od Leibnize k Voevodskému // Problémy filozofie . - 2016. - č. 6 . - S. 134-142 .

Odkazy

cs.cmu.edu/~rwh/courses/hott/ - kursové materiály o teorii homotopického typu vyučované Robertem Harperem na Carnegie Mellon University