Logics and term rewriting
Logiques et réécriture
Résumé
Not available
La première partie de notre thèse est dédiée à l'étude de l'élimination de coupures dans le calcul de séquents classique en s'appuyant sur le théorème de Gentzen (1934). Ce dernier stipule que toute preuve en calcul de séquents classique peut être transformée en une preuve normale ne faisant pas intervenir la règle de coupure. Gentzen a démontré ce résultat en décrivant une procédure de normalisation. Mais sa démonstration ainsi que celles de Tait et de Girard prouvent la terminaison de cette procédure seulement pour une stratégie particulière. La question que nous nous sommes posée est : comment montrer que la procédure d'élimination de coupures termine quelque soit la stratégie employée (une forme forte du théorème de Gentzen) ? L’approche que nous avons alors adoptée consiste à utiliser des techniques standards de réécriture. Plus précisément, nous représentons les preuves par des termes puis nous construisons un système de réécriture réalisant l'élimination de coupures. La définition de ces règles de réécriture fait abstraction de toute stratégie. La preuve de terminaison du système de réécriture construit établit alors une forme forte d'élimination de coupures pour le calcul de séquents considéré. Cette nouvelle approche produit une démonstration générique. En effet nous avons appliqué avec succès cette méthode aux calculs de séquents classique (LK), intuitionniste (LJ1) et linéaires (MALL1 et CLL). En plus de la palette de techniques de preuve de terminaison purement syntaxiques, nous avons employé des méthodes sémantiques pour la preuve de terminaison de la procédure d'élimination de coupures dans le cas des calculs MALL1 et CLL. L’avantage de cette seconde méthode est l'extraction aisée de bornes sur la longueur des séquences de réécriture. En fin de cette thèse, nous nous sommes intéressés aux travaux récents de de Groote et Kfoury & Wells qui s'apparentent à notre travail. En effet ils utilisent des méthodes à caractère syntaxique pour établir la forte normalisation de divers lambda-calculs typés. En combinant un cas particulier de la preuve de de Groote et une version modifiée de la preuve de Kfoury et Wells, nous obtenons une preuve alternative de la forte normalisation du lambda-calcul simplement typé. Cette dernière syntaxique et plus constructive utilise en partie des techniques relevant de la théorie de la réécriture.