tamarin-prover-term-0.4.1.0: Term manipulation library for the tamarin prover.

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellSafe-Infered

Term.Narrowing.Variants.Check

Description

Completeness and minimality checking for the variants of a term.

Synopsis

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.