Agda.TypeChecking.Rewriting.Confluence

Checking local or global confluence of rewrite rules.

For checking LOCAL CONFLUENCE of a given rewrite rule f ps ↦ v, we construct critical pairs involving this as the main rule by searching for:

1. *Different* rules f ps' ↦ ... where ps and ps' can be unified.

2. Subpatterns g qs of ps and rewrite rules g qs' ↦ ... where qs and qs' can be unified.

Each of these leads to a *critical pair* v₁ f us -- v₂, which should satisfy v₁ = v₂.

For checking GLOBAL CONFLUENCE, we check the following two properties:

1. For any two left-hand sides of the rewrite rules that overlap (either at the root position or at a subterm), the most general unifier of the two left-hand sides is again a left-hand side of a rewrite rule. For example, if there are two rules suc m + n = suc (m + n) and m + suc n = suc (m + n), then there should also be a rule suc m + suc n = suc (suc (m + n)).

2. Each rewrite rule should satisfy the *triangle property*: For any rewrite rule u ↦ w and any single-step parallel unfolding u => v, we should have another single-step parallel unfolding v => w.