Definitions by rewriting in the lambda-calculus : confluence, reducibility and typing

Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage

Colin Riba (1)

1 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

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

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

Mots clés: Lambda-calculus; Saturated sets; Biorthogonality; Reducibility candidates; Rewriting; Conditional rewriting; Typing; Union types; Strong normalization

Mots clés: Lambda-calcul; Réécriture; Réécriture conditionnelle; Confluence; Typage; Types union; Normalisation forte; Candidats de réductibilité; Ensembles saturés; Biorthogonalité; Logique combinatoire

Domaines: Autre [cs.OH]; Autre

Colin Riba. Définitions par réécriture dans le lambda-calcul : confluence, réductibilité et typage. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2007. Français. ⟨NNT : 2007INPL102N⟩. ⟨tel-01752911⟩