Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

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' ↦ 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`.

Synopsis

- checkConfluenceOfRules :: ConfluenceCheck -> [RewriteRule] -> TCM ()
- checkConfluenceOfClauses :: ConfluenceCheck -> QName -> TCM ()
- sortRulesOfSymbol :: QName -> TCM ()

# Documentation

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

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

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 () Source #