Models of univalence in cubical sets

Willem Vanhulle Andreas Nuyts
Het univalentie axioma helpt bij de formalisatie en automatisatie van wiskundig redeneren. Dit wordt geïllustreerd met een voorbeeld over decimale en binaire getallen.

Automatisatie in zuivere wiskunde

Inleiding

De laatste decennia automatiseerden bedrijven productieprocessen met slimme algoritmen die vrij zijn van menselijke fouten. Ook wetenschappelijk onderzoek is onderhevig aan menselijke fouten en automatisatie kan die fouten voorkomen. In de wiskundige berekeningen die aan de basis liggen van veel wetenschappen sluipen het snelste fouten. De eerste stap naar de automatisatie van wiskunde is een getrouwe voorstelling van algemene wiskundige berekeningen in een programmeertaal.

In 2010 ontdekte de veelzijdige onderzoeker Vladimir Voevodsky deze getrouwe voorstelling in de vorm van een axioma, genaamd Univalentie Axioma (aangeduid met UA): (X ≅ Y) ≅ (X = Y). Hierin staat '≅' voor een nieuwe vorm van gelijkheid, zoals congruentie of gelijkvormigheid. De variabelen X en Y staan voor ruimten of structuren. Dit axioma verbijsterde onderzoekers door zijn eenvoud en algemeenheid, maar ook omdat het de betekenis van gelijkheid '=' herschreef. In 2012-2013 kwamen onderzoekers van over de hele wereld samen aan het bekende onderzoeksinstituut van Princeton om de toepassingen van het univalentie axioma van Vladimir Voevodsky verder te onderzoeken. In september 2017 overleed Vladimir Voevodsky, maar zijn werk werd verdergezet door andere onderzoekers.

Binaire getallen

Het nut van het univalentie axioma kan geïllustreerd worden met een simpel voorbeeld over getallen. Decimale getallen drukken getallen uit in ons dagelijks leven en bestaan uit de cijfers 0, 1 tot en met 9. Daartegenover bestaan er ook binaire getallen, getallen die opgebouwd zijn uit 0 en 1. Beide getallen hebben hun voordelen en nadelen. Binaire getallen zijn bijvoorbeeld efficiënter om numerieke berekeningen met computers uit te voeren. Twee voorbeelden van binaire getallen zijn 11101 en 1010. Deze binaire getallen zijn gelijk aan de decimale getallen 29 en 9. Zowel binaire als decimale getallen kunnen opgeteld worden: 11101 + 1010 = 29 + 9. Uit het lager onderwijs is gekend dat 29 + 9 = 9 + 29 en voor binaire getallen geldt dat  1010 + 11101 = 11101 + 1010. In het algemeen kunnen we getallen altijd omwisselen bij de optelling, een eigenschap die  'commutativiteit' genoemd wordt.

Dit is een fenomeen dat vaker gebeurt in zuivere wiskunde: twee structuren zijn verschillend, maar voldoen aan dezelfde eigenschappen. De structuren zijn in zuivere wiskunde echter veel ingewikkelder en het is niet altijd duidelijk om te zien waarom de eigenschap (commutativiteit in het voorgaande voorbeeld) bewaard blijft. Vladimir Voevodsky introduceerde twee zaken om dit probleem formeel op te lossen: een definitie van een nieuwe gelijkheid ≅ (genaamd equivalentie) en het voorgenoemde univalentie axioma. Deze laten toe automatisch bewijzen te herschrijven van eigenschappen van gelijkaardige structuren. Zo is het duidelijk dat eigenschappen bewaard blijven tussen twee gelijkaardige structuren zoals de binaire en decimale getallen.

Het nieuwe hieraan is dat dit allemaal formeel kan uitgedrukt worden in geschikte programmeertalen. Voordien was het nodig dergelijke bewijzen handmatig te herschrijven en eigenschappen te verifiëren voor gelijkaardige structuren. Nu kan dit allemaal automatisch gebeuren. Dit zorgt voor een getrouwe voorstelling van veel wiskundige redeneringen en helpt bij het voorkomen van menselijke fouten met behulp van automatisatie.

Nog veel andere nieuwe toepassingen van het univalentie axioma zijn mogelijk en worden beschreven in het boek genaamd "Univalent Foundations of Mathematics", maar zijn eerder gemotiveerd vanuit gespecialiseerde deelgebieden uit zuivere wiskunde.

Abstracte paden

Om deze toepassingen mogelijk te maken, moest nieuwe machinerie gebouwd worden door Vladimir Voevodsky (en zijn voorgangers). Deze machinerie bestaat uit een ruimtelijke of fysieke interpretatie van formele wiskundige logica met behulp van paden en vervormingen. Indien twee gelijkaardige structuren X en Y gegeven zijn en er een equivalentie van de vorm X ≅ Y is, laat het univalentie axioma toe om deze equivalentie te beschouwen als een pad. Aan de eindpunten van dit pad bevinden zich de structuren X en Y.

Voorstelling van het abstracte pad

Bewijzen van een eigenschap P voor de ene structuur kunnen overheen het pad verplaatst worden. Dit betekent dat indien een bewijs (aangeduid met P X) helemaal uitgeschreven is voor de ene structuur, er  automatisch een bewijs voor dezelfde eigenschap de andere structuur (aangeduid met P Y) afgeleid kan worden.

Kubussen

Tot 2018 ontbrak het  mechanisme om dit abstracte pad te bouwen en de verplaatsing van bewijzen uit te voeren. Dit werd opgelost door Cohen et al. met abstracte n-dimensionale kubussen. Deze theorie kon paden bouwen tussen de structuren door de verschillende structuren als het ware aan elkaar te lijmen met een nieuw object genaamd 'Glue'. Dit mechanisme werd de voorbije jaren geperfectioneerd in een computerprogramma genaamd Agda Cubical.

In mijn thesis heb ik dit mechanisme bestudeerd en uitgetest op een eenvoudige algebraïsche structuur. Daaruit blijkt dat de introductie van 'Glue' helpt om bewijzen te automatiseren, maar wel dat de ingewikkelde definitie van dit object extra moeilijkheden introduceert. De efficiëntie van de implementatie in Agda Cubical was bijvoorbeeld nog niet optimaal. Verder onderzoek zal moeten uitwijzen of het gebruikt kan worden door wiskundigen voor hun dagelijks onderzoek, bijvoorbeeld om nieuwe ingewikkelde stellingen te bewijzen.

Bibliografie

Pagina 81 tot 90 in scriptiebestand. Het was niet mogelijk om een HTML-versie hiervan te genereren.

Universiteit of Hogeschool
Zuiver wiskunde
Publicatiejaar
2019
Promotor(en)
Dominique Devriese
Kernwoorden
Share this on: