💻 computer science

Dependent Multiplicities in Dependent Linear Type Theory

Dit artikel introduceert een nieuwe afhankelijke lineaire type-theorie die het mogelijk maakt dat variabele multipliciteiten afhankelijk zijn van andere variabelen, waardoor nauwkeurige resource-aanduidingen worden geboden voor vertakkende en recursieve programma's via een inbedding van lineaire logica in afhankelijke type-theorie, ondersteund door een categorische semantiek en een Agda-implementatie.

Oorspronkelijke auteurs: Maximilian Doré

Gepubliceerd 2026-05-20

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Maximilian Doré

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

Het Grote Idee: Een "Slimme" Resourcebeheerder

Stel je voor dat je een computerprogramma schrijft. In de wereld van de informatica zijn sommige dingen als resources (zoals een bestand dat je opent, een batterij die je leegtrekt, of een geheime sleutel die je gebruikt). Je wilt ervoor zorgen dat je programma deze resources precies het juiste aantal keer gebruikt: niet te vaak (wat ze verspillen of fouten veroorzaakt) en niet te weinig (wat werk onafgewerkt laat).

Al geruime tijd gebruiken informatici een systeem genaamd Lineaire Logica om deze resources bij te houden. Denk hierbij aan een strenge bibliothecaris die zegt: "Je kunt dit boek precies één keer lenen. Als je probeert het twee keer te lenen, stopt het systeem je."

Echter, deze strenge bibliothecaris heeft een probleem: hij is te star. Hij kan geen situaties aanpakken waarbij het aantal keren dat je een resource nodig hebt, afhangt van een beslissing die je neemt terwijl het programma draait.

Het Probleem met de Oude Regels:
Stel je voor dat je een functie hebt die beslist of je een taart bakt of een salade maakt, gebaseerd op een boolean-schakelaar (Waar/Niet-Waar).

Als de schakelaar Waar is, heb je misschien 3 eieren nodig.
Als de schakelaar Niet-Waar is, heb je misschien 0 eieren nodig.

Oude systemen konden niet zeggen: "Het aantal eieren hangt af van de schakelaar." Ze dwongen je om te zeggen: "Je hebt 3 eieren nodig, wat er ook gebeurt," of "Je hebt 0 eieren nodig, wat er ook gebeurt." Dit is inefficiënt en vaak onmogelijk voor complexe programma's met loops of vertakkingslogica.

De Oplossing: "Afhankelijke Multipliciteiten"

Dit artikel introduceert een nieuw systeem waarbij het aantal keren dat je een resource gebruikt (de multipliciteit) kan afhangen van andere variabelen in het programma.

Denk hierbij aan een slimme automaat in plaats van een strenge bibliothecaris.

Oud Systeem: De automaat zegt: "Je kunt precies 1 frisdrank kopen." (Punt).
Nieuw Systeem: De automaat zegt: "Je kunt zoveel frisdrank kopen als het aantal dollars in je portemonnee." Als je 5 dollar inlegt, krijg je 5 frisdranken. Als je 2 dollar inlegt, krijg je 2. De regel hangt af van de waarde die je verstrekt.

In deze nieuwe theorie is de "multipliciteit" (het aantal keren dat een variabele wordt gebruikt) geen vaststaand getal in steen gehouwen. Het is een dynamische berekening die plaatsvindt terwijl het programma draait.

Hoe Het Werkt: De Twee Schillen

De auteur, Maximilian Doré, bouwt dit systeem door twee verschillende manieren van denken over logica te combineren:

De "Host"-theorie (Het Brein): Dit is de standaard, flexibele logica die wordt gebruikt in de meeste moderne programmeertalen. Het behandelt het "denkende" deel: beslissingen nemen, getallen berekenen en voorwaarden controleren.
De "Lineaire" theorie (De Portemonnee): Dit is de strenge logica die resources bijhoudt.

De magie van dit artikel zit hem in hoe ze deze twee verbinden. In plaats dat de "Portemonnee" (Lineaire Logica) een apart, star vakje is, is deze ingebouwd in het "Brein" (Host-theorie).

De Analogie: Stel je voor dat het "Brein" een chef-kok is en de "Portemonnee" het voorraadkastje met ingrediënten.
- In oude systemen moest de chef een vast recept opschrijven: "Gebruik 2 eieren."
- In dit nieuwe systeem kan de chef zeggen: "Gebruik n eieren," waarbij n een getal is dat de chef tijdens het koken berekent, gebaseerd op hoe hongerig de klanten zijn. Het voorraadsysteem (Lineaire Logica) werkt in real-time bij op basis van de berekening van de chef.

Belangrijkste Kenmerken Eenvoudig Uitgelegd

1. Dynamische Vertakking (Het "If/Else"-Probleem)
In het artikel laat de auteur zien hoe "If/Else"-statements perfect kunnen worden verwerkt.

Scenario: Je hebt een boolean-schakelaar.
Oude Manier: Zowel het "If"-pad als het "Else"-pad moesten precies hetzelfde aantal resources gebruiken.
Nieuwe Manier: Het "If"-pad kan 5 resources gebruiken, en het "Else"-pad kan 2 gebruiken. Het systeem weet precies hoeveel resources zijn gebruikt omdat het de waarde van de schakelaar bekijkt voordat het het pad kiest.

2. Recursieve Data (Het "Boom"-Probleem)
Het artikel behandelt complexe datastructuren zoals bomen (een lijst van lijsten, of een stamboom).

Scenario: Je wilt een functie toepassen op elk blad in een boom.
Oude Manier: Je kon niet makkelijk zeggen: "Gebruik de functie precies zo vaak als er bladeren zijn," omdat het systeem niet wist hoeveel bladeren er waren totdat het programma klaar was met draaien.
Nieuwe Manier: Het systeem berekent eerst het aantal bladeren, en stelt dan de regel in: "Gebruik de functie AantalBladeren keer." Het werkt perfect, zelfs voor bomen van elke grootte.

3. De "Realiteit" versus de "Specificatie"
Het artikel maakt onderscheid tussen twee soorten code:

De Specificatie (Het Ontwerp): Dit is het deel waar je getallen berekent en beslissingen neemt. Het is flexibel.
De Uitvoering (De Constructie): Dit is het deel waar resources daadwerkelijk worden verbruikt.
Het systeem staat je toe om het "Ontwerp"-deel te wissen nadat je de wiskunde hebt gedaan, zodat alleen het efficiënte "Constructie"-deel overblijft. Dit betekent dat het definitieve programma snel is en geen onnodige berekeningsbagage met zich meedraagt.

Waarom Dit Belangrijk Is

De auteur heeft dit systeem geïmplementeerd in een programmeertaal genaamd Agda. Ze bewezen dat:

Het wiskundig sound is (het werkt logisch).
Het programma's kan typeren die eerdere systemen niet aankonden (zoals complexe vertakkingen en recursieve functies).
Het een nauwkeurige "bon" geeft voor elk programma, waarin exact wordt getoond hoe vaak elke resource is gebruikt, zelfs als dat getal verandert op basis van de logica van het programma.

Samenvattende Metafoor

Stel je voor dat je een bouwplaats beheert.

Oude Systemen: Je hebt een bouwvoorman die zegt: "We hebben precies 100 bakstenen nodig voor deze muur," ongeacht of de muur groot of klein is. Als de muur klein is, heb je bakstenen over. Als hij groot is, loop je tekort.
Het Systeem van Dit Artikel: Je hebt een slimme bouwvoorman die naar de blauwdrukken kijkt, het aantal bakstenen telt dat nodig is voor deze specifieke muur, en precies dat bedrag bestelt. Als de muur halverwege van grootte verandert, past de bouwvoorman de bestelling direct aan.

Dit artikel geeft informatici een manier om die "slimme bouwvoorman" voor software te bouwen, zodat programma's zowel flexibel zijn als perfect efficiënt met hun resources omgaan.

Probleemstelling
Bestaande kwantitatieve type-theorieën, zoals Quantitative Type Theory (QTT) en Graded Modal Type Theory, staan resource-annotaties toe waarbij variabelen multipliciteiten hebben die specificeren hoe vaak ze worden gebruikt. Deze systemen vertrouwen echter doorgaans op statische multipliciteiten die worden afgeleid uit een vaste resource-algebra (bijvoorbeeld natuurlijke getallen of semiringen). Deze statische aard creëert aanzienlijke beperkingen bij het omgaan met programmalogica die niet direct resources representeert, maar ze organiseert, zoals vertakking (voorwaardelijke instructies) en recursie.

In huidige systemen vereist een booleaanse voorwaarde die wordt gebruikt om te kiezen tussen twee takken dat beide takken identieke resources verbruiken, wat vaak onpraktisch is aangezien verschillende takken doorgaans verschillende bewerkingen uitvoeren. Evenzo hangt bij hogere-orde functies of inductieve typen (zoals binaire bomen) het aantal keren dat een functie wordt toegepast of een resource wordt verbruikt vaak af van waarden die pas tijdens de uitvoering bekend zijn (bijvoorbeeld het aantal bladeren in een boom). Eerdere pogingen om Dependent Type Theory (DTT) te combineren met lineaire logica worstelden met de vraag of typen die afhankelijk zijn van termen een "gebruik" van die termen vormen. Hoewel McBride en Atkey betoogden dat typen voor contemplatie zijn en niet voor berekening (wat afhankelijkheid van lineaire variabelen toestaat), beperkt hun resulterende QTT multipliciteiten nog steeds tot statische elementen, waardoor het dynamische resourcegebruik dat inherent is aan recursieve programma's en data-afhankelijke vertakkingen niet wordt vastgelegd.

Methodologie
Het artikel stelt een nieuwe afhankelijke lineaire type-theorie voor die lineaire logica direct inbedt in een standaard intuïtionistische Dependent Type Theory (de "host-theorie"). De kerninnovatie is de behandeling van multipliciteiten niet als statische algebraïsche elementen, maar als termen binnen de host-theorie zelf.

Twee afleidingsrelaties: Het systeem onderscheidt tussen twee oordelen:
- $\vdash$ : De standaard intuïtionistische DTT (host-theorie), gebruikt voor het definiëren van typen, termen en afhankelijkheden.
- $\Vdash$ : Een resource-bewust calculus waarbij termen worden afgeleid uit "voorraden" (lineaire contexten).
Voorraden als intuïtionistische typen: In tegenstelling tot traditionele lineaire contexten zijn voorraden in dit systeem termen van de host-theorie. Dit stelt de host-theorie in staat om te rekenen met resource-annotaties. Specifiek maakt het systeem gebruik van de natuurlijke getallen van de host-theorie om een "vermenigvuldiging" van voorraden te definiëren ( $\Delta \hat{m}$ ), waarbij $m$ een term is van het type $\mathbb{N}$ . Deze bewerking staat toe dat een voorraad $m$ keer wordt gedupliceerd, waarbij $m$ kan afhangen van andere variabelen in de context.
Dynamische multipliciteiten: Door de multipliciteit $m$ toe te staan een open term van de host-theorie te zijn, ondersteunt het systeem dynamische resource-annotaties. Bijvoorbeeld, een functie die over een boom mapt, kan specificeren dat een functie $f$ precies leafs(t) keer wordt gebruikt, waarbij leafs(t) wordt berekend uit de structuur van de invoerboom $t$ .
Typevormers: Het artikel definieert lineaire versies van standaard DTT-typevormers (functies, paren, booleaanse waarden en W-typen) geannoteerd met deze dynamische multipliciteiten. Cruciaal is dat de eliminatieregels voor booleaanse waarden en W-typen toestaan dat resources verschillend worden verdeeld over takken of constructoren, gebaseerd op waarden tijdens de uitvoering.
Semantiek: De semantiek wordt gekarakteriseerd als "Lineaire Categories with Families" (lCwF), wat Categories with Families (CwF) zijn die geïndexeerd zijn in symmetrische monoidale categorieën. Deze structuur generaliseert Quantitative CwF's die worden gebruikt voor QTT.

Belangrijkste bijdragen

Syntaxis met afhankelijke multipliciteiten: Het artikel presenteert een syntaxis waarbij variabele multipliciteiten termen zijn van de host-theorie, wat een nauwkeurige typering mogelijk maakt van programma's die vertakking en recursie omvatten en die eerder niet typerbaar waren in lineaire systemen.
Lineaire W-typen: Een principiële behandeling van inductieve typen (specifiek W-typen met eindige posities) in een lineaire setting. Het systeem biedt introductie- en eliminatieregels die correct rekening houden met het dynamische resourcegebruik van recursieve structuren.
Semantische karakterisering: De auteurs definiëren lCwF's als het semantische model voor de theorie en tonen aan hoe standaard DTT-modellen en lineaire logica-modellen samenkomen. Ze demonstreren dat dit model de ingewikkelde regels voor lineaire W-typen rechtvaardigt en bestaande modellen voor QTT generaliseert.
Realiseerbaarheid en verwijdering: Er wordt een realiseerbaarheidsmodel geconstrueerd (gebaseerd op BCI-algebra's) om aan te tonen dat het intuïtionistische fragment ( $\vdash$ ) kan worden verwijderd voor berekening, waarbij alleen het lineaire fragment ( $\Vdash$ ) overblijft voor uitvoering, vergelijkbaar met de 0- en 1-fragmenten van QTT.
Implementatie: De theorie is geïmplementeerd in Agda. De implementatie maakt gebruik van de semantische interpretatie (het afbeelden van lineaire oordelen op intuïtionistische termen uitgerust met getuigen van voorraden) om een rigoureuze, zij het nog niet praktische, typechecker te creëren.

Resultaten

Expressiviteit: Het systeem typt succesvol programma's die dynamische resource-telling vereisen, zoals een map-functie voor binaire bomen waarbij het gebruik van de mappende functie evenredig is met het aantal bladeren.
Volledigheid: Het artikel bewijst een volledigheidresultaat voor "duidelijk lineaire termen" (intuïtionistische termen die waarden niet wegwerpen of dupliceren via specifieke eliminators), en toont aan dat deze precies kunnen worden getypt in het lineaire systeem.
Herstel van intuïtionistische logica: Door een lineaire exponentiële comonade ("!") in te voeren, kan het systeem volledige intuïtionistische logica herstellen binnen het lineaire fragment, waardoor onbeperkt gebruik van resources mogelijk is waar nodig.
Afweging beslisbaarheid: De auteurs erkennen dat type-checking in het algemene geval onbeslisbaar is omdat het het vergelijken van open termen van natuurlijke getallen vereist (bijvoorbeeld controleren of $\Delta \hat{m}$ gelijk is aan $\Delta \hat{n}$ ). Ze merken echter op dat propositionele gelijkheid in de host-theorie kan worden gebruikt om de typechecker te overtuigen van resource-equivalentie.

Betekenis
Het artikel claimt een expressievere versie van Quantitative Type Theory te bieden door over te stappen van statische resource-algebra's naar dynamische, berekenbare multipliciteiten die zijn afgeleid uit de host-theorie. Door lineaire logica in DTT in te bedden in plaats van ze als aparte logica's te behandelen, vermijdt het systeem de restrictieve dichotomie tussen intuïtionistische en lineaire variabelen die in eerdere werken werd aangetroffen. Dit staat een "principiële resource-bewuste behandeling" toe van een grote klasse inductieve typen en hogere-orde functies. Het werk toont aan dat bestaande talen met afhankelijk getypte functies kunnen worden uitgebreid met dit systeem, wat een weg biedt naar nauwkeurigere resourcebeheer in functioneel programmeren zonder de expressiviteit van afhankelijke typen op te offeren. De auteurs positioneren hun werk als een generalisatie van QTT die de beperkingen van statische multipliciteiten bij het omgaan met resourcegebruik dat afhankelijk is van de uitvoeringstijd, oplost.