Automating Boundary Filling in Cubical Type Theories

Technische Samenvatting: Automatisering van Boundary Filling in Cubical Type Theories

Probleemstelling
In Cubical Type Theory (CTT) vereist het redeneren over hogere-dimensionale structuren (zoals topologische ruimten via Higher Inductive Types en Univalence) het construeren van "kubussen" met gespecificeerde randen (boundaries). Dit proces, bekend als boundary filling, omvat twee primaire mechanismen: contortion (het herparametriseren van een cel om in een rand te passen) en Kan filling (het construeren van een cel door meerdere kubussen aan elkaar te plakken om een open doos te vullen). Hoewel contortion een vorm van equatoriale redenering is, vertegenwoordigt Kan filling een hogere-dimensionale generalisatie van dergelijke redenering.

De centrale uitdaging is dat het handmatig construeren van deze kubussen tijdrovend en foutgevoelig is, vooral naarmate de dimensionaliteit toeneemt. Bovendien is het algemene probleem van het vinden van Kan fillers onbeslisbaar, en zelfs het beperkte probleem van het vinden van optimale contortions voor expressieve theorieën (zoals Dedekind en De Morgan) lijdt onder combinatorische explosie (bijv. het aantal Dedekind contortions groeit volgens de Dedekind-getallen, die extreem groot zijn). Het artikel beoogt een algoritmische aanpak te ontwikkelen om deze boundary-filling taken te automatiseren voor routinematige bewijsdoelen in CTT.

Methodologie
De auteurs ontwikkelen een vereenvoudigde, algemene cubische taal geparametriseerd door een "contortion theory" (de klasse van toegestane herparametrisaties). Zij isoleren twee afzonderlijke automatiseringsproblemen: Contortion Solving en Kan Solving.

1. Contortion Solving:

   • Theoretische Fundering: De auteurs mappen Dedekind en De Morgan contortions naar poset maps (specifiek, monotone functies tussen eindige machten van de poset $I = \{0 < 1\}$). Dit maakt gebruik van de Birkhoff-dualiteit tussen eindige distributieve lattices en eindige posets.
   • Representatie: Om de exponentiële groei van de zoekruimte te beheersen, introduceren zij Potential Poset Maps (PPMs). Een PPM is een afbeelding van een domein-poset naar de machtsverzameling van een codomein-poset, wat een collectie geldige contortions simultaan representeert. Dit maakt een ruimte-efficiënte representatie mogelijk die exponentieel groeit met de dimensie in plaats van super-exponentieel (zoals bij ruwe enumeratie).
   • Algoritme: Zij stellen een algoritme voor (Algoritme 1) dat iteratief een PPM beperkt op basis van de restricties opgelegd door de doelrand-vlakken (target boundary faces). Door restricties te ordenen op dimensionaliteit en restricties te propageren, wordt de zoekruimte aanzienlijk gepruned voordat een definitieve brute-force controle wordt uitgevoerd op de resterende kandidaten.

2. Kan Solving:

   • Constraint Satisfaction: De zoektocht naar Kan fillers (specifiek hogere-dimensionale fillers) wordt geformuleerd als een Constraint Satisfaction Problem (CSP). De variabelen in de CSP representeren de onbekende vlakken van de open doos, en de domeinen bestaan uit geldige contortions (vertegenwoordigd via PPMs voor efficiëntie).
   • Heuristische Zoektocht: Omdat de zoekruimte oneindig is (door de mogelijkheid van geneste fillers), gebruiken de auteurs een breadth-first search strategie met iteratieve verdieping (Algoritme 2 en 3). De solver geeft prioriteit aan "natuurlijke fillers" (waar een rand-vlak al een filler is) en eenvoudige contortions. Alleen wanneer deze falen, construeert het hogere-dimensionale open dozen, waarbij recursief wordt gezocht naar hun ontbrekende vlakken.
   • Theory Parameterization: De solver is ontworpen om agnostisch te zijn aan de onderliggende contortion theory, waardoor het kan schakelen tussen Cartesian, Disjunctive, Dedekind en De Morgan theorieën afhankelijk van de complexiteit van het probleem.

Belangrijkste Bijdragen

• Algemeen Framework: Formulering van een algemene cubische taal geparametriseerd door contortion theories, die diverse bestaande systemen (Cartesian, CCHM, etc.) verenigt.
• Complexiteitsanalyse:
  • Bewezen dat Kan filling onbeslisbaar is door het woordprobleem voor eindig gepresenteerde groepen te reduceren tot het Kan solving probleem.
  • Vastgesteld dat Dedekind en De Morgan contortion solving NP-compleet zijn (en coNP-hard voor entailment), wat de onhaalbaarheid van brute-force benaderingen voor expressieve theorieën benadrukt.
• Efficiënte Algoritmen:
  • Ontwikkelde een PPM-gebaseerd algoritme voor het oplossen van Dedekind en De Morgan contortion problemen, wat de zoekruimte drastisch verkleint vergeleken met naïeve enumeratie.
  • Ontwikkelde een CSP-gebaseerde solver voor Kan filling die contortion solving als een sub-routine integreert.
• Implementatie: Biedt een praktische Haskell-implementatie van deze algoritmen, in staat om boundary problemen uit de agda/cubical en 1lab bibliotheken op te lossen.

Resultaten
De auteurs evalueerden hun solver op een benchmark-suite van boundary problemen, waaronder:

• Associativiteit van Path Concatenation: Opgelost met De Morgan contortions waarbij pad-reversal betrokken is.
• Het Eckmann-Hilton Argument: De solver slaagde erin de noodzakelijke 3-cube en 4-cube fillers te construeren om te bewijzen dat 2-loop concatenatie commutatief is. Dit werd bereikt in ongeveer 150ms voor de cube constructie en 15ms voor de geassocieerde compositie-lemma.
• Prestaties: Op een standaard laptop werden routinematige bewijsverplichtingen (bijv. het herordenen van cube zijden) opgelost in minder dan 50ms. De solver kon complexe, meerstaps-bewijzen aan die handmatig lastig te construeren zouden zijn.

Betekenis en Claims
Het artikel claimt een van de eerste systematische studies van geautomatiseerd redeneren specifiek voor Cubical Type Theory te presenteren. De betekenis ligt in:

1. Overbruggen van de Kloof: Het adresseert de "cubical puzzles" die vaak voorkomen als routinematige lemma's in de synthetische homotopietheorie, die momenteel moeilijk te voorzien en te enumereren zijn in standaardbibliotheken.
2. Omgaan met Complexiteit: Door gebruik te maken van poset maps en CSP's, demonstreren de auteurs dat zelfs theoretisch moeilijke problemen (zoals Dedekind/De Morgan contortion solving) hanteerbaar kunnen worden gemaakt voor praktische voorbeelden door middel van heuristische zoektochten en efficiënte representatie.
3. Praktisch Nut: De implementatie dient als een proof-of-concept dat automatisering de bewijslast in Cubical Agda aanzienlijk kan verminderen, potentieel werkend als een tactic voor het afhandelen van routinematige doelen.

De auteurs blijven bescheiden over de huidige beperkingen en merken op dat de solver nog niet alle complexe doelen (bijv. de 7-dimensionale square-to-cube analogue of de syllepsis) binnen een redelijke tijd kan oplossen en dat de zoekruimte voor hogere-dimensionale paden nog steeds enorm is. Zij presenteren dit werk als een fundament voor verder onderzoek en toekomstige integratie in theorem provers.