A Classical Linear $λ$-Calculus based on Contraposition

Résumé Technique : Un $\lambda$-calcul classique linéaire basé sur la contraposition

Énoncé du Problème
L'article traite du défi consistant à harmoniser les symétries classiques de la Logique Linéaire (LL) avec le formalisme computationnel du $\lambda$-calcul. Bien que la Logique Linéaire présente de fortes symétries (par exemple, la dualité entre les règles à gauche et à droite, la négation involutive où $\neg\neg A = A$), les présentations classiques de la déduction naturelle échouent souvent à préserver ces symétries tout en maintenant de bonnes propriétés computationnelles telles que la confluence et la normalisation forte. Les systèmes existants se classent généralement en deux catégories :

1. Fragments intuitionnistes : Des systèmes comme l'ILL ou le DILL restreignent la logique à des séquents à conclusion unique, perdant ainsi les symétries classiques et la capacité de modéliser certains de preuves.
2. Systèmes basés sur les séquents : Les systèmes dérivés du calcul des séquents (par exemple, les réseaux de preuves, les calculs de processus) préservent les symétries mais traitent souvent les preuves comme des processus parallèles plutôt que comme des programmes fonctionnels, ce qui les rend moins adaptés aux paradigmes de programmation fonctionnelle.

Plus précisément, les auteurs notent que dans la logique classique, affirmer une proposition $A$ comme thèse est équivalent à nier $A$ comme hypothèse. Dans le contexte de la Logique Linéaire, cela implique que $A \multimap B$ et $B^\perp \multimap A^\perp$ doivent partager les mêmes preuves. Cependant, les $\lambda$-calculs classiques standards (comme le $\lambda\mu$ de Parigot) sont confluents mais non symétriques (la négation n'est pas involutive), tandis que les systèmes symétriques (comme ceux de Barbanera et Berardi) manquent souvent de confluence. L'article cherche un système de déduction naturelle à conclusion unique pour la MELL (Multiplicative Exponential Linear Logic) qui conserve les symétries classiques et jouit des propriétés standards des langages de programmation typés.

Méthodologie
Les auteurs proposent une nouvelle assignation de termes pour la MELL, nommée le calcul $\lambda$MELL, fondée sur le paradigme « propositions-en-types ». La méthodologie centrale comprend :

1. Fondement Logique : En partant du fragment intuitionniste de la Logique Linéaire Multiplicative (MLL), les auteurs introduisent une règle de modus tollens linéaire. Alors que l'élimination standard de l'implication linéaire (modus ponens) permet de dériver $B$ à partir de $A \multimap B$ et $A$, la nouvelle règle permet de dériver $A^\perp$ à partir de $A \multimap B$ et $B^\perp$. Cette addition permet de récupérer la MLL classique.
2. Opération Nouvelle : La Contra-Substitution : Pour fournir une interprétation computationnelle de la règle du modus tollens, les auteurs définissent une nouvelle opération appelée contra-substitution, notée $t\{a \backslash s\}$.
   • Intuition : Si la substitution standard $t\{a := s\}$ remplace une occurrence unique de la variable $a$ dans $t$ par $s$, la contra-substitution « attrape » l'occurrence unique de $a$ dans $t$ et « tire » de celle-ci, retournant efficacement le terme $t$ « à l'envers » (comme une chaussette) avant de remplacer $a$ par $s$.
   • Mécanisme : Cette opération est définie par induction structurelle sur les termes linéaires. Par exemple, si $t = \langle u, a \rangle$ et $s : A \multimap B^\perp$, alors $\langle u, a \rangle\{a \backslash s\}$ résulte en $s \bullet u : B^\perp$.
3. Construction du Calcul : Le calcul inclut les constructions linéaires standards (tensor, implication linéaire, abstraction lambda) aux côtés de la nouvelle contra-application ($t \blacktriangledown s$), qui correspond à l'élimination du modus tollens. Pour la MELL, le calcul est étendu pour inclure les modalités exponentielles ($!$ et $?$) et les unités, nécessissant une définition raffinée de la linéarité et une relation d'équivalence structurelle.
4. Équivalence Structurelle : Pour assurer la confluence en présence d'exponentielles et de chemins de réduction complexes, les auteurs définissent une équivalence structurelle ($\equiv$) qui agit comme une forte bisimulation par rapport à la pré-réduction. Cette équivalence inclut des axiomes pour propager les éliminateurs et gérer les unités (par exemple, $t[\star := s] \equiv s[\star := t]$ pour les termes de type 1).

Contributions Clés

1. Le Calcul $\lambda$MELL : Une présentation à un côté de la déduction naturelle pour la MELL où les preuves sont modélisées comme des expressions fonctionnelles. Il introduit la construction de contra-application et l'opération de contra-substitution.
2. Correction et Complétude : Les auteurs prouvent que le calcul est correct et complet par rapport à la MELL. Spécifiquement, tout séquent MELL valide peut être lu comme un jugement de typage dans $\lambda$MELL en sélectionnant n'importe quelle formule comme thèse et les négations des autres comme hypothèses.
3. Propriétés Métathéoriques : Le calcul satisfait les propriétés standards d'un langage de programmation typé :
   • Réduction de Type (Subject Reduction) : La réduction préserve le typage.
   • Confluence : La relation de réduction est confluente (modulo l'équivalence structurelle).
   • Normalisation Forte : Toute séquence de réduction se termine.
4. Encodage de Systèmes Classiques : L'article démontre que plusieurs assignations de termes bien connues pour la logique classique peuvent être encodées dans $\lambda$MELL, notamment :
   • Le $\lambda\mu$-calcul de Parigot (via les traductions T et Q).
   • Le $\lambda\mu\tilde{\mu}$-calcul de Curien et Herbelin.
   • Le $\mu$DCLL de Hasegawa.

Résultats
Les principaux résultats sont les preuves des propriétés métathéoriques. Les auteurs établissent la normalisation forte en utilisant la technique des candidats de réductibilité, en définissant des ensembles de termes associés à chaque type. La confluence est prouvée via le lemme de Newman en établissant la confluence locale, qui repose sur l'équivalence structurelle agissant comme une forte bisimulation pour la pré-réduction. L'article fournit également des preuves constructives pour la complétude du calcul, montant comment récupérer les termes à partir des dérivations sans coup de la MLL.

Signification
L'article revendique sa signification en offrant une interprétation « fonctionnelle » de la logique linéaire classique qui préserve ses symétries inhérentes sans recourir aux calculs de processus ou à la déduction naturelle à conclusions multiples. En introduisant la contra-substitution, les auteurs fournissent un mécanisme pour gérer computationnellement le principe classique de contraposition au sein d'un cadre à conclusion unique. Ce travail suggère une base pour les langages de programmation fonctionnelle linéaire et les assistants de preuve pouvant supporter nativement le raisonnement classique et la sensibilité aux ressources. Les auteurs notent que l'extension de l'approche aux connecteurs additifs est non triviale en raison de la dépendance de la contra-substitution à la linéarité, mais que le système actuel gère avec succès les fragments multiplicatifs et exponentiels. Ce travail comble le fossé entre la symétrie du calcul des séquents et la nature fonctionnelle des $\lambda$-calculs.