Teorie typu homotopy - Homotopy type theory

Cover of Homotopy Type Theory: Univalent Foundations of Mathematics .

V matematické logice a informatice se homotopická teorie typů ( HoTT / h ɒ t / ) vztahuje k různým vývojovým liniím intuicionistické teorie typů , založené na interpretaci typů jako objektů, na které se vztahuje intuice (abstraktní) teorie homotopie .

To mimo jiné zahrnuje konstrukci homotopických modelů a modelů s vyššími kategoriemi pro takové typové teorie; použití teorie typů jako logiky (nebo vnitřního jazyka ) pro abstraktní homotopickou teorii a teorii vyšších kategorií ; rozvoj matematiky v rámci teoreticko-teoretických základů (včetně dříve existující a nové matematiky, kterou umožňují homotopické typy); a formalizace každého z nich v počítačově ověřených asistentech .

Mezi prací označovanou jako teorie typu homotopy a projektem univalentních základů existuje velké překrývání . Ačkoli ani jeden není přesně vymezen a termíny jsou někdy používány zaměnitelně, volba použití také někdy odpovídá rozdílům v pohledu a důrazu. Tento článek jako takový nemusí představovat názory všech výzkumníků v těchto oblastech stejně. Tento druh variability je nevyhnutelný, když je pole v rychlém toku.

Dějiny

Pravěk: grupoidní model

Svého času představa, že typy v teorii intenzivních typů s jejich typy identit lze považovat za groupoidy, byl matematický folklor . Poprvé byl sémanticky precizně zpracován v dokumentu Martina Hofmanna a Thomase Streichera z roku 1998 s názvem „The groupoid translation of type theory“, ve kterém ukázali, že teorie intenzionálních typů má model v kategorii grupoidů . Jednalo se o první skutečně „ homotopický “ model teorie typů, byť pouze „1- dimenzionální “ (tradiční modely v kategorii množin, které jsou homotopicky 0-dimenzionální).

Jejich příspěvek také předznamenal několik pozdějších vývojů v teorii typu homotopy. Například poznamenali, že model grupoidu splňuje pravidlo, které nazvali „extenzionalita vesmíru“, což není nic jiného než omezení na 1 typy axiomu univalence, které o deset let později navrhl Vladimír Voevodský . (Axiom pro 1 typy je však formulován výrazně jednodušeji, protože není vyžadován soudržný pojem „ekvivalence“.) Rovněž definovali „kategorie s izomorfismem jako rovnost“ a domnívali se, že v modelu využívajícím vyšší dimenzionální grupoidy, u takových kategorií by člověk měl „ekvivalence je rovnost“; to později dokázali Benedikt Ahrens, Krzysztof Kapulkin a Michael Shulman .

Raná historie: kategorie modelů a vyšší groupoidy

První vyšší dimenzionální modely teorie intenzivních typů zkonstruovali Steve Awodey a jeho žák Michael Warren v roce 2005 s využitím modelových kategorií Quillen . Tyto výsledky byly poprvé veřejně prezentovány na konferenci FMCS 2006, na které Warren promluvil s názvem „Homotopické modely teorie intenzivního typu“, který také sloužil jako prospekt jeho diplomové práce (přítomnými disertační komisí byli Awodey, Nicola Gambino a Alex Simpson). Shrnutí je obsaženo v abstraktu prospektu Warrenovy práce.

Na následném workshopu o typech identity na univerzitě v Uppsale v roce 2006 proběhla dvě diskuse o vztahu mezi teorií intenzionálních typů a faktorizačními systémy: jedna od Richarda Garnera, „Faktorizační systémy pro teorii typů“ a jedna od Michaela Warrena, „Modelové kategorie a typy intenzivní identity “. O souvisejících myšlenkách hovořili v rozhovorech Steve Awodey, „Teorie typů vyšších dimenzionálních kategorií“, a Thomas Streicher , „Typy identity vs. slabé omega-grupoidy: některé myšlenky, některé problémy“. Na stejné konferenci vystoupil Benno van den Berg s proslovem „Typy jako slabé omega kategorie“, kde nastínil myšlenky, které se později staly předmětem společného příspěvku s Richardem Garnerem.

Všechny rané konstrukce vícerozměrných modelů se musely vypořádat s problémem koherence typickým pro modely teorie závislých typů a byla vyvinuta různá řešení. Jeden takový dal v roce 2009 Voevodsky, další v roce 2010 van den Berg a Garner. Obecné řešení, založené na Voevodského konstrukci, nakonec poskytli Lumsdaine a Warren v roce 2014.

Na PSSL86 v roce 2007 Awodey promluvil s názvem „Teorie typu homotopy“ (toto bylo první veřejné použití tohoto výrazu, který vytvořil Awodey). Awodey a Warren shrnuli své výsledky v příspěvku „Homotopy theoretic models of identity types“, který byl zveřejněn na serveru ArXiv preprint v roce 2007 a publikován v roce 2009; podrobnější verze se v roce 2008 objevila ve Warrenově práci „Homotopy teoretické aspekty teorie konstruktivního typu“.

Přibližně ve stejnou dobu Vladimir Voevodsky nezávisle zkoumal teorii typů v kontextu hledání jazyka pro praktickou formalizaci matematiky. V září 2006 zaslal na seznam typů „Velmi krátká poznámka k lambda kalkulu homotopy “, který načrtl obrysy teorie typů se závislými součiny, součty a vesmíry a modelu této teorie typů v Kanových zjednodušovacích sadách . Začalo to slovy „Homotopický λ-kalkul je hypotetický (v tuto chvíli) typový systém“ a skončilo to „V tuto chvíli je hodně z toho, co jsem řekl výše, na úrovni dohadů. Dokonce i definice modelu TS v kategorie homotopy je netriviální “s odkazem na složité problémy s koherencí, které nebyly vyřešeny do roku 2009. Tato poznámka obsahovala syntaktickou definici„ typů rovnosti “, o nichž se tvrdilo, že jsou v modelu interpretovány mezerami cest, ale nezohledňovaly Pravidla Per Martin-Löf pro typy identit. Kromě velikosti také stratifikovalo vesmíry podle homotopické dimenze, což byla myšlenka, která byla později většinou vyřazena.

Na syntaktické stránce Benno van den Berg v roce 2006 usoudil, že věž typů identit typu v teorii intenzivního typu by měla mít strukturu ω-kategorie, a skutečně ω-groupoid, v „globulárním, algebraickém“ smyslu Michaela Batanina. To později nezávisle prokázali van den Berg a Garner v příspěvku „Typy jsou slabé omega-groupoidy“ (publikováno v roce 2008) a Peter Lumsdaine v příspěvku „Slabé ω-kategorie z teorie intenzivních typů“ (publikován v roce 2009) a jako část jeho 2010 Ph.D. práce „Vyšší kategorie z teorií typů“.

Axiom univalence, teorie syntetické homotopy a vyšší induktivní typy

Koncept univalentní fibrace zavedl Voevodsky počátkem roku 2006. Avšak vzhledem k naléhání všech prezentací teorie typu Martin-Löf na vlastnost, že typy identity mohou v prázdném kontextu obsahovat pouze reflexivitu, udělal Voevodsky až do roku 2009 nerozpozná, že tyto typy identity lze použít v kombinaci s univalentními vesmíry. Zejména myšlenka, že univalence může být zavedena jednoduše přidáním axiomu ke stávající teorii typu Martin-Löf, se objevila až v roce 2009.

Také v roce 2009 Voevodsky vypracoval více podrobností modelu teorie typů v komplexech Kan a zjistil, že existenci univerzální kanalizace lze použít k vyřešení problémů s koherencí pro kategorické modely teorie typů. Pomocí myšlenky AK Bousfielda také dokázal, že tato univerzální fibrace je univalentní: související fibrace párových homotopických ekvivalentů mezi vlákny je ekvivalentní fibraci cest a prostoru báze.

Aby Voevodsky zformuloval univalenci jako axiom, našel způsob, jak syntakticky definovat „ekvivalence“, které měly důležitou vlastnost, že typ představující tvrzení „f je ekvivalence“ byl (za předpokladu extenze funkce) (-1) zkrácen (tj. stahovatelný, pokud je obýván). To mu umožnilo předložit syntaktické vyjádření univalence, zobecňující „Hofmannovu a Streicherovu„ univerzálnost “do vyšších dimenzí. Dokázal také použít tyto definice ekvivalencí a stahovatelnosti k zahájení vývoje významného množství „teorie syntetické homotopie“ v asistentu důkazu Coq ; toto tvořilo základ knihovny později nazvané „Foundations“ a nakonec „UniMath“.

Sjednocení různých vláken začalo v únoru 2010 neformálním setkáním na univerzitě Carnegie Mellon , kde Voevodsky představil svůj model v komplexech Kan a svůj kód Coq skupině zahrnující Awodey, Warren, Lumsdaine a Robert Harper , Dan Licata, Michael Shulman , a další. Toto setkání přineslo obrysy důkazu (Warrena, Lumsdaina, Licaty a Shulmana), že každá homotopická ekvivalence je ekvivalencí (v dobrém koherentním smyslu Voevodského), založeného na myšlence z teorie kategorií vylepšování ekvivalencí na ekvivalence adjoint. Brzy poté Voevodsky dokázal, že axiom univalence implikuje prodloužení funkce.

Další stěžejní událostí byl mini workshop v Matematickém výzkumném ústavu Oberwolfach v březnu 2011, který pořádali Steve Awodey, Richard Garner, Per Martin-Löf a Vladimir Voevodsky s názvem „Interpretace homotopie konstruktivní teorie typů“. Jako součást Coq tutoriálu pro tento workshop napsal Andrej Bauer malou knihovnu Coq na základě Voevodského myšlenek (ale ve skutečnosti nepoužívá žádný z jeho kódů); toto se nakonec stalo jádrem první verze knihovny „HoTT“ Coq (první odevzdání druhé od Michaela Shulmana poznamenává „Vývoj založený na souborech Andreje Bauera, s mnoha nápady převzatými ze souborů Vladimíra Voevodského“). Jedna z nejdůležitějších věcí, která měla vyjít ze setkání Oberwolfach, byla základní myšlenka vyšších induktivních typů, kvůli Lumsdaineovi, Shulmanovi, Bauerovi a Warrenovi. Účastníci také zformulovali seznam důležitých otevřených otázek, například zda univalenční axiom splňuje kanoničnost (stále otevřený, i když některé speciální případy byly vyřešeny pozitivně), zda axival univalence má nestandardní modely (protože Shulman odpověděl kladně) a jak definovat (polo) zjednodušující typy (v MLTT stále otevřené, i když to lze provést ve Voevodského Homotopy Type System (HTS), teorii typů se dvěma typy rovnosti).

Brzy po workshopu Oberwolfach byla založena webová stránka a blog Homotopy Type Teory a toto téma se začalo popularizovat pod tímto názvem. Názor na některý z důležitých pokroků v tomto období lze získat z historie blogu.

Univalentní základy

Fráze „univalentní základy“ všichni souhlasí s tím, že úzce souvisí s teorií typu homotopy, ale ne každý ji používá stejným způsobem. To bylo původně používáno Vladimir Voevodsky se odkazovat na jeho vizi foundational systému pro matematiku, ve kterém jsou základní objekty homotopické typy, založené na teorii typů splňující univalenční axiom, a formalizované v počítačově korektním asistentovi.

Jak se Voevodského práce začleňovaly do komunity dalších výzkumníků pracujících na teorii typu homotopy, „univalentní základy“ se někdy zaměňovaly s „teorií typu homotopy“ a jindy se odkazovalo pouze na jeho použití jako základního systému (vyjma například , studium modelové kategorické sémantiky nebo výpočetní metateorie). Například předmět zvláštního roku IAS byl oficiálně uveden jako „univalentní základy“, ačkoli mnoho práce, které zde bylo provedeno, se kromě základů zaměřilo na sémantiku a metateorii. Kniha vytvořená účastníky programu IAS měla název „Teorie typu Homotopy: Univalentní základy matematiky“; i když by to mohlo odkazovat na obě použití, protože kniha pojednává pouze o HoTT jako o matematickém základu.

Zvláštní rok na univalentních základech matematiky

Přehrávejte média

Animace ukazující vývoj knihy HoTT v úložišti GitHub účastníky projektu Special Year of Univalent Foundations.

V letech 2012–13 uspořádali vědci z Institutu pro pokročilé studium „Zvláštní rok na univalentních základech matematiky“. Zvláštní rok spojil vědce z topologie , informatiky , teorie kategorií a matematické logiky . Program organizovali Steve Awodey , Thierry Coquand a Vladimir Voevodsky .

Během programu Peter Aczel , který byl jedním z účastníků, zahájil pracovní skupinu, která zkoumala, jak dělat teorii typů neformálně, ale důsledně, stylem, který je analogický běžným matematikům, kteří dělají teorii množin. Po počátečních experimentech vyšlo najevo, že to není jen možné, ale také velmi přínosné, a že by mohla a měla být napsána kniha (tzv. HoTT Book ). Mnoho dalších účastníků projektu se poté připojilo k úsilí s technickou podporou, psaním, korekturou a nabídkou nápadů. Neobvykle pro text matematiky, to byl vyvinut spolupracovat a pod širým nebem na GitHub , je uvolněn pod licencí Creative Commons , která umožňuje lidem vyklopit svou vlastní verzi knihy, a to jak prodejný v tisku a ke stažení zdarma.

Obecněji řečeno, zvláštní rok byl katalyzátorem rozvoje celého tématu; kniha HoTT byla pouze jedním, i když nejviditelnějším výsledkem.

Oficiální účastníci zvláštního roku

ACM Computing Reviews uvedlo knihu jako pozoruhodnou publikaci z roku 2013 v kategorii „matematika výpočetní techniky“.

Klíčové koncepty

Teorie intenzivního typu	Homotopická teorie
typy ${\ displaystyle A}$	mezery ${\ displaystyle A}$
podmínky ${\ displaystyle a}$	body ${\ displaystyle a}$
${\ displaystyle a: A}$	${\ displaystyle a \ v A}$
závislý typ ${\ Displaystyle x: A \ \ vdash \ B (x) \}$	fibrace ${\ displaystyle B \ až A}$
typ identity ${\ displaystyle \ mathrm {Id} _ {A} (a, b)}$	prostor cesty
${\ displaystyle p: \ mathrm {Id} _ {A} (a, b)}$	cesta ${\ displaystyle p: a \ to b}$
${\ Displaystyle \ alpha: \ mathrm {Id} _ {\ mathrm {Id} _ {A} (a, b)} (p, q)}$	homotopy ${\ Displaystyle \ alpha: p \ Rightarrow q}$

„Propozice jako typy“

HoTT používá upravenou verzi interpretace teorie typů „ propozice jako typy “, podle níž typy mohou také představovat propozice a termíny pak mohou představovat důkazy. V HoTT však, na rozdíl od standardních „propozic jako typů“, hrají zvláštní roli 'pouhé propozice', což jsou zhruba ty typy, které mají nejvýše jeden termín, až do rovnosti výroků . Jedná se spíše o konvenční logické věty než o obecné typy v tom, že jsou důkazně irelevantní.

Rovnost

Základním konceptem teorie typu homotopy je cesta . V HoTT je typ typem všech cest od bodu k bodu . (Proto důkaz, že bod se rovná bodu, je totéž jako cesta z bodu do bodu .) Pro jakýkoli bod existuje cesta typu , která odpovídá reflexivní vlastnosti rovnosti. Cestu typu lze převrátit a vytvořit cestu typu odpovídající symetrické vlastnosti rovnosti. Dvě cesty typu resp. lze zřetězit a vytvořit cestu typu ; to odpovídá tranzitivní vlastnosti rovnosti. ${\ displaystyle a = b}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a}$${\ displaystyle a = a}$${\ displaystyle a = b}$${\ displaystyle b = a}$${\ displaystyle a = b}$${\ displaystyle b = c}$${\ displaystyle a = c}$

A co je nejdůležitější, vzhledem k cestě a dokladu o nějakém majetku lze důkaz „přepravit“ po cestě a získat tak důkaz o majetku . (Ekvivalentně řečeno, objekt typu může být přeměněn na objekt typu .) To odpovídá substituční vlastnosti rovnosti . Zde přichází důležitý rozdíl mezi HoTT a klasickou matematikou. V klasické matematice, jakmile byla stanovena rovnost dvou hodnot a byla stanovena, a může být poté použito zaměnitelně, bez ohledu na jakýkoli rozdíl mezi nimi. V teorii typu homotopy však může existovat více různých cest a transport objektu po dvou různých cestách přinese dva různé výsledky. Proto je v teorii typu homotopy při aplikaci vlastnosti substituce nutné uvést, která cesta se používá. ${\ displaystyle p: a = b}$${\ displaystyle P (a)}$${\ displaystyle p}$${\ displaystyle P (b)}$${\ displaystyle P (a)}$${\ displaystyle P (b)}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a}$${\ displaystyle b}$${\ displaystyle a = b}$

Obecně může mít „návrh“ několik různých důkazů. (Například typ všech přirozených čísel, když je považován za tvrzení, má jako důkaz každé přirozené číslo.) I když má tvrzení pouze jeden důkaz , prostor cest může být nějakým způsobem netriviální. „Pouhý návrh“ je jakýkoli typ, který je buď prázdný, nebo obsahuje pouze jeden bod s triviálním prostorem cesty . ${\ displaystyle a}$${\ displaystyle a = a}$

Všimněte si, že lidé píší o , čímž ponechává druh a implicitní. Nezaměňujte to s , označující funkci identity na . ${\ displaystyle a = b}$${\ displaystyle Id_ {A} (a, b)}$${\ displaystyle A}$${\ displaystyle a, b}$${\ displaystyle id_ {A}: A \ to A}$${\ displaystyle A}$

Ekvivalence typu

Dva typy a náležející k nějakému vesmíru jsou definovány jako ekvivalentní, pokud mezi nimi existuje rovnocennost . Ekvivalence je funkce ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle U}$

${\ displaystyle f: A \ to B}$

který má levou i pravou inverzi v tom smyslu, že pro vhodně zvolené a oba typy jsou obývané: ${\ displaystyle g}$${\ Displaystyle h}$

${\ displaystyle Id_ {B \ rightarrow B} (f \ circ g, id_ {B}),}$

${\ Displaystyle Id_ {A \ rightarrow A} (h \ circ f, id_ {A}).}$

tj

${\ Displaystyle f \ circ g = _ {B \ rightarrow B} id_ {B},}$

${\ Displaystyle h \ circ f = _ {A \ rightarrow A} id_ {A}.}$

To vyjadřuje obecný pojem „ má levou i pravou inverzi“ pomocí typů rovnosti. Všimněte si, že výše uvedené podmínky invertibility jsou typy rovnosti v typech funkcí a . Obecně se předpokládá axiom extenze funkce, který zajišťuje, že jsou ekvivalentní následujícím typům, které vyjadřují invertibilitu pomocí rovnosti na doméně a doméně a : ${\ displaystyle f}$${\ displaystyle A \ rightarrow A}$${\ Displaystyle B \ rightarrow B}$${\ displaystyle A}$${\ displaystyle B}$

${\ Displaystyle \ Pi _ {y: B}. \ Id_ {B} ((f \ circ g) (y), id_ {B} (y)),}$

${\ Displaystyle \ Pi _ {x: A}. \ Id_ {A} ((h \ circ f) (x), id_ {A} (x)).}$

tedy pro všechny a , ${\ displaystyle x: A}$${\ displaystyle y: B}$

${\ Displaystyle f (g (y)) = _ {B} y,}$

${\ Displaystyle h (f (x)) = _ {A} x.}$

Funkce typu

${\ displaystyle A \ to B}$

spolu s důkazem, že jde o ekvivalence, jsou označeny

${\ Displaystyle A \ simeq B}$.

Axiom univalence

S definovanými funkcemi, které jsou ekvivalenty výše, lze ukázat, že existuje kanonický způsob, jak obracet cesty k ekvivalencím. Jinými slovy, existuje funkce typu

${\ Displaystyle (A = B) \ to (A \ simeq B),}$

což vyjadřuje, že typy, které jsou si rovny, jsou zejména rovněž ekvivalentní. ${\ displaystyle A, B}$

Univalence axiom uvádí, že tato funkce je sám ekvivalence. Proto máme

${\ Displaystyle (A = B) \ simeq (A \ simeq B)}$

„Jinými slovy, identita je ekvivalentní ekvivalenci. Zejména lze říci, že„ ekvivalentní typy jsou totožné “.“

Aplikace

Dokazování věty

HoTT umožňuje matematické důkazy překládat do počítačového programovacího jazyka asistentům počítačového korektury mnohem snadněji než dříve. Tento přístup nabízí počítačům možnost kontroly obtížných důkazů.

Jedním z cílů matematiky je formulovat axiomy, ze kterých lze odvodit a jednoznačně dokázat prakticky všechny matematické věty. Správné důkazy v matematice musí dodržovat pravidla logiky. Musí být derivovatelné bez chyby z axiomů a již prokázaných tvrzení.

HoTT přidává axiom univalence, který spojuje rovnost logicko-matematických tvrzení s teorií homotopy. Rovnice jako „a = b“ je matematický návrh, ve kterém mají dva různé symboly stejnou hodnotu. V teorii typu homotopy to znamená, že dva tvary, které představují hodnoty symbolů, jsou topologicky ekvivalentní.

Tyto topologické ekvivalenční vztahy, tvrdí ředitel Institutu teoretických studií ETH v Curychu Giovanni Felder , lze lépe formulovat v teorii homotopy, protože je komplexnější: Teorie homotopy vysvětluje nejen proč „a rovná se b“, ale také to, jak to odvodit. V teorii množin by tyto informace musely být definovány dodatečně, což ztěžuje překlad matematických výroků do programovacích jazyků.

Programování

Od roku 2015 probíhala intenzivní výzkumná práce na modelování a formální analýze výpočetního chování axivalu univalence v teorii homotopického typu.

Teorie kubického typu je jedním pokusem poskytnout výpočetní obsah teorii typu homotopy.

Předpokládá se však, že určité objekty, jako jsou částečně zjednodušené typy, nelze konstruovat bez odkazu na určitou představu přesné rovnosti. Proto byly vyvinuty různé dvouúrovňové teorie typů, které rozdělují jejich typy na vláknité typy, které respektují cesty, a nevláknité typy, které ne. Kartézská kubická teorie výpočetních typů je první dvouúrovňovou teorií typů, která poskytuje úplnou výpočetní interpretaci teorii typů homotopy.

Viz také

• Kalkul staveb
• Korespondence Curry -Howard
• Intuicionalistická teorie typů
• Homotopy hypotéza
• Univalentní základy

Reference

Bibliografie

Další čtení

• David Corfield (2020), Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy , Oxford University Press.

externí odkazy

• Teorie typu homotopy
• Teorie typů homotopy v nLab
• Homotopy type theory wiki
• Web Vladimíra Voevodského o univalentních základech
• Teorie homotopických typů a univalentní základy matematiky od Steva Awodeye
• „Teorie konstruktivního typu a homotopie“ - Video přednáška Steva Awodeyho z Institutu pro pokročilé studium

Knihovny formalizované matematiky