FASILL operational-semantics

As a logic language, FASILL inherits the concepts of substitution, unifier and most general unifier (mgu).
Some of them are extended to cope with similarities. Concretely, the most general unifier is replaced by the concept of **weak most general unifier**
(wmgu) and a weak unification algorithm is introduced to compute it. Roughly speaking, the weak unification algorithm states that two expressions
(i.e, terms or atomic formulas) f(t_{1}, ..., t_{n}) and g(s_{1}, ..., s_{n}) weakly unify if the root symbols f
and g are close with a certain degree (i.e. R(f, g) = r > ⊥) and each of their arguments t_{i} and s_{i} weakly unify. Therefore,
there is a weak unifier for two expressions even if the symbols at their roots are not syntactically equals (f ≢ g).

More technically, the weak unification algorithm we are using is a reformulation/extension of the one which appears in [Approximate reasoning by similarity-based SLD resolution] for arbitrary complete lattices.
We formalize it as a transition system supported by a similarity-based unification relation (⇒). The unification of the expressions E_{1} and E_{2}
is obtained by a state transformation sequence starting from an initial state <G ≡ {E_{1} ≈ E_{2}}, id, α_{0}>, where id is the identity
substitution and α_{0} = ⊤ is the supreme of (L,≤): <G, id, α_{0}> ⇒ <G_{1}, θ_{1}, α_{1}> ⇒ ... ⇒ <G_{n}, θ_{n}, α_{n}>.
When the final state <G_{n}, θ_{n}, α_{n}>, with G_{n}= ∅, is reached (i.e., the equations in the initial state have
been solved), the expressions E_{1} and E_{2} are unifiable by similarity with wmgu θ_{n} and unification degree α_{n}.
Therefore, the final state <G_{n}, θ_{n}, α_{n}> signals out the unification success. On the other hand, when expressions
E_{1} and E_{2} are not unifiable, the state transformation sequence ends with failure (i.e., G_{n} = Fail).

The similarity-based unification relation, (⇒), is defined as the smallest relation derived by the following set of transition rules (where Var(t) denotes the set of variables of a given term t):

Rule 1 decomposes two expressions and annotates the relation between the function (or predicate) symbols at their root. The second rule eliminates spurious information and the fourth rule interchanges the position of the symbols to be handled by other rules. The third and fifth rules perform an occur check of variable X in a term t. In case of success, it generates a substitution {X/t}; otherwise the algorithm ends with failure. It can also end with failure if the relation between function (or predicate) symbols in R is ⊥, as stated by Rule 6.

Rules in a FASILL program have the same role than clauses in Prolog programs, that is, stating that a certain predicate relates some terms (the head) if some conditions (the body) hold. The procedural semantics of FASILL is defined in a stepwise manner as follows. First, an operational stage is introduced which proceeds similarly to SLD resolution in pure logic programming, returning an expression still containing values and connectives. Then, an interpretive stage evaluates these connectives and produces a final answer.

Let Q be a goal and σ a substitution. The pair <Q; σ> is a state. Given a FASILL program <Π, R, L> and a t-norm ∧ in L, a computation is formalized as a state transition system, whose transition relation (⇝) is the smallest relation satisfying these rules:

A derivation is a sequence of arbitrary lenght <Q; id> ⇝^{*} <Q'; σ>. As usual, rules are renamed apart.
When Q' = r ∈ L, the state <r; σ> is called a **fuzzy computed answer** (fca) for that derivation.