Information Propagation and Contraction in Functional Interpretations

Technische Samenvatting: Informatiepropagatie en Contractie in Functionele Interpretaties

Probleemstelling
Functionele interpretaties, die hun oorsprong vinden in de Dialectica-interpretatie van Gödel, staan centraal bij het extraheren van computationele inhoud uit bewijzen, met name binnen het vakgebied van proof mining. Bestaande varianten (bijv. Diller–Nahm, monotone, begrensde, Herbrand-geïnterpreteerde) combineren doorgaans gelijktijdig meerdere bewijs-theoretische mechanismen: de propagatie van getuige- en uitdaging-informatie (witness and challenge information), de afhandeling van gedupliceerde aannames (contractie), en de behandeling van extensionaliteit. Deze vermenging maakt het moeilijk om de specifieke algebraïsche structuren te isoleren die verantwoordelijk zijn voor verschillende aspecten van de interpretatie. Het artikel identificeert een noodzaak om het mechanisme van affine informatiepropagatie (waarbij aannames niet worden gedupliceerd) te scheiden van het mechanisme van contractie (waarbij gedupliceerde aannames moeten worden samengevoegd).

Methodologie
De auteur stelt een modulair kader voor dat deze mechanismen ontkoppelt via twee primaire algebraïsche componenten:

1. Informatie-nuclei (Information Nuclei): Een algebraïsche interface ontworpen om de affine kern van functionele interpretaties te vatten. Een informatie-nucleus over een doelsysteem $S$ bestaat uit:

   • Een afbeelding van eindige typen $\sigma$ naar informatie-typen $\sigma^\sharp$.
   • Een compatibiliteitsrelatie $x \triangleleft_\sigma a$ tussen exacte objecten $x$ en informatie-objecten $a$.
   • Een eenheidsoperatie $\eta_\sigma: \sigma \to \sigma^\sharp$ die exacte objecten inbedt in informatie.
   • Een Kleisli-extensie $\kappa_{\sigma,\tau}: (\sigma \to \tau^\sharp) \to \sigma^\sharp \to \tau^\sharp$ die informatie door functies propageert.
     Deze componenten moeten voldoen aan axioma's die garanderen dat exacte objecten compatibel zijn met hun inbeddingen en dat informatie correct propageert door functie-applicatie.

2. Contractiestructuren (Contraction Structures): Een extra laag die vereist is om affine interpretaties uit te breiden naar volledige intuïtionistische systemen. Dit omvat een formule-geïndexeerde operatie $ctr_A$ die twee uitdaging-grenzen (challenge bounds) gegenereerd door gedupliceerde aannames neemt en deze reduceert tot een enkele grens. De correctheid van deze operatie wordt gedefinieerd door een eigenschap die waarborgt dat geldigheid tegenover de samengevoegde grens impliceert dat geldigheid tegenover de oorspronkelijke afzonderlijke grenzen.

Het kader opereert binnen eindige-type rekenkundige systemen, waarbij specifiek onderscheid wordt gemaakt tussen:

• $N\text{-}HA^\omega_{aff}$: Een affien systeem zonder contractie.
• $N\text{-}HA^\omega$: Het volledige systeem met contractie.
• $HA^\omega_{obs}$: Een systeem met observationele gelijkheid (beslisbare basistypen), gebruikt om de standaard Dialectica-interpretaties te herstellen.

Belangrijkste Bijdragen en Resultaten

• Scheiding van Zaken (Separation of Concerns): Het artikel stelt vast dat de complexiteit van functionele interpretaties kan worden gedecomposeerd. De "affine kern" wordt volledig gekarakteriseerd door de informatie-nucleus, terwijl contractie door een aparte structuur wordt afgehandeld. Dit maakt een systematische specificatie mogelijk van de informatie die door geëxtraheerde realizers wordt gedragen, onafhankelijk van hoe aannames worden hergebruikt.
• Geldigheidstheorema's (Soundness Theorems):
  • Affine Geldigheid (Theorem 17): Elke informatie-nucleus induceert een geldige functionele interpretatie voor affine eindige-type rekenkunde ($N\text{-}HA^\omega_{aff}$). De geëxtraheerde realizers en uitdaging-grenzen voldoen aan een vertaling van de bronformule in het doelsysteem.
  • Volledige Geldigheid (Theorem 22): Indien een informatie-nucleus is uitgerust met een geschikte contractiestructuur, breidt de interpretatie zich uit naar volledige eindige-type rekenkunde ($N\text{-}HA^\omega$) en systemen met observationele gelijkheid ($HA^\omega_{obs}$).
• Herstel van Bekende Interpretaties: Het kader verenigt bestaande interpretaties als specifieke instanties van informatie-nuclei en contractiestructuren:
  • Exacte Informatie-nucleus: Waarbij $\sigma^\sharp \equiv \sigma$ en compatibiliteit gelijkheid is. Gecombineerd met een "selectie"-contractiestructuur (het kiezen van één van de twee uitdagingen op basis van beslisbaarheid), herstelt dit de standaard Dialectica-interpretatie over $HA^\omega_{obs}$.
  • Eindige Kandidaat-nucleus: Waarbij $\sigma^\sharp$ eindige collecties van kandidaten representeert en compatibiliteit lidmaatschap is. Gecombineerd met een "merging"-contractiestructuur (de unie van collecties), levert dit een Herbrand-stijl interpretatie op.
• Verrijking van Realizers: Een significante technische resultaat is het vermogen om geëxtraheerde realizers systematisch te verrijken met hulpgegevens. Door te kiezen voor een informatie-nucleus waarbij de informatie-objecten extra structuur dragen, propageert het extractieproces deze data op natuurlijke wijze.
  • Continuïteitsvoorbeeld: Het artikel demonstreert dit met een "continuïteits-nucleus" waarbij de informatie-objecten bestaan uit een waarde en een modulus van continuïteit. De resulterende interpretatie extraheert realizers die niet alleen getuigen berekenen, maar ook continuïteitsdata op puntniveau dragen, afgeleid op compositionele wijze uit het bewijs in plaats van via nabewerking.

Betekenis en Claims
Het artikel claimt een "uniforme methode te bieden voor het specificeren van de informatie die door geëxtraheerde realizers wordt gedragen." In tegenstelling tot eerdere verenigende kaders die zoeken naar het herstellen van alle interpretaties via een enkele complexe parametrisering, isoleert deze benadering een minimale algebraïsche interface voor het affine component en identificeert het de precieze extra structuur die nodig is voor contractie.

De auteurs benadrukken dat dit modulaire perspectief de specificatie van informatie scheidt van de structurele afhandeling van gedupliceerde aannames. Deze scheiding maakt het mogelijk om de extractie van functionele interpretaties systematisch te verrijken met hulpgegevens (zoals continuïteitsinformatie) door simpelweg de informatie-nucleus te wijzigen, zonder de onderliggende logische machinerie van de extractie aan te passen. Het artikel laat de behandeling van extensionaliteit expliciet over aan toekomstig werk, waarbij wordt opgemerkt dat het huidige kader weliswaar de standaard Dialectica-interpretatie over observationele gelijkheid herstelt, maar nog geen zwakke of volledige extensionaliteitsregels adresseert.

Het werk is gepositioneerd als een verfijning van de "verenigende" en "geparameteriseerde" programma's (bijv. door Oliva en medewerkers), en biedt een meer fijnmazige algebraïsche scheiding die de propagatie van aanvullende computationele data door bewijzen faciliteert.