On the confluence of lambda-calculus with conditional rewriting

Frédéric Blanqui 1 Claude Kirchner 1 Colin Riba 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The confluence of untyped lambda-calculus with unconditional rewriting has already been studied in various directions. In this paper, we investigate the confluence of lambda-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Muller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing beta-reduction to weakly normalizing beta-reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using an extended notion of orthogonality that takes advantage of the conditional part of rewrite rules.
Type de document :
Communication dans un congrès
Foundations of Software Science and Computation Structures, Mar 2006, Vienne, Austria. 3921 (3921), 2006, Lecture Notes in Computer Science. 〈10.1007/11690634_26〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00000729
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 11 septembre 2006 - 15:14:01
Dernière modification le : jeudi 8 février 2018 - 11:32:01
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:13:31

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui, Claude Kirchner, Colin Riba. On the confluence of lambda-calculus with conditional rewriting. Foundations of Software Science and Computation Structures, Mar 2006, Vienne, Austria. 3921 (3921), 2006, Lecture Notes in Computer Science. 〈10.1007/11690634_26〉. 〈inria-00000729v2〉

Partager

Métriques

Consultations de la notice

226

Téléchargements de fichiers

84