Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage / Colin Riba ; sous la direction de Claude Kirchner et de Frédéric Blanqui

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Logique combinatoire

Lambda-calcul

Classification Dewey : 004

Classification Dewey : 620

Kirchner, Claude (1951-....) (Directeur de thèse / thesis advisor)

Blanqui, Frédéric (19..-....) (Directeur de thèse / thesis advisor)

Institut national polytechnique de Lorraine (1969-2012) (Organisme de soutenance / degree-grantor)

École doctorale IAEM Lorraine - Informatique, Automatique, Électronique - Électrotechnique, Mathématiques de Lorraine (Ecole doctorale associée à la thèse / doctoral school)

Relation : Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage / Colin Riba ; sous la direction de Claude Kirchner et de Frédéric Blanqui / Vandoeuvre-lès-Nancy : Institut National Polytechnique de Lorraine , 2007

Résumé / Abstract : Cette thèse concerne la combinaison du lambda-calcul et de la réécriture, dont nous étudions principalement deux propriétés : la confluence et la normalisation forte. Nous commençons par étudier sous quelles conditions la combinaison d'une relation de réécriture conditionnelle confluente au lambda-calcul donne une relation de réécriture confluente. Ensuite nous nous intéressons aux preuves de normalisation forte de lambda-calculs typés utilisant la technique de réductibilité. Notre contribution la plus importante est une comparaison de diverses variantes de cette technique, utilisant comme outil de comparaison la manière dont ces variantes s'étendent à la réécriture et dont elles prennent en compte les types unions et les types existentiels implicites. Enfin, nous présentons un critère, basé sur un système de types contraints, pour la normalisation forte de la réécriture conditionnelle combinée au lambda-calcul. Notre approche étend des critères de terminaison existants qui utilisent des annotations de taille. C'est à notre connaissance le premier critère de terminaison pour la réécriture conditionnelle avec membres droits d'ordre supérieur qui prenne en compte, dans l'argument de terminaison, de l'information issue de la satisfaction des conditions des règles de réécriture

Résumé / Abstract : This thesis is about the combination of lambda-calculus with rewriting. We mainly study two properties: confluence and strong normalization. We begin by studying under which conditions the combination of a confluent conditional rewrite relation to the lambda-calculus leads to a confluent relation. Next, we study strong normalization proofs of typed lambda-calculi that use the reducibility technique. Our main contribution is a comparison of variants of this technique, with respect to how they extend to rewriting and how they handle union and implicit existential types. Finally, we present a termination criterion for the combination of conditional rewriting and lambda-calculus based on a constrained type system. Our approach, which extends known criteria that use sized types, is to our knowledge the first termination criterion for conditional rewriting with higher-order right-hand sides that takes into account in the termination argument some information generated by the satisfaction of the conditions of the rewrite rules