Type systems and deduction in the rewriting calculus
Typage et déduction dans le calcul de réécriture
Résumé
The rewriting calculus is a lambda-calculus with pattern matching. This thesis is devoted to the study of type systems for this calculus, and to its applications to the domain of deduction.
We study two typing paradigms. The first one is inspired by the simply typed lambda-calculus, but it differs from it in the sense that a term may be well-typed without being terminating. Thus, we use it for representing programs and rewriting systems.
The second family of type systems we study is adapted from the Pure Type Systems. We show its strong normalization via a translation into a typed lambda-calculus.
Finally, we propose two ways of using the rewriting calculus in logic. In the first approach, we use the strongly normalizing systems to define proof terms for deduction modulo. In the second case, we define a generalization of natural deduction and we show that matching is useful in order to represent the rules of this deduction system.
We study two typing paradigms. The first one is inspired by the simply typed lambda-calculus, but it differs from it in the sense that a term may be well-typed without being terminating. Thus, we use it for representing programs and rewriting systems.
The second family of type systems we study is adapted from the Pure Type Systems. We show its strong normalization via a translation into a typed lambda-calculus.
Finally, we propose two ways of using the rewriting calculus in logic. In the first approach, we use the strongly normalizing systems to define proof terms for deduction modulo. In the second case, we define a generalization of natural deduction and we show that matching is useful in order to represent the rules of this deduction system.
Le calcul de réécriture est un lambda-calcul avec filtrage. Cette thèse est consacrée à l'étude de systèmes de types pour ce calcul et à son utilisation dans le domaine de la déduction.
Nous étudions deux paradigmes de typage. Le premier est inspiré du lambda-calcul simplement typé, mais un terme peut y être typé sans être terminant. Nous l'utilisons donc pour représenter des programmes et des systèmes de réécriture. La seconde famille de systèmes de types que nous étudions est adaptée des Pure Type Systems. Nous en démontrons la normalisation forte grâce à une traduction vers le lambda-calcul typé.
Enfin nous proposons deux approches pour l'utilisation du calcul de réécriture en logique. La première consiste à définir des termes de preuve pour la déduction modulo à l'aide des systèmes fortement normalisants. Dans la seconde, nous définissons une généralisation de la déduction naturelle et nous montrons que le filtrage est utile pour représenter les règles de ce système de déduction.
Nous étudions deux paradigmes de typage. Le premier est inspiré du lambda-calcul simplement typé, mais un terme peut y être typé sans être terminant. Nous l'utilisons donc pour représenter des programmes et des systèmes de réécriture. La seconde famille de systèmes de types que nous étudions est adaptée des Pure Type Systems. Nous en démontrons la normalisation forte grâce à une traduction vers le lambda-calcul typé.
Enfin nous proposons deux approches pour l'utilisation du calcul de réécriture en logique. La première consiste à définir des termes de preuve pour la déduction modulo à l'aide des systèmes fortement normalisants. Dans la seconde, nous définissons une généralisation de la déduction naturelle et nous montrons que le filtrage est utile pour représenter les règles de ce système de déduction.
Fichier principal
tel-000105461.pdf (1.48 Mo)
Télécharger le fichier
tel-00010546.pdf (470.53 Ko)
Télécharger le fichier
Format : Autre