Comment dois-je penser aux filets de preuve?

Dans sa réponse à cette question , Stéphane Gimenez m'a signalé un algorithme de normalisation polynomiale en temps pour les preuves en logique linéaire. La preuve dans l'article de Girard utilise des réseaux de preuve, qui sont un aspect de la logique linéaire que je ne connais pas vraiment.

Maintenant, j'ai essayé de lire des articles sur des filets de preuve auparavant (comme les notes de Pierre-Louis Curien à leur sujet), mais je ne les ai pas vraiment compris. Ma question est donc la suivante: comment dois-je y penser? Par "comment penser à eux", je veux dire à la fois l'intuition informelle derrière eux (par exemple, comment ils se comportent par calcul, ou comment ils sont liés aux séquences), et aussi les théorèmes à leur sujet que je devrais prouver par moi-même pour vraiment les obtenir.

En répondant à cette question, vous pouvez supposer (1) que je connais bien la théorie de la preuve de la logique linéaire (y compris des choses comme le déroulement de la preuve d'élimination des coupures, et sous forme focalisée également), (2) leur sémantique catégorique en termes d'espaces de cohérence ou via la convolution Day, et (3) les rudiments très basiques de la construction du GoI.

Les filets de preuve sont intéressants essentiellement pour trois raisons:

1) IDENTITÉ DES PREUVES. Ils apportent une réponse au problème "quand deux preuves sont-elles identiques"? Dans le calcul séquentiel, vous pouvez avoir de nombreuses preuves différentes de la même proposition qui ne diffèrent que parce que le calcul séquentiel force un ordre parmi les règles de déduction même lorsque cela n'est pas nécessaire. Bien sûr, on peut ajouter une relation d'équivalence sur les preuves de calcul séquentiel, mais il faut ensuite montrer que l'élimination des coupures se comporte correctement sur les classes d'équivalence, et il est également nécessaire de se tourner vers la réécriture modulo, qui est bien plus technique que la réécriture ordinaire. Les réseaux de preuve résolvent le problème du traitement des classes d'équivalence en fournissant une syntaxe où chaque classe d'équivalence est réduite sur un seul objet. Cette situation est de toute façon un peu idéaliste, car pour de nombreuses raisons, les réseaux de preuves sont souvent étendus avec une certaine forme d'équivalence.

2) AUCUNE ÉTAPE D'ÉLIMINATION DE COUPE COMMUTATIVE. L'élimination des coupures sur les réseaux de preuve prend une saveur bien différente de celle des calculs séquentiels car les étapes commutatives d'élimination des coupures disparaissent. La raison en est que dans les réseaux de preuves, les règles de déduction ne sont liées que par leur relation causale. Les cas commutatifs sont générés par le fait qu'une règle peut être masquée par une autre règle sans lien de cause à effet. Cela ne peut pas se produire dans les réseaux de preuves, où les règles sans lien de causalité sont éloignées. Comme la plupart des cas d'élimination de coupure sont commutatifs, on obtient une simplification frappante d'élimination de coupure. Cela a été particulièrement utile pour étudier les calculs lambda avec des substitutions explicites (car exponentielles = substitutions explicites). Encore une fois, cette situation est idéalisée car certaines présentations de réseaux de preuves nécessitent des étapes commutatives. cependant,

3) CRITÈRES D'EXACTITUDE. Les réseaux de preuves peuvent être définis par la traduction d'épreuves de calcul séquentielles, mais généralement un système de réseaux de preuves n'est accepté comme tel que s'il est fourni avec un critère d'exactitude, c'est-à-dire un ensemble de principes théoriques des graphes caractérisant l'ensemble des graphiques obtenus en preuve de calcul séquentiel. La raison pour laquelle un critère d'exactitude est requis est que le langage graphique libre généré par l'ensemble des constructeurs de réseaux de preuve (appelés liens) contient "trop ​​de graphiques", en ce sens que certains graphiques ne correspondent à aucune preuve. La pertinence de l'approche des critères de correction est généralement complètement incomprise. Il est important car il donne des définitions non inductives de ce qui est une preuve, offrant des perspectives étonnamment différentes sur la nature des déductions. Le fait que la caractérisation soit non inductive est généralement critiqué, alors que c'est exactement ce qui est intéressant. Bien sûr, il ne se prête pas facilement à la formalisation, mais, encore une fois, c'est sa force: les réseaux de preuves fournissent des informations qui ne sont pas disponibles à travers la perspective inductive habituelle sur les preuves et les termes. Un théorème fondamental pour les réseaux de preuves est le théorème de séquentialisation, qui dit que tout graphique satisfaisant au critère d'exactitude peut être décomposé par induction comme une preuve de calcul séquentielle (se traduisant par le graphique correct).

Permettez-moi de conclure qu'il n'est pas précis de dire que les réseaux de preuve sont une version classique et linéaire de la déduction naturelle. Le fait est qu'ils résolvent (ou tentent de résoudre) le problème de l'identité des preuves et que la déduction naturelle résout avec succès le même problème pour une logique intuitionniste minimale. Mais les réseaux de preuve peuvent également être réalisés pour les systèmes intuitionnistes et pour les systèmes non linéaires. En fait, ils fonctionnent mieux pour les systèmes intuitifs que pour les systèmes classiques.

Appelons une logique « symétrique » où ( « non A ») hypothèse signifie la même chose que la preuve et une preuve de la même signification que l'hypothèse d' . La logique classique et la logique linéaire sont symétriques en ce sens. La logique intuitionniste ne l'est pas.A - A $-A$$A$$-A$$A$

Girard a remarqué que la déduction naturelle est asymétrique exactement de cette façon. C'est pourquoi cela correspond à une logique intuitionniste. Les filets de preuve représentent une tentative de Girard d'inventer une forme symétrique de déduction naturelle.

La meilleure introduction à ces idées se trouve dans "Preuves et types" de Girard. Si vous travaillez à travers le système de déduction naturelle et de calcul séquentiel pour le fragmenter la logique intuitionniste, et lisez attentivement les sections 5.3 et 5.4 qui établissent un homomorphisme du calcul séquentiel à la déduction naturelle, vous obtenez une appréciation de ce qu'est la déduction naturelle. tout sur. L'annexe de Lafont introduit ensuite des réseaux de preuves dans le même esprit. Il est plus ou moins simple d'étendre l'homomorphisme des sections 5.3-4 à un entre le calcul séquentiel logique linéaire et les réseaux de preuve de logique linéaire (au moins pour le fragment multiplicatif).$\land\to$

Une chose qui est peut-être inutilement déroutante à propos du traitement de Girard est qu'il se passe de séquences à deux côtés et utilise des séquences à un côté dans l'intérêt de l'économie. Pour le calcul séquentiel, cela fonctionne plus ou moins bien. Mais, lorsque la même économie est appliquée à la déduction naturelle, les choses semblent étranges. Un filet de preuve est donc une «preuve de déduction naturelle» d'une disjonction de formules, sans aucune hypothèse . Une déduction de type est transformé en un eseau de type . Si cela vous embrouille, vous voudrez peut-être écrire pour vous-même un calcul séquentiel bilatéral et une forme d'hypothèse-conclusion de réseaux de preuve. Cela pourrait clarifier les choses.⊢ Γ ⊥ , $\Gamma \vdash A$$\vdash \Gamma^\perp, A$

Quelque chose que j'ai raté dans ma réponse originale: les réseaux de preuves sont un moyen d'écrire des preuves, et nous savons que les preuves sont des programmes. Ainsi, les réseaux de preuves sont également un moyen d'écrire des programmes.

La notation fonctionnelle traditionnelle pour l'écriture de programmes est asymétrique, tout comme la déduction naturelle. Ainsi, les réseaux de preuves indiquent une manière d'écrire des programmes sous une forme symétrique . C'est ainsi que les calculs de processus entrent en scène.

Une autre façon de représenter la symétrie est à travers la programmation logique, que j'ai explorée dans deux articles: Une fondation typée pour les programmes logiques directionnels et les aspects d'ordre supérieur de la programmation logique

Je me concentre sur la façon dont les réseaux de preuve sont liés au calcul séquentiel, laissant des choses plus dynamiques.

Réseaux de preuves résumés de calculs séquentiels abstraits: un réseau de preuves représente un ensemble de preuves de calculs séquentiels. Les réseaux de preuves oublient les différences sans importance entre les preuves de calcul séquentielles (comme quelle formule est décomposée en dessous de laquelle). Le théorème important ici est la "séquentialisation", qui convertit un réseau de preuves en une preuve de calcul séquentielle.

Cela concerne principalement la partie «comment ils se comportent sur le plan informatique» de votre question. Une façon de bien comprendre les réseaux de preuves du point de vue du calcul consiste à examiner des interprétations légèrement plus concrètes (par exemple, l'algèbre des processus).

Vous pourriez être intéressé par les éléments suivants:

• L'article d'Abramsky (la section CLL sur les expressions de preuve): Interprétations informatiques de la logique linéaire . Cet article présente également quelques résultats qui sont proches de ceux correspondants pour les réseaux de preuve, donc pourrait aider dans le deuxième aspect de votre question.

• L'article de Honda et Laurent qui montre comment un type spécifique de filets de preuve, appelés filets de preuve polarisés, correspond aux processus de Pi-calcul, et qui est mentionné ci-dessus par Martin Berger: Une correspondance exacte entre un pi-calcul typé et une preuve polarisée. filets

• (ici j'annonce sans vergogne mon propre travail) Le brouillon: Filets de preuve sous forme algébrique en cours

Il existe également des travaux sur les réseaux de preuve et le calcul lambda, qui donnent également des intuitions substantielles. Par exemple, le texte suivant de Delia Kesner et Stéphane Lengrand:

• Opérateurs de ressources pour λ-calcul

Vous pourriez également être intéressé par ce type de travail (très orienté vers les aspects théoriques) qui s'appuie sur des structures de preuve pour prouver en détail la propriété Strong Normalization de LL, par Michele Pagani et Lorenzo Tortora de Falco.

• Forte propriété de normalisation pour la logique linéaire du second ordre (cet article contient une belle carte des théorèmes importants).

En général, quels théorèmes faut-il étudier? Eh bien, je ne suis pas vraiment une autorité mais vous voudrez peut-être regarder la "séquentialisation" (concernant les réseaux de preuve et les preuves de séquence; voir le document TCS original sur LL), et la preuve de normalisation solide (plutôt impliquée, comme prévu, mais beaucoup importante Les théorèmes PN y sont liés [ou, utilisés pour le prouver]).

Si vous êtes familier avec la mise au point, vous pourriez également être intéressé par cet article d'Andreoli:

• Réseaux de focalisation et de preuve en logique linéaire et non commutative

J'espère que cela t'aides. Encore une fois, ces références sont vraiment non exhaustives.

le meilleur, Dimitris

Il y a eu récemment un travail intéressant pour resserrer la relation entre le filet de preuve et les calculs focalisés, en utilisant des variantes "multi-focalisées" où vous pouvez avoir plusieurs trous gauches simultanés, et en étudiant des preuves "focalisées au maximum". Si vous choisissez le bon calcul, les preuves à focalisation maximale peuvent correspondre à des réseaux de preuves MLL ou, dans la logique classique, à des preuves d'expansion ( The Isomorphism Between Expansion Proofs and Multi-Focused Sequent Proofs , Kaustuv Chaudhuri, Stefan Hetzl and Dale Miller, 2013)

Vous pouvez consulter mon article " Un aperçu des réseaux de preuve et des matrices pour les logiques sous-structurelles ".

Abstrait:

Cet article est une étude de deux types de schémas de preuve "compressés", la \ emph {méthode matricielle} et \ emph {réseaux de preuve}, appliqués à une variété de logiques s'étendant le long de la hiérarchie sous-structurelle du classique jusqu'au système Lambek non associatif. Un nouveau traitement des filets de preuve pour ces derniers est proposé. Les descriptions des réseaux de preuve et des matrices sont données dans une notation uniforme basée sur des séquences, de sorte que les propriétés des schémas pour les différentes logiques peuvent être facilement comparées.