A Classical Linear $λ$-Calculus based on Contraposition

Technische Samenvatting: Een Klassieke Lineaire $\lambda$-calculus gebaseerd op Contrapositie

Probleemstelling
Het artikel behandelt de uitdaging om de klassieke symmetrieën van Lineaire Logica (LL) te harmoniseren met de computationele formalisering van de $\lambda$-calculus. Hoewel Lineaire Logica sterke symmetrieën vertoont (bijv. dualiteit tussen linker- en rechterregels, involutieve negatie waarbij $\neg\neg A = A$), falen standaard natuurlijke deductie-presentaties vaak in het behouden van deze symmetrieën terwijl ze goede computationele eigenschappen zoals convergentie en sterke normalisatie behouden. Bestaande systemen vallen doorgaans in twee categorieën:

1. Intuïtionistische fragmenten: Systemen zoals ILL of DILL beperken de logica tot single-conclusion sequenten, waardoor klassieke symmetrieën verloren gaan en het vermogen om bepaalde bewijzen te modelleren wordt beperkt.
2. Sequent-gebaseerde systemen: Systemen afgeleid van de sequentencalculus (bijv. proof-nets, process calculi) behouden symmetrieën maar behandelen bewijzen vaak als parallelle processen in plaats van functionele programma's, wat ze minder geschikt maakt voor functionele programmeerparadigma's.

Specifiek merken de auteurs op dat in klassieke logica het bevestigen van een propositie $A$ als thesis equivalent is aan het ontkennen ervan als hypothese. In de context van Lineaire Logica betekent dit dat $A \multimap B$ en $B^\perp \multimap A^\perp$ dezelfde bewijzen moeten delen. Echter, standaard $\lambda$-calculi voor klassieke logica (zoals Parigot's $\lambda\mu$) zijn confluent maar niet-symmetrisch (negatie is niet involutief), terwijl symmetrische systemen (zoals die van Barbanera en Berardi) vaak een gebrek aan convergentie vertonen. Het artikel streeft naar een single-conclusion natuurlijke deductie systeem voor Multiplicatieve Exponentiële Lineaire Logica (MELL) dat de klassieke symmetrieën behoudt en tevens beschikt over standaard eigenschappen van getypeerde programmeertalen.

Methodologie
De auteurs stellen een nieuwe term-toewijzing voor MELL voor, genaamd de $\lambda$MELL-calculus, geworteld in het "proposities-als-typen" paradigma. De kernmethodologie omvat:

1. Logisch Fundament: Vertrekkend vanuit het intuïtionistische fragment van Multiplicatieve Lineaire Logica (MLL), introduceren de auteurs een lineaire modus tollens regel. Terwijl de standaard lineaire implicatie-eliminatie (modus ponens) het afleiden van $B$ uit $A \multimap B$ en $A$ mogelijk maakt, maakt de nieuwe regel het mogelijk om $A^\perp$ af te leiden uit $A \multimap B$ en $B^\perp$. Deze toevoeging herstelt de klassieke MLL.
2. Nieuwe Operatie: Contra-substitutie: Om een computationele interpretatie te bieden voor de modus tollens regel, definiëren de auteurs een nieuwe operatie genaamd contra-substitutie, aangeduid als $t\{a \backslash s\}$.
   • Intuïtie: Waar standaard substitutie $t\{a := s\}$ een unieke occurence van variabele $a$ in $t$ vervangt door $s$, "grijpt" contra-substitutie de unieke occurence van $a$ in $t$ en "trekt" eruit, wat effectief het term $t$ "binnenstebuiten" keert (zoals een sok) voordat $a$ met $s$ wordt vervangen.
   • Mechanisme: Deze operatie wordt gedefinieerd via structurele inductie op lineaire termen. Bijvoorbeeld, als $t = \langle u, a \rangle$ en $s : A \multimap B^\perp$, dan resulteert $\langle u, a \rangle\{a \backslash s\}$ in $s \bullet u : B^\perp$.
3. Calculus Constructie: De calculus bevat standaard lineaire constructen (tensor, lineaire implicatie, lambda-abstractie) naast de nieuwe contra-applicatie ($t \blacktriangledown s$), die overeenkomt met de modus tollens eliminatie. Voor MELL wordt de calculus uitgebreid met exponentiële modaliteiten ($!$ en $?$) en eenheden, wat een verfijnde definitie van lineariteit en een structurele equivalentierelatie vereist.
4. Structurele Equivalentie: Om convergentie te waarborgen in de aanwezigheid van exponenten en complexe reductiepaden, definiëren de auteurs een structurele equivalentie ($\equiv$) die fungeert als een sterke bisimulatie met betrekking tot pre-reductie. Deze equivalentie bevat axioma's voor het propageren van eliminatoren en het afhandelen van eenheden (bijv. $t[\star := s] \equiv s[\star := t]$ voor termen van type 1).

Belangrijkste Bijdragen

1. De $\lambda$MELL-calculus: Een one-sided natuurlijke deductie presentatie van MELL waar bewijzen worden gemodelleerd als functionele expressies. Het introduceert de contra-applicatie construct en de contra-substitutie operatie.
2. Soundness en Compleetheid: De auteurs bewijzen dat de calculus sound en compleet is ten opzichte van MELL. Specifiek kan elke geldige MELL sequent gelezen worden als een typing judgment in $\lambda$MELL door een willekeurige formule als thesis te selecteren en de negaties van de overige formules als hypothesen.
3. Metatheoretische Eigenschappen: De calculus voldoet aan de standaard eigenschappen van een getypeerde programmeertaal:
   • Subject Reduction: Reductie behoudt de typering.
   • Confluentie: De reductie-relatie is confluent (modulo structurele equivalentie).
   • Sterke Normalisatie: Elke reductie-sequentie termineert.
4. Encoding van Klassieke Systemen: Het artikel demonstreert dat verschillende bekende term-toewijzingen voor klassieke logica geëncodeerd kunnen worden in $\lambda$MELL, waaronder:
   • Parigot's $\lambda\mu$-calculus (via zowel T als Q translaties).
   • Curien en Herbelin's $\lambda\mu\tilde{\mu}$-calculus.
   • Hasegawa's $\mu$DCLL.

Resultaten
De primaire resultaten zijn de bewijzen van de metatheoretische eigenschappen. De auteurs vestigen sterke normalisatie met behulp van de techniek van reducibility candidates, waarbij sets van termen geassocieerd met elk type worden gedefinieerd. Confluentie wordt bewezen via Newman's Lemma door lokale confluentie vast te stellen, wat steunt op het feit dat de structurele equivalentie fungeert als een sterke bisimulatie voor pre-reductie. Het artikel levert eveneens constructieve bewijzen voor de volledigheid van de calculus, door aan te tonen hoe termen gerecupereerd kunnen worden uit cut-vrije MLL-derivaties.

Betekenis
Het artikel claimt significant te zijn door een "functionele" interpretatie van klassieke lineaire logica te bieden die de inherente symmetrieën behoudt zonder terug te vallen op process calculi of multi-conclusion natuurlijke deductie. Door de introductie van contra-substitutie bieden de auteurs een mechanisme om het klassieke principe van contrapositie computationeel af te handelen binnen een single-conclusion framework. Dit werk suggereert een fundament voor lineaire functionele programmeertalen en bewijsassistenten die van nature klassiek redeneren en resource-sensitiviteit kunnen ondersteunen. De auteurs merken op dat het uitbreiden van de aanpak naar additieve connectieven niet triviaal is vanwege de afhankelijkheid van lineariteit voor contra-substitutie, maar het huidige systeem handelt de multiplicatieve en exponentiële fragmenten succesvol af. Dit werk overbrugt de kloof tussen de symmetrie van de sequentencalculus en de functionele aard van $\lambda$-calculi.