Agda
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rewriting.Confluence

Description

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.
Synopsis

Documentation

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

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

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

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