Ordered Adjoint Logic (Extended Version)

Résumé technique de « Logique adjointe ordonnée »

Énoncé du problème
Les logiques ordonnées et les systèmes de types sont essentiels pour des applications allant de la linguistique computationnelle à la mise en application des protocoles de sécurité, où l'ordre d'utilisation des ressources est significatif. Dans la plupart des formulations, les types ordonnés sont également linéaires, exigeant que les ressources soient utilisées exactement une fois. Bien que des travaux antérieurs de Kanovich et al. aient étudié des calculs assouplissant cette contrainte via des sous-exponentielles au sein d'une logique ordonnée linéaire, cette approche repose sur un « mode de base » où toutes les inférences se produisent. Pour les logiques ordonnées, ce mode de base doit interdire toutes les règles structurelles (affaiblissement, contraction, échange), contraignant les applications à basculer fréquemment dans et hors de ce mode restrictif. De plus, les systèmes de sous-exponentielles existants n'explorent pas pleinement la possibilité de propriétés structurelles unilatérales (par exemple, la mobilité à gauche sans mobilité à droite). Les auteurs visent à généraliser ces cadres pour prendre en charge un préordre de modes aux propriétés structurelles variées et fines — incluant un contrôle indépendant de l'affaiblissement, de la contraction à gauche/droite et de la mobilité à gauche/droite — sans dépendre d'un unique mode de base restrictif.

Méthodologie
Les auteurs introduisent la Logique adjointe ordonnée, un système qui combine la flexibilité structurelle des modalités adjointes avec les contraintes d'ordre des logiques ordonnées. La méthodologie procède en deux étapes principales :

1. Formulation en calcul des séquents :
   Les auteurs définissent un calcul des séquents où les antécédents sont des séquences ordonnées d'hypothèses étiquetées. Les règles structurelles ne sont pas globales mais régies par un préordre de modes ($k \geq m$). Chaque mode $m$ est associé à un ensemble de propriétés structurelles $\sigma(m) \subseteq \{W, C, M_{\leftarrow}, M_{\rightarrow}\}$ (Affaiblissement, Contraction, Mobilité à gauche, Mobilité à droite).

   • Modalités de bascule : Au lieu d'un mode de base, le système utilise des modalités de bascule ($\downarrow^k_m$ et $\uparrow^m_l$) pour passer d'un raisonnement à un autre selon les modes. Ces bascules sont dérivées de la logique adjointe de Benton mais généralisées pour gérer des contextes ordonnés.
   • Règles structurelles : Les auteurs décomposent la mobilité et la contraction en variantes unilatérales. Les règles de mobilité permettent à une seule proposition de se déplacer arbitrairement loin vers la gauche ou la droite au sein de la séquence d'antécédents, à condition que le mode de la proposition admette la mobilité directionnelle correspondante. La contraction est autorisée de manière non locale (fusion de doublons non adjacents) pour assurer l'élimination de la coupure, distincte de la contraction locale dans la logique linéaire standard.
   • Connecteurs logiques : Le langage inclut des implications ordonnées ($\multimap$ et $\multimap$), des conjonctions fusionnées et tordues, et des bascules. Les règles sont paramétrées par leurs modes, avec des conditions spécifiques assurant la préservation de l'indépendance des modes (par exemple, $k \geq m \geq r$) lors de la lecture des règles de la conclusion vers les prémisses.

2. Déduction naturelle et décidabilité :
   Les auteurs passent à une formulation en déduction naturelle où les règles structurelles sont implicites, visant une fondation adaptée aux langages de programmation.

   • Explicite vs Implicite : Initialement, ils présentent un système avec des règles structurelles explicites pour combler l'écart avec le calcul des séquents. Ils définissent ensuite un système où les règles structurelles (affaiblissement, contraction, mobilité) sont implicites.
   • Algorithme de vérification de preuves : Pour traiter le non-déterminisme introduit par les règles structurelles implicites (spécifiquement l'application illimitée de l'affaiblissement et le placement des variables dans les règles d'élimination), les auteurs définissent un jugement de « forme normale » ($\Omega \gg_{\Gamma, r} \Omega_{nf}$). Cet algorithme calcule l'ensemble de toutes les formes normales possibles (contextes sans variables répétées) pour un contexte donné $\Omega$, un ensemble d'hypothèses $\Gamma$ et un mode $r$.
   • Jugements basés sur des ensembles : Les règles de déduction naturelle sont relevées pour opérer sur des ensembles de contextes en forme normale ($\Xi$). Par exemple, l'introduction de la conjonction calcule le produit cartésien des ensembles de contextes, tandis que l'intersection est utilisée pour les règles nécessitant un accord de contexte (comme la conjonction additive).

Contributions clés

• Logique adjointe généralisée : L'article généralise la logique adjointe aux contextes ordonnés, introduisant un préordre de modes où chaque mode contrôle indépendamment l'affaiblissement, la contraction et la mobilité unilatérale.
• Propriétés structurelles unilatérales : Le système modélise et prouve explicitement les propriétés de la mobilité et de la contraction à gauche et à droite comme des propriétés structurelles séparées et indépendantes, une fonctionnalité anticipée mais non explorée dans les travaux antérieurs sur les sous-exponentielles.
• Élimination de la coupure : Les auteurs prouvent que le calcul des séquents adjoint ordonné admet l'élimination de la coupure (via la multicoupure) et l'élimination de l'identité, établissant le système comme un cadre logique bien comporté.
• Décidabilité de la vérification de preuves : L'article fournit un système de déduction naturelle avec des règles structurelles implicites et prouve que la vérification de preuves pour ce système est décidable. Cela est réalisé en construisant un algorithme terminant qui calcule l'ensemble des contextes en forme normale.

Résultats

• Correction théorique : Le calcul des séquents est montré satisfaisant l'élimination de la coupure et de l'identité. Le système de déduction naturelle est prouvé correct et complet par rapport au calcul des séquents.
• Décidabilité : L'algorithme de calcul des formes normales ($NF_{\Gamma, r}(\Omega)$) est prouvé terminant. Par conséquent, le problème de la vérification des preuves dans le système de déduction naturelle implicite est décidable.
• Subsumption substructurelle : Les résultats impliquent la décidabilité de la subsumption substructurelle, un composant central des algorithmes de vérification de types pour des langages comme QRTT (qui utilise la sémantique de Kripke avec des mondes explicites).

Signification et revendications
Les auteurs affirment que la Logique adjointe ordonnée fournit une fondation adaptée à un langage de programmation adjoint expressif ou à un cadre logique. En découplant les propriétés structurelles d'un unique mode de base et en utilisant des bascules adjointes, le système permet un raisonnement natif dans diverses disciplines (linéaire, ordonnée, illimitée) avec des basculements transparents. La décidabilité de la vérification de preuves avec des règles structurelles implicites est soulignée comme une étape critique vers la mise en œuvre de vérificateurs de types bidirectionnels pour les langages de programmation fonctionnelle capables de gérer des propriétés structurelles fines du code. L'article note que bien que la procédure de décision soit établie, l'efficacité pratique (par exemple, éviter la complexité exponentielle due à des affaiblissements inutiles) reste un sujet pour une optimisation future. Le travail est présenté comme une généralisation directe de la logique ordonnée à sous-exponentielles de Kanovich et al. et une extension des types adjoints de Jang et al. pour inclure l'ordre.