Un cadre sémantique qui interprète la réduction de preuves (élimination des coupures) comme un flux dynamique ou une interaction d'information, souvent modélisé par des opérateurs, des traces ou des machines à jetons suivant le déplacement d'information dans un réseau de preuve.

Principe

Remplacer la réduction syntaxique statique par un processus dynamique sémantique où des chemins d'interaction, la composition d'opérateurs ou le mouvement de jetons codent le comportement computationnel des preuves et mettent en lumière des invariants préservés par l'élimination des coupures.

Démonstration

Dans les preuves de logique linéaire, représenter les coupures comme des connexions dans un proof net et modéliser l'élimination des coupures par des jetons parcourant le réseau ou en composant des opérateurs linéaires dont la trace enregistre le flux d'information, caractérisant ainsi la normalisation comme une dynamique de type matrice.

Mauvaise application

Employer un modèle d'interaction qui ignore des contraintes structurelles (par exemple ne pas tenir compte de la sensibilité aux ressources en logique linéaire) peut produire des modèles qui ne reflètent pas la normalisation proof-théorique et fournissent des invariants trompeurs.

Conséquence

Va au-delà des identités syntaxiques statiques pour fournir des comptes rendus opérationnels de la normalisation, produit de nouveaux invariants (formules d'exécution, traces), relie à la théorie des opérateurs et aux modèles machines, et suggère des implémentations sémantiques de la computation extraites des preuves.

Inversion

L'inverse est de voir l'élimination des coupures purement comme des règles locales de réécriture syntaxique sans insister sur le flux dynamique global ; une telle vue manque d'invariants globaux et de connexions à la sémantique par opérateurs.

Limite

S'applique de préférence aux systèmes dotés de représentations en circuits ou réseaux de preuves (proof nets, graphes d'interaction) et où la dynamique peut recevoir une sémantique par opérateurs ou jetons ; moins directement applicable aux systèmes dépourvus d'une représentation compositionnelle adaptée.

Tension sémantique

Une tension existe entre les présentations algébriques/par opérateurs qui mettent l'accent sur les propriétés spectrales ou de trace et les présentations combinatoires/à jetons qui insistent sur le mouvement pas à pas ; les deux capturent l'interaction mais soulignent des invariants différents.

Synthèse

La Géométrie de l'Interaction reconsidère l'élimination des coupures comme un flux d'information : les preuves deviennent des réseaux traversés par des jetons ou des opérateurs, produisant une sémantique opérationnelle qui dévoile des invariants dynamiques et unifie la réduction syntaxique avec le comportement en théorie des opérateurs.