Propriétés de normalisation de calculs logiques symétriques
Institution:
ChambéryDisciplines:
Directors:
Abstract EN:
This thesis examines, from proof theoretical point of view, some of the calculi which can be related to classical logic by the Curry-Howard isomorphism. First of all, we study the simply typed λμ-calculus defined by Parigot. Parigot proved that the λμ-calculus is strongly normalizing. David and Nour showed that the strong normalization is preserved for the λμμ'-calculus also. This is no more true if we add the ρ-rule to the λμμ'-calculus. However, the weak normalization still holds. We prove that the untyped μμ'ρ calculus as well as the typed λμμ'ρ-calculus are weakly normalizing. Next, a bound for the lengths of the reduction sequences in the simply typed λμρθ-calculus is established, extending a result of Xi stated for the simply typed λ-calculus. Then we give an arithmetical proof for the strong normalization of the simply typed symmetric λ-calculus defined by Berardi and Barbanera. Finally, we define a translation between the simply typed symmetric λ-calculus and an extension of the λμ*-calculus of Curien and Herbelin in such a way that the strong normalization of one of the calculi implies that of the other one.
Abstract FR:
Dans cette thèse quelques-uns des calculs ont été étudiés qui peuvent être mis en rapport avec la logique classique à l'aide de l'isomorphisme de Curry-Howard. On étudie tout d'abord le λμ-calcul simplement typé de Parigot. Parigot a prouvé que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte du λμμ'-calcul. Cependant, si l'on ajoute au λμμ'-calcul la règle ρ de simplification, la normalisation forte est perdue. On montre que le μμ'ρ-calcul non-typé est faiblement normalisable et que le λμμ'ρ-calcul typé est aussi faiblement normalisable. On établit ensuite une borne de la longueur des séquences de réductions en λμρθ-calcul simplement typé. Ce résultat est une extension de celui de Xi pour le λ-calcul simplement typé. Dans le chapitre suivant on présente une preuve arithmétique de la normalisation forte du λ-calcul symétrique de Berardi et Barbanera. Enfin, on établit des traductions entre le λ-calcul symétrique de Berardi et Barbanera et le λμ*-calcul, qui est le calcul de Curien et Herbelin étendu avec une négation, de telle manière que la normalisation forte d'un de ces calculs implique celle de l'autre.