Talk:Proof-nets

Maybe we should try and start again our discussion concerning proof nets, their definition(s), and their graphical representations on this wiki. First, I leave some open questions:

• Is there anything new concerning this matter ?
• Can we agree on some common ground to start these pages ?
• Why not start from scratch and see what breaks ?

In order to fix ideas, I recall the main points of our email discussions of October 2009. --Lionel Vaux 13:45, 17 January 2011 (UTC)

Discussion des 11-12 oct. 2009

Message initial d'Olivier

Bonjour a tous,

Il est grand temps de commencer a se pencher sur la question des reseaux de preuve dans llwiki.

Je vous rappelle quelques elements que je suggerais dans mon precedent mail sur la question :

De maniere a pouvoir commencer a parler de reseaux de preuve dans le wiki, il semble necessaire de:

• Faire un choix de definition formelle principale qui sera utilisee dans les differentes pages parlant de reseaux (il faut donc qu'elle s'adapte facilement aux differentes extensions que l'on voudra traiter). Des definitions alternatives pourront etre decrites dans la page des reseaux (ou des pages specifiques) mais pas utilisees en dehors.
• Definir une syntaxe pour saisir les reseaux (au moins pour les plus simples, ou en fournissant la possibilite de donner des indications de placements de noeuds, ...).
• Choisir comment dessiner les reseaux a partir de la syntaxe de saisie et les integrer dans les pages du wiki.

Je vous propose dans un premier temps de faire une collecte de suggestions :

• votre (vos) choix de definition formelle de reseaux (juste une esquisse des elements clefs)
• la syntaxe dont vous reveriez pour ecrire vos reseaux
• votre moteur favori pour dessiner/afficher des reseaux
• des exemples significatifs de reseaux de maniere a faire un peu de benchmark entre les differentes propositions des 3 points precedents

J'attends vos propositions, Olivier.

Définition formelle des réseaux

Contribution de Laurent

Réseaux de preuve = réseau d'interaction (plus boîtes), c'est à dire un ensemble de ports, un ensemble de tuples de ports (les cellules) et un ensemble de couples de ports (les fils) et tout le tintouin qui va avec.

Question d'Olivier: comment est-ce qu'on traite les axiomes et coupures ? comme des fils ou comme des cellules bi-ports ?

Réponse de Laurent: Je proteste: ces questions ne sont pas bateau. En toute rigueur si on veut coller à la définition originale de Girard (et accessoirement pour d'autres raisons intéressantes comme par exemple définir simplement la eta-expansion, garder la possibilité de définir la réduction non-ax) il faut des cellules bi-ports ce qui oblige à lever la restriction "un unique port ppal" des réseaux d'interaction (les restrictions sont faites pour être levées s'pas?). Après on peut ajouter qu'il est souvent commode - par exemple pour définir les réseaux diff ou les zones de broadcast - de virer les cellules ax et cut.

Remarque de Lorenzo: Tout à fait d'accord avec la remarque de Laurent (Regnier :-), autrement c'est tautologique).

Question d'Olivier: comment definit-on les boites ? comme des sous-reseaux ou comme des cellules (multi-ports ?) auquelles sont recursivement associes des reseaux ?

Réponse de Laurent: Des cellules auxquelles sont récursivement associés des réseaux.

Remarque de Lorenzo: Là aussi, je suis d'accord. Il m'est arrivé cependant de faire subir des opérations chirurgicales délicates aux réseaux (notamment en étudiant l'injectivité), et je pense que ce serait utile d'avoir une définition permettant facilement de décrire l'effacement du pourtour des boites. L'option préconisée par Laurent me parait compatible avec cette nécessité (quitte à rajouter une cellule porte auxiliaire de boite $?P$).

Contribution de Marc

Bon il faut se demander ce que l'on a envie de faire avec des réseaux. Voila ce que j'imagine. On veut :

• (a) pouvoir décrire facilement des traductions dans les réseaux
• (b) pouvoir écrire naturellement des réseaux
• (c) avoir une définition de la réduction autrement qu'avec les mains
• (d) avoir un partage entre les réseaux de preuve et les réseaux d'interaction
• (e) pouvoir ajouter des boites (promotion et additives)
• (f) pouvoir ajouter des sommes
• (g) avoir une notion de chemins et de réduction de chemins pour pouvoir embrayer sur la gdi à la D-R

J'annonce la couleur tout de suite, il n'existe pas, à mon avis, une solution parfaite pour tout cela. Dans ma thèse j'ai une définition qui nous permet de faire bien c-d-g, a peu près a-e-f, mais qui n'est pas vraiment une représentation très naturelle (enfin c'est celle que propose Laurent à peu de différences près). Pour résumer j'ai une définition des réseaux qui permet de définir la réduction par clôture au contexte.

Contribution de Michele

Moi j'hesite entre trois differentes definitions des reseaux, chaque definition ayant des pour et contre. Je note ici un'esquisse des mes choix, avec les + et les -...

(ne me pas grondez trop durament pour mon fraicais et mes impardonnables omissions: ils sont des notes, ecrites rapidement ;-)).

(j'omets des variants plus specifiques comme "reseaux = forets des formules + axiom linking"...).

Syntaxe JY

JY=Jean-Yves Girard.

un reseau est un hypergraphe etiquete, les noeds etant les (occurrences des) formules, et les hyperaretes etant les regles deductives (axiomes et coupures y compris).

• + definition formelle simple
• + elegant traitement de fussionement des formules pour composer les modules (voir minus de syntax Y);
• - distinction entre conclusion et hypothese, donc distinction entre reseau et module: regles de reduction doivent etre definies sur les modules (redexes et contracta sont modules). En plus, immaginez quelle "joie" est introduire les sommes formelles de modules, pour parler de sliced proof nets, ou des reseaux differentiels;
• - l'elimination des coupures sur les structures de preuve (il faut permettre la reduction aussi en presence des erreurs, bien sur!) crée des circles vicieux (e.g. une contraction ayant une parmi ses premisses comme conclusion): laid à les dessiner;
• - la presence des axioms est legerement antypatique pour etudier la correspondence lambda-calcul/réseaux, et tout à fait antypatique pour parler des reseaux differentiels (reduction contraction/cocontraction introduise des axioms).

Syntaxe L

L=Laurent regnier (PhD Thesis), comme olivier Laurent (PhD Thesis) et beaucoup d'autres autors, comme Lorenzo tortora de falco et la plus parts des papiers sur les logiques Legeres.

un reseau est un graphe etiquete, les regles sont les noeds et les aretes les (occurrences des) formules

• + pedagogiquement superefficace: les graphes sont beaucoup plus intuitives des hypergraphes; aussi formellement la syntax L peut etre definie sans trop "baroquisme";
• + les circles vicieux (e.g. une contraction ayant une premisse comme sa conclusion) peuvent etre facilement dessines; en general les dessins resultent jolis
• + comme dans JY, elegant fussionement des aretes pour composer les modules (cela depend du fait que on a les axiomes explicits);
• - memes problemes de la syntaxe JY: distinction conclusion/hypothese, reseau/module, presence axiomes antypatique pour reseaux differentiels.

Syntaxe Y

Y=Yves Lafont, base de depart des reseaux differentiels.

un reseau est un graphe et un hypergraphe, le graphe donnant les wires (i.e. les occurences des formules (modulo dualite) et regles identite (axioms et coupure)) et l'hypergraphe donnant les cellules (i.e. les regles logiques et structurelles).

• + distinction entre conclusion et hypothese d'un module devient une difference d'orientation des wires, quelle elegance! On depasse la distinction entre reseau et module;
• + mis en evidence des coupures commutatives, comme la coupure qui depasse le paradigme des réseaux *d'interactions* (commutative = coupure ayant une porte active qui n'est pas principal, i.e. porte auxiliare boite)
• +/- superjolie dessins, au niveau graphique la syntaxe Y est sans doute la meilleur mais au niveau de definition formelle elle est lourde (deux structure graphique, wires et cells...)
• - laborieuse definition de fussionement des conclusions entre reseaux (voir theses de Damiano et Lionel ("alpha"-reecriture que fonde step by step les wires a fusionner), sinon voir solution Marc (reseaux = permutations, mais puis il faut bien definire les cellules "commutatives", comme la contraction...))

Les trois groupes peuvent avoir differentes "declinations", selon la maniere d'approcher à des problemes classiques des réseaux, par exemples:

• boites (exponentielles, additives...): sont des regles sequentielles (i.e. in JY (resp. L et Y) des hyperarretes (resp. des noeds, cellules) etiquettes par des reseaux), ou des "zones" qui delimites des sousgraphes? (moi je suis pour la solution des boites comme regles sequentielles, beaucoup plus elegante au niveau formel)
• definition des reductions canoniques (associativite des contractions, neutralite affaiblissement, commutations de la contraction avec la porte auxiliaire) ou utilisation de rapresentantes canoniques?
• definition des additives (& et \top) par boites, tranches, poids etc; definition du second ordre par boites ou subtiles conditions d'avoir variables lies distincte deux à deux; etc.

Syntaxe pour écrire vos reseaux

Laurent

Le calcul des séquents.

Question d'Olivier: c'est une base solide ! un petit defaut est, pour des reseaux un peu gros : est-ce que l'information induite pour le placement des noeuds est suffisante ou faut-il un moyen de rajouter une telle information ?

Marc

Je propose deux syntaxes : une syntaxe permettant par exemple d'écrire un lambda-terme et que le réseau se fasse tout seul, et une syntaxe explicite pour écrire des réseaux, cette-dernière devrait être assez proche de la syntaxe d'Yves pour les réseaux d'interaction. L'idéal serait d'avoir une syntaxe hybride permettant de manipuler des traductions comme des sortes de boites.

Michele

calcul de sequent, avec tensor/coupure unaire si je veux ecrire des reseaux pas corrects

Moteur pour dessiner/afficher des réseaux

Marc

J'ai un moteur basé sur ma proposition précédente. Pour le moment j'ai du code caml pour écrire et réduire des réseaux d'interaction (avec somme) et du code pour faire du placement automatique. Le tout affichant une interface pour modifier le dessin. Pour pouvoir l'intégrer au wiki il faudrait rajouter une interface oueb, et c'est là le problème. Vincent Balat a un truc permettant de faire exécuter du caml sur un navigateur par un interprète bytecode en javascript, ca devrait suffir à nos besoins, mais je ne sais pas si on peut l'avoir indépendemment de Ocsigen. En tout cas, pour continuer ce programme j'ai un problème de temps, donc pour le rendre productif il faudrait que j'ai de l'aide.

Michele

quand je suis tout seul: xfig (pas superjolie mais efficace, avec "combined Latex/Pdf"); quand j'ai l'assistence de Paolo j'utilise son package basé sur tikz... les dessins sont magnifiques, mais je trouve la syntaxe encor trop difficile pour moi quand je dois dessiner des reseaux avec boites, sommes formelles et quelques cycles...

Exemples significatifs de réseaux

Laurent

Le contre-exemple de David à l'injectivité de la sémantique en lambda-mu-calcul.

Marc

Je propose les zones de communication, parce que c'est l'exemple typique de réseau n'ayant pas d'orientation verticale naturelle.

Michele

• reseaux et semantique: controexemple injectivité dans Coh qui vient de David-Py (l'originale de David-Py est separé dans Coh); controexemple injectivité Coh sans boite (Lorenzo docet); controexemple injectivité de Rel (:o, non, je rigole, je ne l'ai pas...)
• reseaux et elimination de coupures: controexemple confluence et/ou normalisation en presence de cycle switching ou des types pures; contrexemple à confluence de DiLL sans associativité de (co)contraction.

Complément de Michele sur ce qu'on voudrait pouvoir traiter

Il peut etre utile pour bien choisir une syntaxe et un langage pour ecrire les reseaux avoir en tete les sujets qu'on veut traiter. Ici une petite liste de sujets que je trouve tres amusants (il est vraiment une esquisse, pour commencer la discussion):

• reseaux et sequentialization (critere de correction):
  • dans MLL (critere voyage, switching acyclicité et connexion, contractions (linearité du critere), autres?); problemes des unites (solutions ?, reseaux MLL et categories *-autonome);
  • dans MELL: extension facile avec mix (probleme affaiblissement analogue problemes des unites); extension au "lambdaMELL" (fragment minimale de MELL);
  • dans MALL..........................................
  • criteres polarises (LLpol et LLP);
  • dans LL2
• lambda calcul:
  • resultats de bisimulation
  • reseaux et lambda calcul avec substitutions explicites
  • reseaux polarise et calculs avec stream (lambdamu, lambdac, etc)
• elimination des coupures:
  • normalisation (avec correction + types), developments finis (reduction exponentielle termine), interaction et correction (Th de Bechet)
  • confluence (avec correction et tranches additives); perpetualité;
  • classes de complexité borné (proprietes structurelles des reseaux qui caracterisent des classes de complexité)
• semantique:
  • webbed semantics: experiments, injectivité, correction semantique et logique (problemes dans MELL, dans MALL)
  • game semantics et GoI
• reseaux differentiels (DiLL):
  • traduction de LL dans DiLL
  • calcul avec ressources (et differentiel) dans DiLL
  • pi-calcul dans DiLL
  • proprietes d'elimination des coupures dans DiLL (confluence, normalization, developements finis, standardisation, perpetualité)