Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|

Safe Haskell | Safe-Infered |

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.