Konstruksjoner i grafteori i homotopitypeteori
Jonathan Prieto-Cubides disputerer 13.12.2024 for ph.d.-graden ved Universitetet i Bergen med avhandlingen "Investigations into Graph-theoretical Constructions in Homotopy Type Theory".
Hovedinnhold
Jonathan Prieto-Cubides' avhandling utforsker emner innen grafteori gjennom linsen av homotopitypeteori (HoTT), et fremvoksende felt i skjæringspunktet mellom høyere algebra, logikk og informatikk med anvendelser i formaliserings av matematikk. Avhandlingen fokuserer på univalent kombinatorikk, og presenterer spesielt en ny typeteoretisk karakterisering av planare kart og relaterte grafteoretiske konstruksjoner. Dette arbeidet kan være av interesse for forskere innen typeteori og formalisering av matematikk, da det finnes få arbeider innen kombinatorikk i denne settingen, og utforsker spørsmål som: Hvordan kan grafer defineres i homotopitypeteori? Hvordan kan kombinatoriske kart karakteriseres strukturelt i stedet for som konkrete konstruksjoner? Hva er de grunnleggende betingelsene for planheten til grafer? Kan vi demonstrere Eulers formel for planare grafer? Og hvordan relaterer den geometriske realiseringen av en graf seg til dens underliggende kombinatoriske struktur?
Hvorfor HoTT egentlig? Mens klassisk matematikk bygger på begrepet mengder, er HoTT grunnlagt på det mer fundamentale konseptet typer - analogt med datatypene kjent for dataprogrammerere som Bool eller Int. Dette rammeverket gir en elegant måte å uttrykke matematiske konstruksjoner på et mer vennlig språk for datamaskiner slik at vi kan verifisere bevis mekanisk. I Jonathan's arbeid er flere av resulatene verifisert i Agda, et avhengig typet programmeringsspråk.
Denne beregningsbaserte tilnærmingen til matematikk lar oss se klassiske resultater fra en helt ny vinkel og oppdage nye muligheter for nye konstruksjoner og bevis.
Personalia
Jonathan Prieto-Cubides (født i Colombia) fullførte en mastergrad i logikk og algoritmer ved EAFIT University. Han er stipendiat ved Institutt for informatikk ved Universitetet i Bergen, veiledet av Håkon Gylterud og Marc Bezem. For tiden jobber han som forskningsingeniør for Anoma Foundation, hvor han arbeidet med kompilatoren for det funksjonelle programmeringsspråket Juvix og, mer nylig, med spesifikasjonen av Anoma-protokollen.