On the confluence of lambda-calculus with conditional rewriting

Frédéric Blanqui 1 Claude Kirchner 2 Colin Riba 3, *
* Auteur correspondant
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : The confluence of untyped λ-calculus with unconditional rewriting is now well un- derstood. In this paper, we investigate the confluence of λ-calculus with conditional rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether β-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty's result is improved from the assumption of strongly normalizing β-reduction to weakly normalizing β-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 a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2010, 411 (37), pp.3301-3327. 〈http://dx.doi.org/10.1016/j.tcs.2009.07.058〉. 〈10.1016/j.tcs.2009.07.058〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00509054
Contributeur : Frédéric Blanqui <>
Soumis le : mardi 20 septembre 2011 - 05:17:50
Dernière modification le : vendredi 20 avril 2018 - 15:44:24
Document(s) archivé(s) le : mercredi 21 décembre 2011 - 02:20:06

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Frédéric Blanqui, Claude Kirchner, Colin Riba. On the confluence of lambda-calculus with conditional rewriting. Theoretical Computer Science, Elsevier, 2010, 411 (37), pp.3301-3327. 〈http://dx.doi.org/10.1016/j.tcs.2009.07.058〉. 〈10.1016/j.tcs.2009.07.058〉. 〈inria-00509054〉

Partager

Métriques

Consultations de la notice

365

Téléchargements de fichiers

155