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:
- *Different* rules
f ps' ↦ ...
whereps
andps'
can be unified. - Subpatterns
g qs
ofps
and rewrite rulesg qs' ↦ ...
whereqs
andqs'
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:
- 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)
andm + suc n = suc (m + n)
, then there should also be a rulesuc m + suc n = suc (suc (m + n))
. - Each rewrite rule should satisfy the *triangle property*: For
any rewrite rule
u ↦ w
and any single-step parallel unfoldingu => v
, we should have another single-step parallel unfoldingv => 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 #