Teoria tipului de homotopie

Homotopy type theory ( HoTT , din engleză homotopy type theory ) este o teorie matematică, o versiune specială a teoriei tipurilor , dotată cu concepte din teoria categoriilor , topologie algebrică , algebră omologică ; se bazează pe relația dintre conceptele de tipul homotopie de spațiu, categorii superioare și tipuri din limbaje logice și de programare .

Univalent Foundations of Mathematics este un program pentru construirea unui limbaj formal universal folosind teoria tipurilor homotopie, care este o bază constructivă pentru ramurile moderne ale matematicii și oferă capacitatea de a verifica automat corectitudinea dovezilor pe computer . Inițiat de Vladimir Voevodsky la sfârșitul anilor 2000; impulsul pentru un interes mai larg pentru fundațiile univalente a fost biblioteca de matematică formalizată „Fundații” scrisă de Voevodsky, care a devenit parte a bibliotecii UniMath la mijlocul anilor 2010 și a servit drept bază pentru multe alte biblioteci ; a fost scrisă de o echipă numeroasă de matematicieni .

Dovada matematică în teoria tipurilor de homotopie constă în stabilirea „locuibilitatii” tipului cerut, adică în construirea unei expresii de tipul corespunzător. Utilizarea sistemelor de demonstrare automată pentru teorie exploatează ideea izomorfismului Curry-Howard , iar datorită conținutului matematic încorporat în conceptele teoretice de tip, în limbajul formal al teoriei, este posibil să se exprime și să se verifice mai degrabă. rezultate complexe din secțiuni abstracte de matematică care anterior erau considerate neformalizabile de software.

Ideea cheie a teoriei este axioma univalenței , care postulează egalitatea obiectelor între care se poate stabili echivalența, adică în teoria tipului de homotopie, structurile izomorfe, homeomorfe, echivalente homotopic sunt considerate egale; această axiomă surprinde proprietăți importante ale interpretării de categorie superioară și oferă, de asemenea, o simplificare tehnică a limbajului formal.

Istorie

Ideea de a folosi teoria intuiționistă a tipurilor a lui Per Martin-Löf pentru a formaliza categorii superioare se întoarce la lucrarea lui Mihai Makkai ( Hung. Makkai Mihály ), în care a fost construit sistemul FOLDS ( logica de ordinul întâi cu sortări dependente ) [1] . Diferența cheie dintre bazele univalente și ideile lui Mackay este principiul că obiectele fundamentale ale matematicii nu sunt categorii superioare, ci grupoide superioare. Deoarece grupoizii superiori corespund corespondenței Grothendieck cu tipurile de homotopie , se poate spune că matematica, în ceea ce privește bazele univalente, studiază structurile pe tipuri de homotopie. Posibilitatea utilizării directe a teoriei tipurilor Martin-Löf pentru a descrie structuri pe tipuri de homotopie este o consecință a construcției lui Voevodsky a unui model univalent de teorie a tipurilor. Construcția acestui model a necesitat soluționarea a numeroase probleme tehnice asociate așa-numitelor proprietăți de coerență și, deși ideile principale de baze univalente au fost formulate de el în anii 2005–2006, a apărut doar un model univalent complet în categoria mulțimilor simple . în 2009 . În aceiași ani cu aceste studii ale lui Voevodsky, s-au efectuat și alte lucrări pentru a studia diverse legături dintre teoria tipurilor și teoria homotopiei, în special, unul dintre evenimentele importante din punct de vedere istoric care a reunit oamenii de știință care lucrează în această direcție a fost un seminar la Uppsala în noiembrie. 2006 ani [2] .

În februarie 2010, Voevodsky a început să creeze o bibliotecă pe Coq , care a crescut ulterior într-o „biblioteca de baze univalente” dezvoltată în comun de o gamă largă de oameni de știință .

La inițiativa lui Voevodsky, anul universitar 2012–2013 la Institutul de Studii Avansate a fost declarat „anul fundațiilor univalente”, a fost deschis un program special de cercetare în cooperare cu Audi și Kokan , iar în cadrul acestuia un grup de matematicieni și informaticienii au lucrat la dezvoltarea teoriei. Unul dintre rezultatele anului a fost realizarea în comun de către participanții a cărții de șase sute de pagini „ Teoria tipurilor homotopice: Fundamente univalente ale matematicii ”, postată pe site-ul programului pentru acces gratuit sub licența CC-SA ; a fost creat un proiect pe GitHub [3] pentru a colabora la cartea .

Participanții la program, prezentați în introducerea cărții [4] :

Thorsten Altenkirch ( în engleză Thorsten Altenkirch )
Benedikt Ahrens ( Benedikt Ahrens )
Steve Audi _ _ _
Bruno Barras ( Bruno Barras )
Andrej Bauer ( slovenă Andrej Bauer )
Marc Bezem ( Marc Bezem )
Yves Bertot ( Yves Bertot )
Benno van den Berg
Vladimir Voevodsky
Daniel Grayson ( Daniel Grayson , creatorul Macaulay2 computer algebra system )
André Joyal ( franceză André Joyal )
Thierry Cocan
Dan Licata ( Dan Licata )
Peter Lumsdaine ( Peter Lumsdaine )
După Martin-Löf
Assia Mahboubi ( Assia Mahboubi )
Serghei Melihov
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 , manager de proiect de dezvoltare Coq

În plus, introducerea indică faptul că șase studenți au avut și contribuții semnificative și, de asemenea, remarcă contribuția a peste 20 de oameni de știință și practicieni care au vizitat Institutul de Studii Superioare în „anul fundațiilor univalente” (inclusiv creatorul semanticii λ-calcul Dana Scott și formalizările dezvoltatorului pe Coq ale dovezilor problemei cu patru culori și teorema Feit-Thompson ( Georges Gontier ). Cartea este construită în două părți - „Fundamente” și „Matematică”, în prima parte sunt enunțate principalele prevederi și instrumentele sunt definite, în a doua - implementări ale teoriei homotopiei, teoria categoriilor , teoria mulțimilor , numerele reale sunt construit folosind mijloacele introduse .

Bazele

Teoria se bazează pe o variantă intensională a teoriei intuiționiste a tipurilor a lui Martin-Löf și folosește interpretarea tipurilor ca obiecte ale teoriei homotopiei și categorii superioare. Deci, din acest punct de vedere, relația de apartenență a unui punct la spațiu este considerată ca un termen de tipul corespunzător: , un mănunchi cu bază - ca tip dependent . În acest caz, nu este nevoie să se reprezinte spații sub formă de mulțimi de puncte echipate cu topologia și să se reprezinte mapări continue între spații ca funcții care păstrează sau reflectă proprietățile punctuale corespunzătoare ale spațiilor. Teoria tipurilor homotopiei consideră spațiile tip și termenii acestor tipuri (puncte) ca concepte elementare, iar construcțiile peste spații, cum ar fi homotopiile și mănunchiurile, ca tipuri dependente. $a\în A$ $a:A$ $X$ $Topor)$

În construcția formală a teoriei tipurilor, se folosește universul tip , ai cărui termeni sunt toate celelalte tipuri neuniversale („mice”), apoi tipurile sunt construite astfel încât , în plus, toți termenii tipului sunt de asemenea termeni . de tipul . Tipurile dependente (familiile de tipuri) sunt definite ca funcții al căror codomeniu este un tip-univers. ${\mathcal U}_{0}$ ${\mathcal U}_{1},{\mathcal U}_{2},\dots$ $U_{i}:U_{{i+1}}$ ${\mathcal U}_{i}$ ${\mathcal U}_{{i+1}}$ $B:A\la {\mathcal U}$

În teoria tipurilor de homotopie, există mai multe moduri de a construi noi tipuri din cele existente. Exemple de bază de acest fel sunt -types (tipuri funcționale dependente, tipuri de produse ) și -types ( tipuri dependente de sumă ). Pentru un anumit tip și familie , se poate construi un tip ai cărui termeni sunt funcții al căror codomeniu depinde de un element al domeniului de definiție (geometric, astfel de funcții pot fi reprezentate ca secțiuni ale unui pachet), precum și un tip ai cărui termeni geometric corespund elementelor din spațiul total al mănunchiului. ${\boldsymbol \Pi }$ ${\boldsymbol \Sigma }$ $A:{\mathcal U}$ $B:A\la {\mathcal U}$ ${\boldsymbol \Pi }_{{x:A}}B(x)$ ${\boldsymbol \Sigma }_{{x:A}}B(x)$

Egalitatea termenilor de același tip în teoria tipurilor de homotopie poate fi fie o egalitate „prin definiție” ( ) fie o egalitate propozițională. Egalitatea prin definiție implică egalitate propozițională, dar nu invers. În general, egalitatea propozițională a termenilor și tipului este reprezentată ca un tip nevid , care se numește tip de identitate; termenii acestui ultim tip sunt traseele vederii în spaţiu ; tipul de identitate este astfel privit ca spațiul de căi (adică mapări continue ale segmentului unității la ) de la un punct la altul . $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}$

Axioma univalenței

Teoria intuiționistă a tipurilor ne permite să definim conceptul de echivalență de tip (pentru tipurile aparținând aceluiași univers) și să construim o funcție în mod canonic de la un tip de identitate la un tip de echivalență : $A=B$ $A\simeq B$

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

Axioma univalenței , formulată de Voevodsky, afirmă că această funcție este, de asemenea, o echivalență:

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

adică tipul de identitate a două tipuri date este echivalent cu tipul de echivalență al acelor tipuri. Dacă și sunt tipuri propoziționale, axioma are un înțeles deosebit de transparent și se rezumă la ceea ce se numește uneori principiul de extensialitate al lui Church: egalitatea propozițiilor este echivalentă logic cu echivalența lor logică; utilizarea acestui principiu înseamnă că sunt luate în considerare doar valorile de adevăr ale afirmațiilor, dar nu și sensul lor. O consecință a axiomei este extensionalitatea funcțională , adică afirmația că funcțiile ale căror valori sunt egale pentru toate valorile egale ale argumentelor lor sunt egale între ele. Această proprietate a funcțiilor este importantă în informatică. $A$ $B$

Axioma este considerată de unii filozofi ai matematicii ca o formulare matematică exactă a tezei principale a filozofiei structuralismului matematic , care se bazează pe practica comună a raționamentului matematic „până la izomorfism ” sau „până la echivalență ” [ 5] .

Logica, multimi, grupoide

O propoziție ( propoziție simplă , „ propoziție goală ”) în teoria tipurilor de homotopie este definită ca un tip care este fie vid, fie conține un singur termen ; astfel de tipuri sunt numite propoziționale. Dacă tipul este gol, atunci propoziția corespunzătoare este falsă; dacă conține un termen (simbolic - ), atunci propoziția corespunzătoare este adevărată, iar termenul este considerat drept dovada sa. Astfel, teoria folosește conceptul intuiționist de adevăr, conform căruia adevărul unei afirmații este înțeles ca posibilitatea de a prezenta o demonstrație a acestei afirmații. $P$ $p$ $P$ $P$ $p$ $p:P$ $P$ $p$

Un fragment de teorie a tipurilor de homotopie, care se limitează la operații cu tipuri propoziționale, adică cu propoziții, poate fi descris ca un fragment logic (logică) al acestei teorii. Disjuncția logică din fragmentul propozițional corespunde tipului sumă , conjuncției tipului produs , implicației tipului funcțional , negației tipului , unde este tipul gol (tipul nul). Logica corespunzătoare unor astfel de construcții este o variantă a logicii intuiționiste , în special, afirmații precum legea dublei negații sau mijlocul exclus nu au loc în ea . $A\vee B$ $A+B$ $A\wedge B$ $A\ori B$ $A\Rightarrow B$ $A la B$ $\nu A$ $A\to \mathbf {0}$ ${\mathbf 0}$

Orice tip care conține doi sau mai mulți termeni diferiți poate fi pus în corespondență unu-la-unu cu un tip propozițional, care se obține prin identificarea tuturor termenilor de tip , o astfel de operație se numește trunchiere propozițională ( trunchiere propozițională ). Acest lucru face posibilă distingerea între „nivelul propozițional” (nivelul de enunț) al unei teorii și ierarhia de homotopie a nivelurilor sale nepropoziționale „superioare”. $X$ $x,y,\dots$ $X$

Nivelul propozițiilor este urmat de nivelul mulțimilor . O mulțime în teoria tipurilor de homotopie este definită ca un spațiu (tip) cu o topologie discretă . În mod echivalent, o mulțime poate fi descrisă în teorie ca un tip astfel încât, pentru oricare dintre termenii săi , tipul este o propoziție, adică fie goală (cazul când și sunt elemente diferite ale mulțimii ), fie conține un singur element (cel cazul când și sunt același element). Dupa nivelul multimilor vine nivelul grupoizilor (multimea de puncte si setul de cai dintre fiecare pereche de puncte) si nivelurile -groupoidelor de toate ordinele. $A$ $a_{1},a_{2}:A$ ${\mathsf {Id}}_{A}(a_{1},a_{2})$ $a_{1}$ $a_{2}$ $A$ $a_{1}$ $a_{2}$

Diverse interpretări ale conceptelor teoretice de tip

Biblioteci și implementări de HoTT

Bibliotecile HoTT sunt mai multe proiecte găzduite pe GitHub (în același depozit în care se află codul sursă al cărții) care creează descrieri formale ale diferitelor ramuri ale matematicii folosind sisteme automate de demonstrare folosind construcții ale teoriei tipului homotopiei.

În proiectul lui Vladimir Voevodsky, numit „Biblioteca bazelor univalente” [6] , este utilizat un subset minim sigur Coq special dezvoltat , care asigură puritatea ideologică și fiabilitatea construcțiilor în conformitate cu teoria. Proiectul HoTT [7] este condus de instrumente standard Coq, implementate ca parte a programului de cercetare al Institutului pentru Studii Avansate și, în general, urmează cartea , începând cu 2020, 48 de dezvoltatori participă la proiect, cel mai activi sunt Jason Gross, Michael Shulman, Ali Kaglayan și Andrey Bauer [8] . Există și un proiect paralel în Agda [9] .

Există mai multe sisteme experimentale de dovezi interactive bazate în întregime pe HoTT: Arend , RedPRL, redtt, cooltt, iar în versiunea Agda 2.6.0, a fost adăugat așa-numitul „mod cubic”, care permite utilizarea deplină a tipurilor de homotopie.

Note

↑ Makkai Mihaly. Logica de prim ordin cu sortări dependente, cu aplicații la teoria categoriilor (engleză) (1995). Consultat la 5 decembrie 2014. Arhivat din original la 10 octombrie 2015.
↑ Tipuri de identitate - Structură topologică și categorială . Workshop, Uppsala, 13-14 noiembrie 2006 (2006) . Data accesului: 5 decembrie 2013. Arhivat din original pe 18 decembrie 2014. (nedefinit)
↑ Teoria tipurilor de homotopie: Fundamentele univalente ale codurilor sursă ale proiectului de matematică pe GitHub
↑ HoTT, 2013 , p. iii.
↑ Steve Avodey. Structuralism, Invariance and Univalence // Philosophia Mathematica . - Oxford University Press , 2014. - V. 22 , Nr. 1 . — ISSN 0031-8019 . - doi : 10.1093/philmat/nkt030 .
↑ Proiectul Bibliotecă de bază univalentă pe GitHub
↑ Proiectul Teoria tipului Homotopy pe GitHub
↑ HoTT 20 mar 2011 — 02 octombrie 2020 Contribuții la master, excluzând comiterile de îmbinare .
↑ Proiect de bibliotecă Agda HoTT pe GitHub

Literatură

Teoria tipurilor de homotopie: fundamente univalente ale matematicii . - Princeton : Institutul pentru Studii Avansate , 2013. - 603 p.
Steve Awodey, Álvaro Pelayo, Michael A. Warren. Axioma de Univalență a lui Voevodsky în teoria tipurilor de homotopie (engleză) // Notices of the AMS . - 2013. - Vol. 60 , nr. 9 . - P. 1164-1167 .
Hannes Hummel. Vor redefini computerele rădăcinile matematicii? . Când un matematician legendar a găsit o greșeală în propria sa lucrare, el a pornit într-o căutare asistată de computer pentru a elimina eroarea umană. Pentru, el trebuie să rescrie regulile vechi de un secol care stau la baza întregii matematici . Quanta Magazine (19 mai 2015) . Preluat: 31 decembrie 2017.
Don Monroe. Un nou tip de matematică? (engleză) // Comunicări ale ACM . - 2014. - Vol. 57 , nr. 2 . - P. 13-15 . - doi : 10.1145/2557446 .
Andrei Rodin. Atomismul logic și geometric de la Leibniz la Voevodsky // Probleme de filosofie . - 2016. - Nr 6 . - S. 134-142 .

Link -uri

cs.cmu.edu/~rwh/courses/hott/ - materiale de curs despre teoria tipurilor de homotopie predate de Robert Harper la Universitatea Carnegie Mellon