Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
Completeness and minimality checking for the variants of a term.
- checkComplete :: LNTerm -> [LNSubstVFresh] -> WithMaude Bool
- checkMinimal :: LNTerm -> [LNSubstVFresh] -> WithMaude Bool
- variantsFrom :: LNTerm -> LNSubstVFresh -> WithMaude [LNSubstVFresh]
- isNormalInstance :: LNTerm -> LNSubst -> LNSubst -> WithMaude Bool
- leqSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh -> WithMaude Bool
Documentation
checkComplete :: LNTerm -> [LNSubstVFresh] -> WithMaude BoolSource
checkComplete t substs
checks if substs
is a complete set of variants
for t
and returns Just (subst1,subst2)
if there is a narrowing step
from subst1
that yields a new variant subst2
.
checkMinimal :: LNTerm -> [LNSubstVFresh] -> WithMaude BoolSource
checkMinimal t substs
checks if substs
is a minimal set of variants
for t
and returns False
if there are subst1 /= subst2 in substs with
subst1 <=_Var_t subst2.
variantsFrom :: LNTerm -> LNSubstVFresh -> WithMaude [LNSubstVFresh]Source
variantsFrom rules t subst
returns all the one-step variants of
norm (t subst)
for the given set of rules
.
isNormalInstance :: LNTerm -> LNSubst -> LNSubst -> WithMaude BoolSource
isNormalInstance t s s'
returns True
if s'(norm(s(t)))
is in normal
form.
leqSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh -> WithMaude BoolSource
leqSubstVariant t s1 s2
compares two substitutions using the variant order
with respect to t
and returns True
if s1
is less or equal than s2
and False
otherwise. Use the more expensive compareSubstVariant
which uses two AC matchings instead of one if you also want to distinguish
Nothing
, Just EQ
, and Just GT
.
s1 is smaller or equal to s2 wrt. to the variant order (less general) iff there is an s1' such that s1 = s2' . s2 restricted to vars(t) and s2'(norm(s2(t))) is in normal form, or equivalently norm(s1(t)) =AC= s2'(norm(s2(1))). This means s1 is redundant since it is just an AC instance of s2 that does not require additional normalization steps.