Towards Weak Stratification for Logics of Definitions

Résumé technique : Vers une stratification faible pour les logiques de définitions

Énoncé du problème
La logique des définitions est une famille de logiques utilisées pour encoder et raisonner sur des jugements spécifiés par des règles d'inférence, où les prédicats atomiques sont associés à des formules logiques pouvant dépendre du prédicat lui-même. Pour résoudre la circularité apparente inhérente à de telles définitions, les approches standards imposent une condition de stratification, garantissant qu'un prédicat n'apparaît pas négativement (à gauche d'une implication) dans le corps de sa propre définition. Cette condition traite effectivement les définitions comme des opérateurs de point fixe monotones.

Cependant, de nombreuses spécifications utiles, particulièrement celles impliquant des relations logiques pour prouver des propriétés de langages de programmation, nécessitent des définitions où le prédicat apparaît négativement. Dans la logique $\mathcal{G}$, qui sous-tend l'assistant de preuve Abella, de telles définitions sont proscrites. Tiu [19] a précédemment introduit une logique appelée $\mathcal{LD}$ qui assouplit la condition de stratification vers une stratification faible (autorisant les occurrences négatives à condition que le niveau de la tête soit strictement supérieur au niveau de l'occurrence négative), mais $\mathcal{LD}$ était limitée à un fragment central. Elle manquait du support pour le quantificateur nabla ($\nabla$), essentiel pour raisonner sur les noms et la fraîcheur via des constantes nominales, ainsi que pour les définitions inductives générales au-delà de l'induction sur les entiers naturels. Le défi abordé dans ce travail est d'étendre la logique des définitions pour inclure la stratification faible tout en maintenant la cohérence en présence de $\nabla$ et de définitions inductives générales.

Méthodologie
Le papier définit une nouvelle logique, $\mathcal{LD}\mu\nabla$, qui étend $\mathcal{LD}$ de Tiu avec la quantification nabla et les définitions inductives générales. La méthodologie se déroule en trois étapes principales :

1. Syntaxe et sémantique de $\mathcal{LD}\mu\nabla$ :
   La logique est formulée comme une extension du calcul de séquents du premier ordre avec un ensemble de définitions $\mathcal{D}$ et un ensemble de définitions inductives $\mathcal{I}$.

   • Stratification faible : Un ensemble de définitions $\mathcal{D}$ est faiblement stratifié si, pour chaque clause $H \triangleq_X B$ et toute substitution de base $\rho$, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Crucialement, cela permet des occurrences négatives du prédicat défini si le niveau de la tête est strictement supérieur au niveau de l'occurrence négative.
   • Stratification stricte pour l'induction : Le papier impose une condition plus stricte sur les définitions inductives $\mathcal{I}$ : elles doivent être strictement stratifiées (le niveau d'un prédicat atomique de base doit être indépendant de ses arguments). Cette restriction est nécessaire pour prévenir l'incohérence lors de la combinaison de l'induction avec la stratification faible.
   • Quantificateur Nabla : La logique incorpore le quantificateur $\nabla$ pour gérer les constantes nominales et la fraîcheur, distinguant les instances génériques et spécifiques de noms.

2. Logique de base et interprétation :
   Pour prouver la cohérence, les auteurs construisent une version de base de la logique, $\mathcal{LD}\mu\nabla_\infty$, où toutes les formules sont de base (sans variables propres).

   • Lemme de base (Grounding Lemma) : Une étape technique clé consiste à prouver que toute dérivation dans $\mathcal{LD}\mu\nabla$ peut être interprétée comme une dérivation dans $\mathcal{LD}\mu\nabla_\infty$ via une substitution de base. Cela réduit le problème de cohérence de la logique complète à la cohérence de la logique de base.
   • Règles infinitaires : Dans $\mathcal{LD}\mu\nabla_\infty$, les règles standard $\forall R$ et $\exists L$ sont remplacées par des règles infinitaires qui quantifient sur tous les termes de base, et la règle $\mu L$ pour l'induction est de la même manière étendue pour couvrir toutes les instances de base.

3. Élimination du cut :
   Le cœur de la preuve de cohérence est l'élimination de la règle de cut (spécifiquement la règle de multicut) dans $\mathcal{LD}\mu\nabla_\infty$.

   • Relation de réduction : Une relation de réduction est définie sur les dérivations, spécifiant comment les cuts peuvent être poussés vers le haut ou éliminés.
   • Réductibilité : Suivant la technique de Tait-Martin-Löf adaptée par McDowell et Miller, les auteurs définissent une notion de réductibilité (et de normalisabilité) pour les dérivations. Ils prouvent que toute dérivation dans $\mathcal{LD}\mu\nabla_\infty$ est réductible.
   • Gestion des cas inductifs : Un aspect critique de la preuve est la gestion de l'interaction entre la stratification faible et l'induction. Les auteurs montrent que si la stratification faible suffit pour les définitions générales, les définitions inductives doivent rester strictement stratifiées. Ils fournissent un contre-exemple (Section 3.3) démontrant que permettre des définitions inductives faiblement stratifiées mène à l'incohérence logique.

Contributions clés

• Définition de $\mathcal{LD}\mu\nabla$ : Le papier définit formellement une logique qui combine la stratification faible, la quantification nabla et les définitions inductives générales.
• Preuve de cohérence : La contribution principale est la preuve que $\mathcal{LD}\mu\nabla$ est cohérente. Ceci est accompli en prouvant l'élimination du cut pour la logique de base $\mathcal{LD}\mu\nabla_\infty$ et en établissant une interprétation de base.
• Contraintes de stratification : Le travail clarifie la frontière entre les définitions permises et impermises. Il démontre que si la stratification faible suffit pour les définitions générales (permettant les relations logiques), les définitions inductives requièrent une stratification stricte pour préserver la cohérence.
• Contre-exemple : Le papier fournit un contre-exemple spécifique montrant que relâcher la condition de stratification pour les définitions inductives conduit à l'incohérence logique, justifiant la restriction imposée sur $\mathcal{I}$.

Résultats

• Cohérence : La logique $\mathcal{LD}\mu\nabla$ est prouvée cohérente. Par conséquent, la logique $\mathcal{LD}\mu\nabla_\infty$ admet des dérivations sans cut pour tous les séquents prouvables.
• Propriétés d'inversion : Le papier établit des propriétés méta-théoriques pour $\mathcal{LD}\mu\nabla_\infty$, incluant l'invertibilité de diverses règles d'introduction (ex: $\wedge R$, $\vee L$, $\nabla R$) et une partialité d'invertibilité spécifique pour $\vee R$, $\exists R$, et les règles de définition ($\Delta R$) lorsque le contexte est vide. Ces propriétés sont cruciales pour les procédures de recherche de preuve.
• Limitations : Le théorème d'élimination du cut est établi uniquement pour la logique de base $\mathcal{LD}\mu\nabla_\infty$. Le papier note que l'extension de ce résultat à la logique complète $\mathcal{LD}\mu\nabla$ (avec variables propres) reste un défi ouvert.

Signification
La signification de ce travail réside dans son potentiel à étendre les capacités de l'assistant de preuve Abella. Abella est basé sur la logique $\mathcal{G}$, qui restreint actuellement les définitions à être strictement stratifiées. En justifiant l'inclusion de définitions faiblement stratifiées, cette recherche ouvre la voie à ce qu'Abella supporte nativement les relations logiques, une technique fondamentale pour prouver des propriétés sémantiques de langages de programmation (telles que la sûreté de type et la correction de compilateur).

Le papier positionne ce travail comme une étape fondamentale vers une extension plus large de $\mathcal{G}$. Bien que le résultat actuel traite la stratification faible avec $\nabla$ et l'induction, les auteurs notent qu'une justification complète pour Abella nécessiterait des extensions supplémentaires pour inclure la co-induction et l'abstraction nominale. Le travail souligne également la nécessité de maintenir une stratification stricte pour les définitions inductives, une contrainte qui empêche les incohérences qui surgiraient autrement en mélangeant la stratification faible avec l'induction.