On the confluence of lambda-calculus with conditional rewriting

TL;DR

This paper investigates the confluence properties of lambda-calculus combined with conditional rewriting, extending previous results to algebraic rules and exploring new orthogonality-based approaches.

Contribution

It provides new confluence results for lambda-calculus with conditional rewriting, including cases with algebraic rules and extended orthogonality, improving upon prior work.

Findings

Confluence results for algebraic conditional rules with and without beta-reduction.

Examples showing modularity challenges outside the studied conditions.

New orthogonality-based confluence results beyond algebraic frameworks.

Abstract

The confluence of untyped lambda-calculus with unconditional rewriting has already been studied in various directions. 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 Muller 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 an extended notion of orthogonality that takes advantage of the conditional part of rewrite rules.