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

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

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

# 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

sortRulesOfSymbol :: QName -> TCM () Source #