💻 computer science

Rzk: a Proof Assistant for Synthetic $\infty$ -Categories

Dit artikel introduceert Rzk, een praktische bewijsassistent die een verfijnde, computationele variant van de simpliciale typetheorie van Riehl en Shulman implementeert om synthetisch redeneren over $\infty$ -categorieën mogelijk te maken, terwijl het de getrouwheid en conservativiteit ervan ten opzichte van de oorspronkelijke theorie vaststelt en een tutorial over het gebruik en de implementatie ervan biedt.

Oorspronkelijke auteurs: Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

Gepubliceerd 2026-07-15

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Nikolai Kudasov, Violetta Sim, Benedikt Ahrens

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je de wereld van de wiskunde voor als een gigantische, oneindige speeltuin. Lange tijd was het populairste spel hier Homotopy Type Theory (HoTT). In dit spel zijn alle objecten gemaakt van "vormen" die perfect flexibel zijn. Als je een pad hebt van punt A naar punt B, kun je dat pad altijd achteruit bewandelen. Het is als een wereld van elastische banden waarbij elke rek weer terug kan naar de oorspronkelijke staat. Dit is geweldig voor het bestuderen van "ruimtes" (wiskundige objecten waar alles omkeerbaar is), maar het is een beetje te perfect voor de rommelige, echte wereld van categorieën waar sommige paden eenrichtingsverkeer zijn.

Maak kennis met Rzk, een nieuwe proof assistant gebouwd door Nikolai Kudasov, Violetta Sim en Benedikt Ahrens. Zie Rzk als een gespecialiseerde constructieset ontworpen om gerichte vormen te bouwen. In deze nieuwe speeltuin kun je een pad hebben van A naar B dat niet achteruit bewandelbaar is. Het is alsof je bouwt met LEGO-steentjes waarbij sommige verbindingen permanent zijn: je kunt een stuk erop klikken, maar je kunt het niet meer losklikken zonder het model te breken. Dit stelt wiskundigen in staat om te redeneren over $\infty$ -categorieën, complexe structuren waarbij pijlen (morfismen) een richting hebben en niet altijd omkeerbaar zijn.

Het Grote Idee: Een Nieuwe Manier om te Bouwen

Het artikel introduceert Rzk als een hulpmiddel dat een specifieke theorie implementeert genaamd Simplicial Type Theory (RSTT), oorspronkelijk voorgesteld door Emily Riehl en Michael Shulman.

Hier is de slimme truc die Rzk gebruikt:
In de oorspronkelijke theorie (RSTT) was er een speciale "magische doos" genaamd een extension type. Deze doos liet je een functie definiDeferen die op een specifieke manier zich gedraagt op de randen van een vorm (zoals een driehoek) en in het midden doet wat hij wil. Het was krachtig, maar een beetje als een zwarte doos; de regels voor hoe het werkte, waren soms verborgen in de kleine lettertjes.

Rzk neemt deze magische doos en opent hem open.

De Vorm: Het scheidt het "vorm"-gedeelte (de driehoek of het interval) van het "rand"-gedeelte (de regels voor de zijden).
De Regels: Het introduceert een nieuwe, expliciete regel genaamd coercion-free subtyping. Stel je voor dat je een speelgoedauto hebt die in een kleine doos past. In het oude systeem zou het systeem simpelweg aannemen dat de auto in een grotere doos past zonder het te controleren. In Rzk controleert het systeem expliciet of de auto past, maar het dwingt je niet om de auto in extra verpakking te wikkelen (een "coercion") om hem te laten passen. Het zegt gewoon: "Ja, deze auto is ook een speeltje, dus hij hoort in de speelgoeddoos." Dit maakt de logica schoner en gemakkelijker voor computers om te controleren.

Wat Rzk Kan (en Niet Kan)

De auteurs hebben een "standaardbibliotheek" voor dit nieuwe systeem gebouwd, genaamd sHoTT. Deze is al enorm en bevat meer dan 25.000 regels code en bijna 1.500 top-level verklaringen. Deze bibliotheek heeft complexe concepten zoals de $\infty$ -categorische Yoneda-lemma (een fundamentele stelling in de categorietheorie) en diverse soorten "fibraties" (manieren om categorieën op elkaar te stapelen) succesvol geformaliseerd.

Echter, het artikel is zeer voorzichtig over wat het beweert te hebben bewezen:

Het is Getrouw (Faithful): De auteurs hebben bewezen dat alles wat je in de oorspronkelijke theorie (RSTT) kunt bewijzen, ook in Rzk bewezen kan worden. Het is een perfecte vertaling.
Het is Conservatief (met een kanttekening): Ze hebben bewezen dat Rzk geen nieuwe waarheden over de oude theorie uitvindt. Als Rzk iets bewijst over een oude vorm, kon de oude theorie dat ook bewijzen. Maar, dit bewijs werkt alleen voor een specifiek "natuurlijk fragment" van afleidingen. De auteurs geven toe dat ze dit nog niet volledig hebben bewezen voor elke mogelijke vreemde casus; ze vermoeden dat het algemeen geldt, maar het is nog steeds een conjectuur voor het volledige systeem.
Het is Praktisch: Het hulpmiddel werkt nu direct. Het draait in een webbrowser, heeft een VS Code-extensie en is al gebruikt in zomercursussen en masterscripties.

De "Shape Solver"

Een van de moeilijkste onderdelen van deze wiskunde is controleren of een vorm binnen een andere vorm past (bijv. zit deze driehoek binnen dit vierkant?). Rzk gebruikt een geautomatiseerde "tope solver" om dit te doen.

Hoe het werkt: Het is een beetje als een detective die een puzzel probeert op te lossen. Het kijkt naar de regels (topes) en probeert te zien of ze passen.
Hoe goed is het? In tests op de sHoTT-bibliotheek heeft de solver meer dan 25.000 vragen afgehandeld. De meeste werden direct opgelost (in één stap). Een paar waren erg moeilijk en namen duizenden stappen in beslag, maar de solver beheerst ze.
De Limiet: De solver is onvolledig. Het is een prototype. Het werkt geweldig voor de problemen die het tegenkomt, maar de auteurs geven toe dat het sommige lastige oplossingen kan missen omdat het niet elke mogelijke route probeert. Ze zijn van plan in de toekomst een "perfecte" solver te bouwen, maar voor nu is de huidige versie "voldoende in de praktijk".

Wat Rzk Verwerpt

Het artikel argumenteert expliciet tegen het idee dat je elke kleine inclusie van vormen handmatig moet bewijzen. In oudere systemen moest je misschien een lang bewijs schrijven om alleen maar te zeggen "deze driehoek zit binnen dit vierkant". Rzk verwerpt deze handmatige arbeid; het automatiseert het.

Het verwerpt ook het idee van coercions (het toevoegen van extra lagen verpakking om dingen te laten passen). De auteurs laten zien dat je een systeem kunt hebben dat subtypes begrijpt zonder de computer te dwingen om onzichtbare conversiestappen in te voegen die de wiskunde compliceren.

De Kernboodschap

Rzk is een werkend, bruikbaar hulpmiddel dat de abstracte theorie van gerichte $\infty$ -categorieën naar de echte wereld van computergecontroleerde bewijzen brengt. Het splitst complexe wiskundige "magische dozen" op in eenvoudigere, transparante delen en bewijst dat het de oude regels niet breekt terwijl het nieuwe mogelijkheden toevoegt.

De auteurs zijn zelfverzekerd dat Rzk de theorie getrouw implementeert en dat hun bibliotheek werkt. Ze zijn zeker dat het hulpmiddel nuttig is voor onderwijs en onderzoek vandaag. Echter, ze zijn minder zeker over de volledige theoretische garanties voor elke mogelijke uitzondering (de "full conservativity" conjecture) en geven toe dat hun shape-solver een prototype is dat verbeterd kan worden. Ze hebben het probleem nog niet opgelost om het systeem voor alle mogelijke inputs te laten termineren (normalisatie), wat een openstaande uitdaging blijft voor de toekomst.

Kortom: Rzk is een werkende, geverifieerde en groeiende motor voor een nieuw soort wiskunde, gebouwd met een fris ontwerp dat de taak van de computer makkelijker maakt zonder de magie van de oorspronkelijke theorie te verliezen.

Probleemstelling
Het artikel behandelt de behoefte aan een bewijsassistent die in staat is tot synthetisch redeneren over $\infty$ -categorieën, specifiek $(\infty, 1)$ -categorieën. Hoewel Homotopy Type Theory (HoTT) een synthetisch kader biedt voor $\infty$ -groepoids (waarbij alle morfismen inversibel zijn), mist het de machinerie om gerichte morfismen te hanteren, die essentieel zijn voor de categorietheorie. Simplicial Type Theory (RSTT) van Riehl en Shulman werd voorgesteld als een oplossing, waarbij "shapes" (zoals gerichte intervallen en driehoeken) en "extension types" worden geïntroduceerd om morfismen en hogere cellen definitioneel te definiëren. RSTT blijft echter grotendeels een theoretisch kader; het is nog niet geïmplementeerd in een praktische bewijsassistent. De primaire uitdagingen bij het implementeren van RSTT omvatten het computationeel uitvoerbaar maken van type checking, het afhandelen van de complexe randvoorwaarden van extension types, en het formaliseren van de metatheoretische aannames (zoals shape inclusies) waarop RSTT-stellingen vaak schematisch steunen.

Methodologie
De auteurs presenteren Rzk, een bewijsassistent die een computationele verfijning van RSTT implementeert. De methodologie bestaat uit drie hoofdlagen van ontwikkeling:

Theoretische Verfijning (Declaratieve Rzk): De auteurs definiëren een declaratieve variant van RSTT (dRzk) die twee belangrijke structurele wijzigingen introduceert om de theorie geschikter te maken voor implementatie:
- Split Extension Types: In plaats van één enkele extension type-vormer, scheidt dRzk het concept in een vorm-geïndexeerde functietype (een $\Pi$ -type over een vorm) en een type-restrictie (het aanhechten van een definitionele rand aan een willekeurig type). Dit stelt de type checker in staat om tussenliggende types te verwerken waarbij een functie wordt toegepast, maar de randvoorwaarden nog niet volledig zijn opgelost.
- Coercion-Free Subtyping: Om de "stille" identificaties te hanteren die vaak in papieren bewijzen worden gemaakt (bijv. het behandelen van een gerestringeerd type als het onderliggende type), introduceert dRzk een expliciete, coercie-vrije subtyping-relatie. Dit zorgt ervoor dat termen ongewijzigd blijven tijdens subtyping-checks, waardoor coherentieproblemen worden vermeden.
Metatheoretische Formalisering: De auteurs formaliseren de "Meta-Theoretic Parameter Layer" (MPL). RSTT-stellingen worden vaak schematisch geformuleerd over abstracte kubussen, topes (logische formules op kubussen) en type-families. Rzk internaliseert deze als first-class parameters binnen definities, waardoor het systeem shape inclusies en zijdelingse voorwaarden expliciet kan afhandelen in plaats van als impliciete meta-niveau aannames.
Algoritmische Implementatie: De auteurs implementeren een algoritmische versie (aRzk) met:
- Bidirectionale Type Checking: Een standaard bidirectionaal algoritme dat is aangepast om de tope-context door alle oordelen (judgments) te dragen.
- Type-Directed Computation: Normalisatie wordt gedefinieerd op geëlaborreerde termen die hun types cachen, aangezien reductie afhankelijk is van type-informatie (specifiek, of een rand-tope standhoudt).
- Geautomatiseerde Tope Solver: Een prototype solver voor de logica van vormen (intuïtionistische propositielogica over gerichte intervallen) die automatisch implicaties controleert die vereist zijn voor shape inclusies en randvoorwaarden.
- Subtyping Integratie: Subtyping is geïntegreerd in de definitionele gelijkheid met behulp van een variantie-flag, waardoor het invoegen van expliciete coercies wordt vermeden.

Kernbijdragen

Rzk Bewijsassistent: De eerste implementatie van een simplicial type theory voor synthetische $\infty$ -categorietheorie. Het is geschreven in Haskell en werkt via een browser-gebaseerde playground en een VS Code extensie.
Formele Translatie en Conservativiteit: De auteurs definiëren een translatie $\tau$ van RSTT naar dRzk en een achterwaartse translatie $\sigma$ . Ze bewijzen dat de translatie getrouw (faithful) is (elke RSTT-bewijs vertaalt naar een Rzk-bewijs) en conservatief op een natuurlijk fragment van afleidingen (dRzk bewijst niets nieuws over RSTT-types). Dit fragment vereist dat "vrijstaande" restricties (restricties die niet aan een shape- $\Pi$ codomein zijn gehecht) niet als hypothesen worden aangenomen, maar alleen als conclusie.
sHoTT Library: De auteurs demonstreren het nut van Rzk via de sHoTT library, een standaardbibliotheek met meer dan 25.000 regels code en bijna 1.500 declaraties. Deze bibliotheek formaliseert kernconcepten van synthetische $(\infty, 1)$ -categorietheorie, waaronder Segal en Rezk types, covariante families, adjuncties en de eerste formele formalisering van de $\infty$ -categorische Yoneda lemma.
Implementatiedetails: Het artikel beschrijft de specifieke algoritmen voor het afhandelen van tope-logica, bidirectionale typing met tope-contexten, en de integratie van subtyping in definitionele gelijkheid.

Resultaten

Correctheid: Het systeem voert de sHoTT library succesvol type-check. De auteurs rapporteren dat de tope solver, hoewel incompleet, het overgrote deel van de queries in de bibliotheek efficiënt afhandelt (59% in één stap, 99% binnen 35 stappen).
Bugfixes: De rigoureuze vergelijking tussen de declaratieve theorie en de implementatie legde twee soundness bugs bloot in eerdere versies (v0.7.7) gerelateerd aan identity type vergelijking en asymmetrische subtyping checks, die zijn opgelost in v0.7.8.
Prestaties: De solver beslaat ongeveer 10% van de totale type-checking tijd. Het systeem is in staat complexe bewijzen, zoals de Yoneda lemma, te verwerken zonder handmatige interventie voor shape inclusies.

Betekenis en Claims
Het artikel claimt dat Rzk de eerste en enige bewijsassistent is voor RSTT, waarmee de kloof tussen de theoretische voorstel van Riehl en Shulman en praktische formalisering wordt overbrugd. De betekenis ligt in:

Mogelijk maken van Synthetische $\infty$ -Categorietheorie: Het stelt wiskundigen in staat om direct binnen de type theory over $(\infty, 1)$ -categorieën te redeneren, met behulp van extension types om hom-types en compositie definitioneel te definiëren, zonder propositionele boekhouding.
Praktisch Gebruiksgemak: Het bestaan van sHoTT toont aan dat de theorie niet alleen theoretisch solide is, maar ook praktisch bruikbaar voor niet-triviale wiskunde.
Theoretische Rigor: Door getrouwheid en conservativiteit te bewijzen, zorgen de auteurs ervoor dat Rzk een getrouwe implementatie is van het oorspronkelijke RSTT-voorstel, en geen afwijkende variant.

De auteurs blijven bescheiden over openstaande problemen. Ze erkennen dat volledige conservativiteit voor alle dRzk afleidingen (inclusief die met vrijstaande restricties in hypothesen) momenteel een conjectuur is. Ze merken ook op dat de terminatie van normalisatie voor RSTT in het algemeen niet bekend is, en dat de tope solver een prototype is dat weliswaar sound maar incompleet is. Toekomstig werk omvat het mechaniseren van de metatheorie, het implementeren van een normalisation-by-evaluation backend, en het toevoegen van ondersteuning voor impliciete argumenten en hogere inductieve types.

Het Grote Idee: Een Nieuwe Manier om te Bouwen

Wat Rzk Kan (en Niet Kan)

De "Shape Solver"

Wat Rzk Verwerpt

De Kernboodschap

Meer zoals dit