On the confluence of lambda-calculus with conditional rewriting

Frédéric Blanqui 1 Claude Kirchner 2 Colin Riba 3, *
* Corresponding author
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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/inria-00509054
Contributor : Frédéric Blanqui <>
Submitted on : Tuesday, September 20, 2011 - 5:17:50 AM
Last modification on : Friday, April 12, 2019 - 10:18:09 AM
Long-term archiving on : Wednesday, December 21, 2011 - 2:20:06 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

430

Files downloads

250