Retour à la page du séminaire

7/05/99: Patrick Baillot Longley (Marseille)
Complexité élémentaire et géométrie de l'interaction (travail en collaboration avec Marco Pedicini)

résumé

Résumé : Les modèles de géométrie de l'interaction sont des modèles des preuves où la procédure d'élimination des coupures est interprétée explicitement par une opération traduisant un échange d'information (Exécution). Nous nous intéressons à l'interprétation de la Logique Linéaire Elémentaire (ELL), un système où le nombre détapes de la normalisation est majorée par une fonction élémentaire de la taille de la preuve. Nous décrivons un modèle de géométrie de l'interaction offrant la même borne de complexité sur le calcul : l'exécution termine en un temps élémentaire en la taille de l'entrée. Ce modèle est donné par une algèbre de clauses muni de la loi de résolution : les preuves sont interprétées par des combinaisons de clauses et l'exécution est définie au moyen de la résolution.