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' ↦ v' where ps and ps' can be unified@.
2. Subpatterns g qs of ps and rewrite rules g qs' ↦ w where qs and qs' can be unified.

Each of these leads to a *critical pair* v₁ u -- 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.

Documentation

checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()

checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()

Check confluence of the given rewrite rules wrt all other rewrite rules (also amongst themselves).

Check confluence of the clauses of the given function wrt rewrite rules of the constructors they match against

sortRulesOfSymbol :: QName -> TCM ()