This library provides predicates for unification.
In FASILL the concepts of unifier and most general unifier (mgu) are extended to cope with similarities. Let be a similarity relation, be a cut value and and be two expressions. The substitution is a weak unifier of level for and with respect to if its unification degree . Note that our algorithm uses a different notion of unification state, where an extra component accumulates an approximation degree. The unification of the expressions and is obtained by a state transformation sequence starting from an initial state , where is the identity substitution and is the supremum of the lattice . The thresholded similarity-based unification relation, "", is defined as the smallest relation derived by the following set of transition rules (where denotes the set of variables of a given term ):
In addition to a different notion of unification state, which uses an extra component to accumulate the approximation degree obtained so far, our algorithm diverges from the classical algorithm of Martelli and Montanari in what concerns the rules 1 (Term Decomposition) and 6 (Failure Rule). Rule 1 is triggered when the value , resulting from the composition of the approximation degree, , of the symbols at the root in the terms to be unified and the accumulated approximation degree , is equal or greater than and, also, greater than (the last condition deals with the case where and ). Otherwise, Rule 6 is triggered and the unification process ends with failure. Usually, given two expressions and , if there is a successful transition sequence, , then we write that , being the -wmgu of and , and is their unification degree.
In the particular case where , no thresholding effects are achieved by our weak unification algorithm for supporting the basic (non-thresholded yet) operational semantics of FASILL. In the FASILL system, the user can set the cut value by modifying the value of the flag
lambda_unification (whose value is by default).
For more details see:
This predicate returns the thresholded weak most general unifier (lambda-wmgu) WMGU of the expressions ExpressionA and ExpressionB with level Threshold.
This predicate returns the weak most general unifier (wmgu) WMGU of the expressions ExpressionA and ExpressionB.
This predicate returns the most general unifier (mgu) MGU of the expressions ExpressionA and ExpressionB.
This predicate returns the (W)MGU of the expressions ExpressionA and
ExpressionB using the (possible weak) unification algorithm. The FASILL
system allows selecting the unification algorithm by setting the value of
true (WMGU) or
false (MGU). If weak
unification is active, it is possible to choose the unification threshold
by setting the flag
bot by default).
This predicate succeds when Expression does not contain the variable Variable.