FASILL documentation Source fasill_unification

# Unification

This library provides predicates for unification.

In FASILL the concepts of unifier and most general unifier (mgu) are extended to cope with similarities. Let $\mathcal{R}$ be a similarity relation, $\lambda$ be a cut value and $\mathcal{E}_1$ and $\mathcal{E}_2$ be two expressions. The substitution $\theta$ is a weak unifier of level $\lambda$ for $\mathcal{E}_1$ and $\mathcal{E}_2$ with respect to $\mathcal{R}$ if its unification degree $\hat{\mathcal{R}}(\mathcal{E}_1\theta, \mathcal{E}_2\theta) \geq \lambda$. Note that our algorithm uses a different notion of unification state, where an extra component accumulates an approximation degree. The unification of the expressions $\mathcal{E}_1$ and $\mathcal{E}_2$ is obtained by a state transformation sequence starting from an initial state $\langle\{\mathcal{E}_1 \approx \mathcal{E}_2\}, id, \alpha_0\rangle$, where $id$ is the identity substitution and $\alpha_0 = \top$ is the supremum of the lattice $(L, \leq)$. The thresholded similarity-based unification relation, "$\Rightarrow_\lambda$", is defined as the smallest relation derived by the following set of transition rules (where $\mathcal{V}ar(t)$ denotes the set of variables of a given term $t$):

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 $v_2$, resulting from the composition of the approximation degree, $\mathcal{R}(f, g)$, of the symbols at the root in the terms to be unified and the accumulated approximation degree $v_1$, is equal or greater than $\lambda$ and, also, greater than $\bot$ (the last condition deals with the case where $\mathcal{R}(f, g) \geq \lambda$ and $\lambda = \bot$). Otherwise, Rule 6 is triggered and the unification process ends with failure. Usually, given two expressions $\mathcal{E}_1$ and $\mathcal{E}_2$, if there is a successful transition sequence, $\langle\{\mathcal{E}_1 \approx \mathcal{E}_2\}, id, \top\rangle \Rightarrow_\lambda^* \langle\emptyset, \theta, v\rangle$, then we write that $wmgu^\lambda_\mathcal{R}(\mathcal{E}_1, \mathcal{E}_2) = \langle \theta, v\rangle$, being $\theta$ the $\lambda$-wmgu of $\mathcal{E}_1$ and $\mathcal{E}_2$, and $v \geq \lambda$ is their unification degree.

In the particular case where $\lambda = \bot$, 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 $\lambda$ by modifying the value of the flag lambda_unification (whose value is $\bot$ by default).

For more details see:

• Julián-Iranzo, Pascual, Ginés Moreno, and Jaime Penabad. "Thresholded semantic framework for a fully integrated fuzzy logic language." Journal of logical and algebraic methods in programming 93 (2017): 42-67. https://doi.org/10.1016/j.jlamp.2017.08.002

#### lambda_wmgu/5

lambda_wmgu( +ExpressionA, +ExpressionB, +Threshold, +OccursCheck, ?WMGU )

This predicate returns the thresholded weak most general unifier (lambda-wmgu) WMGU of the expressions ExpressionA and ExpressionB with level Threshold.

#### wmgu/4

wmgu( +ExpressionA, +ExpressionB, +OccursCheck, ?WMGU )

This predicate returns the weak most general unifier (wmgu) WMGU of the expressions ExpressionA and ExpressionB.

#### mgu/4

mgu( +ExpressionA, +ExpressionB, +OccursCheck, ?MGU )

This predicate returns the most general unifier (mgu) MGU of the expressions ExpressionA and ExpressionB.

#### unify/4

unify( +ExpressionA, +ExpressionB, +OccursCheck, ?WMGU )

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 the flag weak_unification to true (WMGU) or false (MGU). If weak unification is active, it is possible to choose the unification threshold by setting the flag lambda_unification (bot by default).

#### occurs_check/2

occurs_check( +Variable, +Expression )

This predicate succeds when Expression does not contain the variable Variable.