Cours 11: Réseaux de preuves

Réseaux de preuves pour MLL

Fragment M(ultiplicative) L(inear) L(ogic) de la logique linéaire

MLL sans unités ($1$ et $⊥$) (IMLL: intuitionniste):

\[A, B ≝ \; X \mid X^⊥ \mid A \otimes B \mid A ⅋ B\]

Calcul des séquents pour ce fragment

\[\cfrac{}{⊢ A^⊥, A} \; ax\] \[\cfrac{⊢ Γ, A \qquad ⊢ Δ, A^⊥}{⊢ Γ, Δ} \; cut\] \[\cfrac{⊢ Γ, A \qquad ⊢ Δ, B}{⊢ Γ, Δ, A \otimes B} \; \otimes\] \[\cfrac{⊢ Γ, A, B}{⊢ Γ, A ⅋ B} \; \otimes\]

Qu’est-ce qu’une preuve dans cette logique ?

⟶ Réponse naïve: un arbre de dérivation (comme d’habitude).

MAIS pour montrer $⊢ A ⅋ B, C ⅋ D$ à partir de $⊢ A, B, C, D$, on peut déjà appliquer $⅋$ à $A$ et $B$, puis à $C$ et $D$ OU dans l’ordre inverse.

On peut faire la même chose avec le tenseur et la coupure (si on a $A$ implique $B$/ $B$ implique $C$/ $C$ implique $D$ ⟶ on a deux manières d’appliquer le modus ponens deux fois de suite).

Ces preuves ne sont pas les mêmes, elles sont distinguées par le calcul des séquents, mais c’est embêtant, on aimerait avoir une propriété “d’associativité” qui nous permettrait d’identifier ces preuves (qui sont sensiblement les mêmes, on le voit bien) ⟹ on voudrait définir ll’essence d’une preuve.

Les Réseaux de preuves capturent cette essence.

Dans les règles du calcul des séquents: les contextes $Γ, Δ$ n’“agissent pas” ⟶ on aimerait ne pas les expliciter.

⟹ Calcul graphique (cf. photos) ⟶ on voudrait écrire ces règles comme des gadgets grapiques/des graphes (que Girard appelle des liens).

• orientation: du haut vers le bas
• arêtes entrantes: premisses
  • ex: axiome: 0 prémisse
• arêtes sortantes: conclusions
  • ex: axiome: 2 conclusions

NB: Attention: les prémisses sont orientés, il y a un prémisse gauche, et un droit, CAR la commutativité est vraie modulo un isomorphisme naturel

\[A \otimes B ≃ B \otimes A\\ (A \otimes B) \otimes C ≃ A \otimes (B \otimes C)\]

  digraph {
    rankdir=TB;
    bl[label="", shape=none]
    π -> bl[label="A_1"];
  }

Les réseaux forment une catégorie, dont la composition est la coupure.

Déséquentialisation

A toute preuve $δ$ dont les conclusions sont $⊢ A_1, ⋯, A_n$, on associe un réseau $des(δ)$

  digraph {
    rankdir=TB;
    bl1[label="", shape=none]
    bl2[label="", shape=none]
    "des(δ)" -> bl1[label="A_1"];
    "des(δ)" -> bl2[label="A_n"]
  }

On définit

$δ \sim δ’$:

si $des(δ) = des(δ’)$

Prop: $\sim$ est exactement l’équivalence engendrée par les commutations de règles “parallèles” (parr et parr, tenseur et tenseur, cut et cut, parr et tenseur, parr et coupure)

NB: la coupure est comme le tenseur, d’un point de vue structurel

D’ailleurs, c’est exactement l’équivalence qui assure la confluence de l’élimination des coupures.

Confluence (Church-Rosser):

Si $M ⟶^\ast M’$ et $M ⟶^\ast M’’$, alors il existe $N$ tel que $M’, M’’ ⟶^\ast N$

Le $λ-calcul avec l’élimination des coupures n’est pas confluent, pour des raisons “bêtes” (raisons qu’on élimine avec les réseaux) ⟶ en revanche, on a “confluence modulo”

\[\begin{xy} \xymatrix{ M \ar[r]^\ast \ar[d]_\ast & M' \ar[d]^\ast \\ M'' \ar[r]_\ast & N' \sim N'' } \end{xy}\]

Elimination des coupures dans les réseaux:

On a des diagrammes de cordes dans les réseaux de preuves (cf. photos).

Séquentialisation

MLL satisfait l’élimination des coupures ⟹ donc par la propriété de la sous-formule, le séquent vide n’est pas démontrable.

MAIS Attention: si on applique une coupure à un axiome, on “démontre” le séquent vide (le réseau correspondant a une forme de preuve).

Structure de preuve (Proof structure) ⟺ Réseaux (Net) ⟺ Pseudo-preuves:

réseaux, qui ne correspondent pas forcément à une preuve

Réseaux de preuve (Proof net):

réseaux qui correspondent à une preuve

NB: la réécriture des réseaux est “non typée” ⟶ la structure logique/réécriture existe “avant” les formules (les blocs initiaux sont les règles de réécriture, plus les formules).

Un réseau est séquentialisable:

s’il est dans l’image de $des$

Un réseau de preuve:

est un réseau dont tous les graphes de correction sont connexes et acycliques (AC(yclic) C(onnex) ⟶ définition due à Danos et Regnier (1988))

Graphe de correction: on définit un switching (i.e. un choix pour d’un prémisse pour chaque parr du réseau). Un switching $S$ pour un réseau $π$ induit un multigraphe appelé graphe de correction de $S$, noté $G_S(π)$

Théorème de Séquentialisation: Un réseau est séquentialisable ssi il est un réseau de preuve

NB: c’est très élégant, parce que la définition des réseaux de preuves n’utilise pas le calcul des séquents.

⟹ Critère de correction: on isole les réseaux de preuves parmi les réseaux de manière “structurelle” (i.e. sans parler du calcul des séquents).

La caractéristique d’Euler-Poincaré (vraie pour les multigraphes)

\[\text{nb noeuds} - \text{nb arêtes} = \text{nb composantes conn.} - \text{nb cycles}\]

permet de montrer que les réseaux de preuves sont stables par élémination des coupures.

Réseaux de preuves pour toute la logique linéaire

On ne veut plus se limiter à MLL.

Mais il y a un souci: la règle de promotion (parmi les exponentiels) et la règle du $\&$ (parmi les additifs) sont sensibles au contexte ! (on ne peut plus se contenter d’une définition locale)

Les unités ($1$ et $⊥$) posent énormément problème ⟶ on n’a plus de critère de correction comme ACC ! En effet, le $⊥$ tout seul n’est pas un réseau de preuve, mais concaténé avec un réseau de preuve, on a encore un réseau de preuve.

NB: Décider de l’équivalence

\[δ \sim δ'\]

est PSPACE-complet, donc il n’y a pas de critère de correction simple pour les réseaux de preuve !

De plus: la correction ACC (décider si un réseau n’est pas un réseau de preuve) est dans $coNP$ (il suffit de deviner un switching).

Donc à moins que $coNP = PSPACE$, on n’a pas de critère de correction ACC avec les unités.

Pire encore: il existe un critère de correction linéaire !

M(ultiplicative) E(Exponential) LL + mix

Solution de fortune: on ajoute les règles

\[\cfrac{⊢Γ \qquad ⊢ Δ}{⊢ Γ, Δ} \; mix\] \[\cfrac{}{⊢} \; mix_0\] \[A, B ≝ X \mid X^⊥ \\ \mid A \otimes B \mid 1 \\ \mid A ⅋ B \mid ⊥ \\ \mid !A \mid ?A\]

Le critère est maintenant AC (acyclique seulement), et s’applique récursivement dans chaque boîte.

Sémantique du $λ$-calcul dans les réseaux de preuves

Chaque $λ$-terme devient un réseau de preuve, qui a une conclusion supplémentaire non étiquetée représentant la racine du $λ$-terme.

Les rédex induisent des coupures par tenseur.

Les substitutions explicites viennent de là.