Maintainer	Benedikt Schmidt <beschmi@gmail.com>
Safe Haskell	None

Term.Subsumption

Contents

Canonical representations for substitutions
for testing only

Description

Subsumption of terms and substitutions.

Synopsis

Documentation

compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering)Source

Compare terms t1 and t2 with respect to the subsumption order modulo AC.

eqTermSubs :: LNTerm -> LNTerm -> WithMaude Bool Source

Returns True if s1 and s2 are equal with respect to the subsumption order modulo AC.

factorSubstVia :: [LVar] -> LNSubst -> LNSubst -> WithMaude [LNSubst]Source

Canonical representations for substitutions

canonizeSubst :: LNSubstVFresh -> LNSubstVFresh Source

Returns a substitution that is equivalent modulo renaming to the given substitution.

for testing only

varOccurences :: HasFrees a => a -> [(LVar, Set Occurence)]Source

Returns the variables occuring in t together with the contexts they appear in. Note that certain contexts (and variables only occuring in such contexts) are ignored by this function. The function is used to guess renamings of variables, i.e., if t is a renaming of s, then variables that occur in equal contexts in t and s are probably renamings of each other.