Computer Science – Logic in Computer Science
Scientific paper
2011-09-20
Theoretical Computer Science 411, 37 (2010) 3301-3327
Computer Science
Logic in Computer Science
Scientific paper
10.1016/j.tcs.2009.07.058
The confluence of untyped \lambda-calculus with unconditional rewriting is now well un- derstood. 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 M\"uller 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 a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.
Blanqui Frédéric
Kirchner Claude
Riba Colin
No associations
LandOfFree
On the confluence of lambda-calculus with conditional rewriting does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On the confluence of lambda-calculus with conditional rewriting, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the confluence of lambda-calculus with conditional rewriting will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-147705