inria-00509054, version 1
On the confluence of lambda-calculus with conditional rewriting
Frédéric Blanqui
a, 1Claude Kirchner
a, 2Colin Riba
b, 3
Theoretical Computer Science 411, 37 (2010) 3301-3327
Résumé : 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.
- a – INRIA
- b – ENS Lyon
- 1 : FORMES (LIAMA)
- INRIA – Tsinghua University / Beijing – LIAMA
- 2 : INRIA Bordeaux - Sud-Ouest (INRIA Bordeaux - Sud-Ouest)
- INRIA
- 3 : Laboratoire de l'Informatique du Parallélisme (LIP)
- Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
- Domaine : Informatique/Logique en informatique
- Mots-clés : lambda-calculus – higher-order rewriting – conditional rewriting – confluence
- inria-00509054, version 1
- http://hal.inria.fr/inria-00509054
- oai:hal.inria.fr:inria-00509054
- Contributeur : Frédéric Blanqui
- Soumis le : Mardi 20 Septembre 2011, 05:17:50
- Dernière modification le : Mardi 20 Septembre 2011, 18:56:57






Documents associés

Exporter