On the confluence of lambda-calculus with conditional rewriting

TL;DR

This paper explores the confluence properties of lambda-calculus combined with conditional rewriting, extending known results to algebraic rules and introducing new conditions for confluence beyond algebraic frameworks.

Contribution

It generalizes confluence results to algebraic conditional rewriting with and without eta-reduction, and introduces a new orthogonality-based approach for broader cases.

Findings

Confluence is maintained for algebraic conditional rules with weakly normalizing eta-reduction.

Modularity of confluence is limited outside algebraic conditions.

New confluence results are achieved using a restricted orthogonality concept.

Abstract

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.