💻 computer science

Ordered Adjoint Logic (Extended Version)

Dit artikel generaliseert eerder werk over geordende logica's door een systeem van adjungerende modaliteiten te introduceren dat logica's met uiteenlopende structurele eigenschappen zoals verzwakking en contractie combineert, en bewijst dat de resulterende sequentiekalkulus eliminatie van de cuts toestaat en dat zijn formulering in natuurlijke deductie beslisbare bewijscontrole ondersteunt.

Oorspronkelijke auteurs: Sophia Roshal, Frank Pfenning

Gepubliceerd 2026-05-20

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Sophia Roshal, Frank Pfenning

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 zeer strenge, hoogbeveiligd magazijn beheert. In dit magazijn heeft elk item (een "resource") een specifieke set regels over hoe het behandeld mag worden. Sommige items kunnen worden gekopieerd, sommige kunnen worden weggegooid, sommige kunnen vrijelijk worden verplaatst, en andere moeten precies één keer en in een specifieke volgorde worden gebruikt.

Al geruime tijd hebben informatici "logieken" (wiskundige regelboeken) gebouwd om deze items te beheren. De meeste regelboeken waren echter te star. Ze lieten items ofwel overal naartoe bewegen (zoals een rommelige kamer) of dwongen ze om in een strenge rij te blijven zonder enige flexibiliteit.

Het Probleem: De "Eén-Formaat-Voor-Alles" Bottleneck
Eerdere pogingen om deze regels te mengen (zoals het werk van Kanovich et al.) probeerden dit op te lossen door een "basismodus" te hebben: een standaard, super-strenge zone waar alles gebeurt. Om iets flexibels te doen, moest je je items inpakken, ze naar deze strenge zone verplaatsen, je werk doen, en ze vervolgens weer terugbrengen. Het was alsof je door een beveiligingscontrole moest om een pen van je bureau te pakken. Het was onhandig en vereiste constante wisselingen.

De Oplossing: Geordende Adjoint Logica
Sophia Roshal en Frank Pfenning stellen een nieuw systeem voor dat Geordende Adjoint Logica heet. Denk hierbij niet aan één enkel magazijn, maar aan een slim, meerlagig logistiek netwerk.

Hier is hoe hun nieuwe systeem werkt, met eenvoudige analogieën:

1. De "Modi" zijn Verschillende Zones

In plaats van één strenge basiszone, stel je een gebouw voor met verschillende verdiepingen, of "modi".

Verdieping A (Strenge): Items hier moeten precies één keer worden gebruikt, in volgorde, en kunnen niet worden verplaatst.
Verdieping B (Flexibele): Items hier kunnen worden gekopieerd, weggegooid of door elkaar gehusseld.
Verdieping C (Directionele): Items hier kunnen naar links bewegen, maar niet naar rechts, of andersom.

In dit nieuwe systeem hoef je niet alles in één strenge zone te forceren. Je kunt native werken op de verdieping die bij je behoeften past.

2. De "Liften" (Adjoint Modaliteiten)

De magie van hun systeem zit in de lift. Ze gebruiken speciale "shift"-operatoren (adjointen genoemd) om items tussen verdiepingen te verplaatsen.

Als je een flexibel item hebt maar het in een strenge zone moet gebruiken, neem je de lift naar beneden.
Als je een streng item hebt maar het in een flexibele zone moet gebruiken, neem je de lift naar boven.

Dit is veel soepeler dan de oude "basismodus"-aanpak, omdat je alleen de lift neemt wanneer je absoluut moet wisselen van context. Je blijft zo lang mogelijk op je native verdieping.

3. De "Eénrichtingsstraten" (Directionele Mobiliteit)

Dit is de grootste innovatie van het artikel. In eerdere systemen, als een item kon bewegen, kon het meestal in beide richtingen bewegen (links en rechts).

Roshal en Pfenning beseften dat je soms alleen dingen in één richting hoeft te verplaatsen.

De Beveiligingsanalogie: Stel je een beveiligingsbadge voor.
- Autorisatie (Links Mobiel): Je kunt je beveiligingsclearance voordat je je hoogbeveiligde taak begint. Je kunt het "autorisatie"-item naar links van het "taak"-item verplaatsen.
- De Taak (Rechts Mobiel): Je kunt de hoogbeveiligde taak na de autorisatie uitvoeren. Je kunt het "taak"-item naar rechts verplaatsen.
- De Beperking: Je kunt de taak niet voor de autorisatie verplaatsen.

Hun systeem staat Links Mobiliteit (naar links bewegen) en Rechts Mobiliteit (naar rechts bewegen) toe als aparte, onafhankelijke regels. Hierdoor kunnen ze complexe real-world protocollen (zoals beveiligingscontroles) veel nauwkeuriger modelleren dan voorheen.

4. De "Verkeersregelaar" (Cut Elimination)

In de logica is "cut elimination" als het bewijzen dat een verkeersregelaar niet nodig is om het verkeer te leiden; de auto's kunnen het kruispunt zelf navigeren zonder te crashen.

De auteurs bewezen dat hun nieuwe, complexe systeem van liften en éénrichtingsstraten stabiel is. Zelfs met al deze verschillende regels kun je een bewijs (een pad door het magazijn) altijd vereenvoudigen tot zijn meest directe vorm zonder vast te lopen of tegenstrijdigheden te creëren. Dit bewijst dat het systeem wiskundig sound is.

5. De "Geautomatiseerde Inspecteur" (Beslisbaarheid)

Tot slot creëerden ze een "Natural Deduction"-versie van dit systeem. Denk hierbij aan een geautomatiseerde inspecteur voor code.

In de oude systemen was het controleren of een programma de regels volgde eenvoudig.
In dit nieuwe, complexe systeem is het controleren of een programma geldig is moeilijker, omdat de inspecteur moet gokken waar items zich mogelijk hebben verplaatst (door mobiliteit) of zijn gekopieerd (door verzwakking).
Het Resultaat: De auteurs bewezen dat deze inspecteur altijd zijn werk afmaakt. Hij blijft niet vastzitten in een oneindige lus. Hij kan altijd beslissen: "Ja, deze code is geldig" of "Nee, het breekt de regels", zelfs als de regels zeer subtiel en verborgen zijn.

Samenvatting

Roshal en Pfenning bouwden een nieuw, flexibel regelboek voor het beheren van resources in computerprogramma's.

Geen meer onhandige wisselingen: Je werkt native in je specifieke "modus" en wisselt alleen wanneer nodig.
Eénrichtingsstraten: Ze introduceerden de mogelijkheid om beweging directioneel te controleren (links versus rechts), wat cruciaal is voor beveiliging en ordening.
Het werkt: Ze bewezen dat de wiskunde standhoudt (geen crashes) en dat een computer altijd kan controleren of een programma deze complexe regels volgt.

Dit biedt een solide fundament voor het bouwen van programmeertalen die zeer fijnmazige regels kunnen afdwingen over hoe data wordt gebruikt, verplaatst en beveiligd, zonder dat het systeem te rommelig wordt om te begrijpen of te verifiëren.

Technische Samenvatting van "Ordered Adjoint Logic"

Probleemstelling
Geordende logica's en typesystemen zijn essentieel voor toepassingen variërend van computationele linguïstiek tot handhaving van beveiligingsprotocollen, waarbij de volgorde van hulpbrongebruik van belang is. In de meeste formuleringen zijn geordende types ook lineair, wat vereist dat hulpbronnen precies één keer worden gebruikt. Hoewel eerdere werken van Kanovich et al. calculi onderzochten die deze beperking opheffen via subexponentiënten binnen een lineaire geordende logica, vertrouwt deze aanpak op een "basismodus" waarin alle inferenties plaatsvinden. Voor geordende logica's moet deze basismodus alle structurele regels (verzwakking, contractie, uitwisseling) verbieden, waardoor toepassingen frequent in en uit deze restrictieve modus moeten schakelen. Bovendien verkennen bestaande subexponentiële systemen de mogelijkheid van eenzijdige structurele eigenschappen (bijvoorbeeld linkermobiliteit zonder rechtmobiliteit) niet volledig. De auteurs streven ernaar deze kaders te generaliseren om een preorde van modi te ondersteunen met variërende, fijnmazige structurele eigenschappen – inclusief onafhankelijke controle over verzwakking, linkse/rechtse contractie en linkse/rechtse mobiliteit – zonder te vertrouwen op een enkele restrictieve basismodus.

Methodologie
De auteurs introduceren Ordered Adjoint Logic, een systeem dat de structurele flexibiliteit van adjointe modaliteiten combineert met de ordeningsbeperkingen van geordende logica's. De methodologie verloopt in twee hoofdfasen:

Formulering van het Sequentiecalculus:
De auteurs definiëren een sequentiecalculus waar antecedenten geordende sequenties van gelabelde hypothesen zijn. Structurele regels zijn niet globaal, maar worden beheerst door een preorde van modi ( $k \geq m$ ). Elke modus $m$ is gekoppeld aan een verzameling structurele eigenschappen $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$ (Verzwakking, Contractie, Linkermobiliteit, Rechtmobiliteit).
- Shift-modaliteiten: In plaats van een basismodus gebruikt het systeem shift-modaliteiten ( $\downarrow^k_m$ en $\uparrow^m_l$ ) om te schakelen tussen redeneren op verschillende modi. Deze shifts zijn afgeleid van Benton's adjointe logica, maar gegeneraliseerd om geordende contexten te behandelen.
- Structurele regels: De auteurs ontleden mobiliteit en contractie in eenzijdige varianten. Mobiliteitsregels staan toe dat een enkele propositie willekeurig ver naar links of rechts beweegt binnen de antecedentsequentie, mits de modus van de propositie de overeenkomstige directionele mobiliteit toestaat. Contractie is niet-lokaal toegestaan (het samenvoegen van niet-aangrenzende duplicaten) om eliminatie van de snede te waarborgen, wat verschilt van de lokale contractie in standaard lineaire logica.
- Logische connectieven: De taal bevat geordende implicaties ( $\multimap$ en $\multimap$ ), gefuseerde en gedraaide conjuncties, en shifts. De regels zijn parametrisch in hun modi, met specifieke voorwaarden die de behoud van modusonafhankelijkheid waarborgen (bijvoorbeeld $k \geq m \geq r$ ) bij het lezen van regels van conclusie naar premissen.
Natural Deduction en Beslisbaarheid:
De auteurs schakelen over naar een natural deduction-formulering waar structurele regels impliciet zijn, met als doel een fundament dat geschikt is voor programmeertalen.
- Expliciet versus Impliciet: Aanvankelijk presenteren ze een systeem met expliciete structurele regels om de kloof met het sequentiecalculus te overbruggen. Vervolgens definiëren ze een systeem waar structurele regels (verzwakking, contractie, mobiliteit) impliciet zijn.
- Algoritme voor bewijscontrole: Om het nondeterminisme aan te pakken dat wordt geïntroduceerd door impliciete structurele regels (specifiek de onbeperkte toepassing van verzwakking en de plaatsing van variabelen in eliminatieregels), definiëren de auteurs een "normaalvorm"-oordeel ( $\Omega \gg_{\Gamma, r} \Omega_{nf}$ ). Dit algoritme berekent de verzameling van alle mogelijke normaalvormen (contexten zonder herhaalde variabelen) voor een gegeven context $\Omega$ , verzameling hypothesen $\Gamma$ , en modus $r$ .
- Op verzamelingen gebaseerde oordelen: De natural deduction-regels worden opgeheven om te opereren op verzamelingen van normaalvorm-contexten ( $\Xi$ ). Bijvoorbeeld, conjunctie-invoering berekent het Cartesisch product van contextverzamelingen, terwijl doorsnede wordt gebruikt voor regels die contextovereenkomst vereisen (zoals additieve conjunctie).

Belangrijkste Bijdragen

Gegeneraliseerde Adjointe Logica: Het artikel generaliseert adjointe logica naar geordende settings, waarbij een preorde van modi wordt geïntroduceerd waarbij elke modus onafhankelijk verzwakking, contractie en eenzijdige mobiliteit controleert.
Eenzijdige Structurele Eigenschappen: Het systeem modelleert en bewijst eigenschappen voor linkse en rechtse mobiliteit en contractie expliciet als aparte, onafhankelijke structurele eigenschappen, een kenmerk dat werd verwacht maar niet werd onderzocht in eerdere subexponentiële werken.
Eliminatie van de Snede: De auteurs bewijzen dat het geordende adjointe sequentiecalculus toelaat tot eliminatie van de snede (via multicut) en eliminatie van identiteit, waarmee het systeem wordt gevestigd als een goed functionerend logisch kader.
Beslisbaarheid van Bewijscontrole: Het artikel biedt een natural deduction-systeem met impliciete structurele regels en bewijst dat bewijscontrole voor dit systeem beslisbaar is. Dit wordt bereikt door een eindig algoritme te construeren dat de verzameling normaalvorm-contexten berekent.

Resultaten

Theoretische Korrektheid: Het sequentiecalculus voldoet aan eliminatie van snede en identiteit. Het natural deduction-systeem wordt bewezen correct en volledig ten opzichte van het sequentiecalculus.
Beslisbaarheid: Het algoritme voor het berekenen van normaalvormen ( $NF_{\Gamma, r}(\Omega)$ ) wordt bewezen te termineren. Bijgevolg is het probleem van het controleren van bewijzen in het impliciete natural deduction-systeem beslisbaar.
Substructuur-Subsumptie: De resultaten impliceren de beslisbaarheid van substructuur-subsumptie, een kerncomponent van typecontrole-algoritmen voor talen zoals QRTT (die Kripke-semantiek met expliciete werelden gebruikt).

Betekenis en Claims
De auteurs claimen dat Ordered Adjoint Logic een geschikt fundament biedt voor een expressieve adjointe programmeertaal of logisch kader. Door structurele eigenschappen te ontkoppelen van een enkele basismodus en adjointe shifts te gebruiken, staat het systeem native redenering toe in diverse disciplines (lineair, geordend, onbeperkt) met naadloze schakeling. De beslisbaarheid van bewijscontrole met impliciete structurele regels wordt benadrukt als een kritieke stap naar de implementatie van bidirectionele typecheckers voor functionele programmeertalen die fijnmazige structurele eigenschappen van code kunnen verwerken. Het artikel merkt op dat hoewel de beslissingsprocedure is vastgesteld, praktische efficiëntie (bijvoorbeeld het vermijden van exponentiële complexiteit door onnodige verzwakkingen) onderwerp blijft voor toekomstige optimalisatie. Het werk wordt gepositioneerd als een directe generalisatie van Kanovich et al.'s subexponentiële geordende logica en een uitbreiding van Jang et al.'s adjointe types om ordening op te nemen.