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₁, ..., t_n) and g(s₁, ..., 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₁ and E₂ is obtained by a state transformation sequence starting from an initial state <G ≡ {E₁ ≈ E₂}, id, α₀>, where id is the identity substitution and α₀ = ⊤ is the supreme of (L,≤): <G, id, α₀> ⇒ <G₁, θ₁, α₁> ⇒ ... ⇒ <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₁ and E₂ 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₁ and E₂ 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.