💻 computer science

Nominal techniques as an Agda library

Dit artikel beschrijft de ontwikkeling van een Agda-bibliotheek die nominal techniques implementeert om de behandeling van namen en variabele binding in programmeertalen wiskundig onderbouwd en praktisch bruikbaar te maken.

Oorspronkelijke auteurs: Murdoch J. Gabbay, Orestis Melkonian

Gepubliceerd 2026-03-05

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Murdoch J. Gabbay, Orestis Melkonian

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 voor dat je een enorme bibliotheek bouwt waar boeken (of in dit geval, computerprogramma's) worden opgeslagen. In deze bibliotheek zijn er veel boeken met dezelfde titel, maar ze zijn eigenlijk allemaal verschillend. Het probleem is: hoe zorg je ervoor dat je precies weet welk boek je pakt als je alleen de titel kent?

In de wereld van informatica noemen we deze titels "namen" en het koppelen van een naam aan een boek "variabele binding". Dit is een van de lastigste puzzels voor programmeurs en wiskundigen.

Dit paper, geschreven door Murdoch Gabbay en Orestis Melkonian, gaat over het oplossen van deze puzzel met een nieuwe, slimme tool die ze hebben gebouwd voor een programma genaamd Agda.

Hier is de uitleg in simpele taal, met een paar creatieve vergelijkingen:

1. Het "Kip-en-Ei" Probleem

De auteurs beginnen met een vervelend probleem: niemand gebruikt deze slimme wiskundige methode (genaamd "nominal techniques") omdat er geen gereedschap is om het te gebruiken. Maar niemand bouwt gereedschap omdat er niemand is die het wil gebruiken. Het is een klassiek kip-en-ei-dilemma.

Ze willen dit doorbreken. Ze zeggen: "Laten we een gereedschap bouwen dat zo makkelijk is om te gebruiken, dat iedereen het wil proberen."

2. De Magische Bibliotheek (Agda)

Agda is een heel streng en nauwkeurig programma (een "bewijs-assistent"). Het is als een super-intelligente bibliothecaris die elke fout in je logica direct ziet. Maar Agda is vaak lastig om mee te werken als je met namen en variabelen te maken hebt.

De auteurs hebben een bibliotheek (een verzameling gereedschappen) voor Agda gemaakt. Je kunt dit zien als een "plugin" of een extra gereedschapskist die je aan Agda toevoegt.

3. De Sleutel: Atomen en het "Nieuw"-Principe

In hun systeem gebruiken ze iets dat ze atomen noemen.

De Analogie: Stel je voor dat atomen zijn als unieke, onvergankelijke stickers die je op alles kunt plakken.
Ze hebben oneindig veel stickers, en ze kunnen altijd een nieuwe, frisse sticker vinden die nog nergens op staat. Dit is cruciaal. In de oude methoden was het lastig om een "nieuwe" naam te vinden die niet al ergens in je programma voorkwam. Bij deze nieuwe methode is dat net zo makkelijk als het pakken van een nieuwe sticker uit een oneindige doos.

4. Het "Wissel-Spel" (Swapping)

Een van de slimste onderdelen van hun systeem is het concept van wisselen (swapping).

De Analogie: Stel je voor dat je twee stickers op een bord hebt: een rode (A) en een blauwe (B). Als je ze verwisselt, verandert de hele situatie, maar de structuur blijft hetzelfde.
In hun systeem kunnen ze wiskundig bewijzen dat als je twee namen verwisselt, je programma nog steeds correct werkt. Ze hebben een automatische manier gevonden om dit "wissel-spel" toe te passen op elk type data, zonder dat de programmeur het handmatig hoeft te doen. Het is alsof je een magische knop hebt die zegt: "Verwissel alle rode en blauwe stickers in dit hele gebouw, en zorg dat alles nog steeds klopt."

5. Het Grote Voordeel: Geen "De Bruijn Indexen"

Vroeger, als je wilde werken met deze namen in Agda, moest je gebruikmaken van iets dat "de Bruijn indexen" heet.

De Vergelijking: Dit is alsof je in plaats van namen te gebruiken, alleen maar getallen moet gebruiken om aan te geven welke naam bij welk boek hoort. "Boek 3 verwijst naar Boek 1". Dit is saai, foutgevoelig en moeilijk te lezen.
Met hun nieuwe bibliotheek kunnen programmeurs gewoon echte namen gebruiken (zoals x of y), precies zoals ze dat in hun hoofd doen. De computer regelt de ingewikkelde getallen en indexen op de achtergrond.

6. Het Resultaat: Een Schone Substitutie

Het paper laat zien hoe je met deze nieuwe methode heel makkelijk kunt werken met lambda-calculus (de basis van programmeertalen).

Ze tonen aan hoe je een variabele kunt vervangen (substitutie) zonder in de war te raken door welke naam waar staat.
Het is alsof ze de "gnarly" (ingewikkelde en vervelende) appendix van een wiskundig boek hebben vervangen door een heldere, overzichtelijke instructie.

Samenvatting

Kortom, Gabbay en Melkonian hebben een brug gebouwd tussen een complexe wiskundige theorie en een praktisch programmeerhulpmiddel.

Ze zeggen: "Wiskundigen hebben al jaren een prachtig systeem bedacht om met namen om te gaan, maar het was te moeilijk om te gebruiken. Wij hebben het nu verpakt in een gebruiksvriendelijke doos voor Agda. Nu kunnen programmeurs en onderzoekers zich richten op het bouwen van goede programma's, in plaats van vast te zitten aan de technische details van namen."

Het is een stap in de richting van een wereld waar complexe softwareformalisaties makkelijker, veiliger en sneller te bouwen zijn.

Probleemstelling

Nominal techniques (nominale technieken) bieden een wiskundig onderbouwde aanpak voor het omgaan met namen en variabelebinding in programmeertalen. Ondanks hun theoretische kracht is de integratie in praktische toolchains traag verlopen. De auteurs identificeren een "kip-en-ei"-probleem: er zijn geen gebruikers voor nominale technieken omdat ze niet geïmplementeerd zijn, en er wordt niets geïmplementeerd omdat er geen gebruikers zijn. Het doel van dit paper is deze vicieuze cirkel te doorbreken door een brug te slaan tussen theoretische elegantie en praktische bruikbaarheid binnen een bewijsassistent.

Methodologie

De auteurs hebben een Agda-bibliotheek ontwikkeld die nominaal werken mogelijk maakt binnen een constructieve type-theoretische context. De aanpak omvat de volgende technische stappen:

Abstracte Atomen: De ontwikkeling begint met een abstract type Atom dat voldoet aan specifieke constraints: decibele gelijkheid (DecEq) en oneindige telbaarheid (Enumerable∞). Dit wordt gemodelleerd via moduleparameters in Agda.
De 'N'-kwantificator: Er wordt een kwantificator N geïntroduceerd die uitdrukt dat een predicaat geldt voor "alle maar eindig veel" atomen. Dit is essentieel voor het definiëren van eindige ondersteuning (finite support).
Swapping en Wetten: Een fundamenteel concept is het verwisselen (swap) van twee atomen. Dit wordt gedefinieerd als een record Swap met een veld swap : Atom → Atom → A → A. Voor atomen zelf is dit gedefinieerd met een if-then-else constructie.
- Er worden strikte wetten (SwapLaws) opgelegd, zoals identiteit, reversibiliteit en symmetrie.
- Een cruciale eigenschap is dat swapping distribueert over alle typeconstructoren (constructors, functies, typevormers), wat wordt gerealiseerd via een tactiek die deze axioma's automatisch toepast.
Constructieve Concretisering: In tegenstelling tot niet-constructieve theorieën (zoals Fraenkel-Mostowski verzamelingstheorie), is het in deze constructieve Agda-setup mogelijk om een totale functie conc (concretization) te definiëren. Deze functie neemt een abstractie (een paar van een atoom en een element) en een atoom, en levert een element op door het atoom te "vervangen" via swapping.
Meta-programmering: Om de ergonomie te maximaliseren, gebruiken de auteurs Agda's elaborator reflection (macros). Deze macro's genereren automatisch de implementatie van swapping voor elke door de gebruiker gedefinieerde datatype, gebaseerd op de structuur van het type. Dit elimineert de noodzaak voor handmatige, repetitieve bewijzen van swapping-wetten.

Belangrijkste Bijdragen

Een Ergonomische Agda-bibliotheek: Het paper presenteert een port van het Haskell nom-package naar Agda, maar met een tweeledig doel: het bieden van een gebruiksvriendelijke bibliotheek voor eigen formalisaties én het bestuderen van de meta-theorie van nominale technieken op een rigoureuze, constructieve manier.
Constructieve Concretisering: Een nieuw inzicht is dat een totale concretiseringsfunctie (conc) consistent is binnen een constructieve opzet, iets dat in traditionele niet-constructieve nominale theorieën onmogelijk is.
Automatisering: De implementatie van een macro die automatisch swapping-wetten en -definities afleidt voor complexe datatypes, wat de "moral victory" (acceptabele overhead) garandeert voor praktische systemen.
Vereenvoudiging van Substitutie: In plaats van de lastige indexmanipulaties van de de Bruijn-indiceermethode (zoals in de PLFA-textbook), wordt substitutie nu op een natuurlijke manier gedefinieerd met behulp van nominale concepten (zoals freshAtom en conc).

Resultaten

De auteurs hebben de bibliotheek succesvol toegepast in een case study voor de ongetypeerde $\lambda$ -calculus:

Definitie van Termen: Termen kunnen worden gedefinieerd zonder verwijzing naar de Bruijn-indices, puur via atomen en abstrcties (Abs).
$\alpha$ -equivalentie: De $\alpha$ -equivalentie van $\lambda$ -termen wordt natuurlijk uitgedrukt met de N-kwantificator.
Substitutie: De definitie van substitutie (_[_:=_]) is aanzienlijk vereenvoudigd. Het gebruik van freshAtom zorgt ervoor dat variabelebinding correct wordt gehanteerd zonder handmatige indexherberekening.
Mechanisering: De resultaten zijn volledig gemechaniseerd en openbaar beschikbaar. De auteurs hebben bewezen dat de benodigde lemmata voor de confluëntiebewijzen (confluence proof) haalbaar zijn, en zien geen inherente obstakels voor het voltooien van deze bewijzen.

Betekenis en Impact

Dit werk is significant omdat het de toegankelijkheid van nominale technieken vergroot binnen de gemeenschap van constructieve type-theorie.

Virtuele Cirkel: Het biedt een oplossing voor het "kip-en-ei"-probleem door een werkend, gebruiksvriendelijk voorbeeld te leveren dat de adoptie kan stimuleren.
Complementair: De bibliotheek vult bestaande implementaties aan (zoals in FreshML, Isabelle/HOL en Nuprl) door specifiek te focussen op een constructieve, lichtgewicht en ergonomische aanpak binnen Agda.
Toekomstperspectief: Het succes met de $\lambda$ -calculus legt de basis voor verdere formalisaties, zoals het bewijs van cut-eliminatie voor eerste-orde logica, wat complexere naam-abstrcties vereist.

Kortom, het paper demonstreert dat nominale technieken niet alleen theoretisch elegant zijn, maar ook praktisch toepasbaar en bewijsbaar binnen een moderne, constructieve bewijsassistent zoals Agda.