Dynamique des preuves (et des programmes)

Sur l’écran de droite, une preuve formalisée en calcul des séquents (à gauche) et sa forme normale (à droite). Le passage de la première à la seconde est un processus dynamique, appelé élimination des coupures, qui correspond à l’exécution d’un programme informatique. Au-dessous, sont représentées leurs interprétations en géométrie de l’interaction, un modèle mathématique des preuves qui oublie certaines informations (comme les noms des formules) mais représente correctement la dynamique de l’élimination des coupures et donc de l’exécution des programmes. Une propriété importante de ce processus dynamique est l’adjonction, qui est reliée à la propriété de Church-Rosser, énonçant que le résultat de l’évaluation d'un programme prenant deux arguments ne dépend pas de l’ordre dans lequel ceux-ci sont utilisés. Sur l’écran de gauche, est illustré le fait que la représentation de l’exécution des programmes par l’opération consistant à construire l’ensemble des chemins maximaux simples (ne passant qu’une seule fois par chaque sommet), ne satisfait pas cette propriété. Le graphe de gauche représente un programme (en rouge) auquel sont appliqués deux arguments (en vert et en bleu) ; le graphe de droite représente l’état intermédiaire où le programme a utilisé son argument vert. Il est possible de vérifier que le cycle visible sur le graphe de droite est simple, mais le cycle correspondant dans le graphe illustré à gauche n’est pas simple. Cette non-préservation de la simplicité montre que cette construction ne représente pas adéquatement l’exécution des programmes.