Operational semantics of FASILL

Rules in a FASILL program have the same role than clauses in PROLOG (or MALP [8, 4, 11]) programs, that is, stating that a certain predicate relates some terms (the head) if some conditions (the body) hold.

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 (w.m.g.u.), following the line of Bousi∼Prolog [5]. Roughly speaking, the weak unification algorithm states that two expressions (i.e, terms or atomic formulas) f(t1,...,tn) and g(s1,...,sn) 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 ti and si 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 [16] for arbitrary complete lattices. We formalize it as a transition system supported by a similarity-based unification relation “⇒”. The unification of the expressions E1 and E2 is obtained by a state transformation sequence starting from an initial state ⟨G ≡ {E1 ≈ E2},id,α0⟩, where id is the identity substitution and α0 = ⊤ is the supreme of (L,≤): ⟨G,id,α0⟩ ⇒ ⟨G1,θ1,α1⟩ ⇒ ··· ⇒ ⟨Gn,θn,αn⟩. When the final state ⟨Gn,θn,αn⟩, with Gn = ∅, is reached (i.e., the equations in the initial state have been solved), the expressions E1 and E2 are unifiable by similarity with w.m.g.u. θn and unification degree αn. Therefore, the final state ⟨∅,θn,αn⟩ signals out the unification success. On the other hand, when expressions E1 and E2 are not unifiable, the state transformation sequence ends with failure (i.e., Gn = Fail).

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

  1. ⟨{f(t1,...,tn)≈g(s1,...,sn)} ∪ E , θ, r1⟩ ⇒ ⟨{t1 ≈ s1,...,tn ≈ sn} ∪ E, θ, r1 ∧ r2⟩ if R(f,g)=r2 >⊥
  2. ⟨{f(t1,...,tn)≈g(s1,...,sn)} ∪ E , θ, r1⟩ ⇒ ⟨{t1 ≈ s1,...,tn ≈ sn} ∪ E, θ, r1 ∧ r2⟩ if R(f,g)=r2 >⊥
  3. ⟨ { X ≈ t } ∪ E , θ , r1 ⟩ ⇒ ⟨(E){X/t},θ{X/t}, r1⟩ if X not in Var( t )
  4. ⟨{t ≈X}∪E, θ, r1⟩ ⇒ ⟨{X ≈ t} ∪ E, θ, r1⟩
  5. ⟨{X ≈t}∪E, θ, r1⟩ ⇒ ⟨Fail, θ, r1⟩ if X ∈ Var(t)
  6. ⟨{f(t1,...,tn)≈g(s1,...,sn)} ∪ E, θ, r1⟩ ⇒ ⟨Fail, θ, r1⟩ if R(f,g)=⊥

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 coped 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.

Usually, given two expressions E1 and E2, if there is a successful transition sequence, ⟨{E1 ≈ E2},id,⊤⟩ ⇒⋆ ⟨∅,θ,r⟩, then we write that wmgu(E1,E2) = ⟨θ,r⟩, being θ the weak most general unifier of E1 and E2, and r is their unification degree.

Finally note that, in general, a w.m.g.u. of two expressions E1 and E2 is not unique [16]. Certainly, the weak unification algorithm only computes a representative of a w.m.g.u. class, in the sense that, if θ = {x1/t1,...,xn/tn} is a w.m.g.u., with degree β, then, by definition, any substitution θ′ = {x1/s1,...,xn/sn}, satisfying R(si,ti) > ⊥, for any 1 ≤ i ≤ n, is also a w.m.g.u. with approximation degree β′ = β ∧(∧n1 R(si,ti)), where “∧′′ is a selected t-norm. However, observe that, the w.m.g.u. representative computed by the weak unification algorithm is one with an approximation degree equal or greater than other w.m.g.u. As in the case of the classical syntactic unification algorithm, our algorithm always terminates returning a success or a failure.

In order to describe the procedural semantics of the FASILL language, in the following we denote by C[A] a formula where A is a sub-expression (usually an atom) which occurs in the –possibly empty– context C[] whereas C[A/A′] means the replacement of A by A′ in the context C[]. Moreover, Var(s) denotes the set of distinct variables occurring in the syntactic object s and θ[Var(s)] refers to the substitution obtained from θ by restricting its domain to Var(s). In the next definition, we always consider that A is the selected atom in a goal Q and L is the complete lattice associated to Π.

Definition 2.1 (Computational Step). Let Q be a goal and let σ be a substitution. The pair ⟨Q, σ⟩ is a state. Given a 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:

  1. Successful step (denoted as ->SS):
    ⟨Q[A], σ⟩ ->SS ⟨Q[A/B∧r]θ, σθ⟩ if A′ ← B ∈ Π, wmgu(A,A′) = ⟨θ,r⟩
  2. Failure step (denoted as ->FS):
    ⟨Q[A], σ⟩ ->FS ⟨Q[A/⊥], σ ⟩ if there is no A′ ← B ∈ Π such that wmgu(A,A′) = ⟨θ,r⟩, r > ⊥
  3. Interpretive step (denoted as ->IS):
    ⟨Q[@(r1,...,rn)], σ⟩ ->IS ⟨Q[@(r1,...,rn)/rn+1], σ⟩ if [[@]](r1,...,rn)=rn+1

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 (f.c.a.) for that derivation.

References

  • [1] R.Caballero, M.Rodríguez-Artalejo & C.Romero-Díaz(2014): A Transformation-based implementation for CLP with qualification and proximity. Theory and Practice of Logic Programming 14(1), pp. 1–63. Available at http://dx.doi.org/10.1017/S1471068412000014.
  • [2] F. A. Fontana (2002): Likelog for flexible query answering. Soft Computing 7(2), pp. 107–114.
  • [3] F. Formato, G. Gerla & M.I. Sessa (2000): Similarity-based Unification. Fundamenta Informaticae 41(4), pp. 393–414.
  • [4] P. Julián-Iranzo, G.Moreno & J. Penabad(2009): On the Declarative Semantics of Multi-Adjoint Logic Programs. In: Proc. of 10th Intl Work-Conference on Artificial Neural Networks (Part I), IWANN’09, Springer Verlag, LNCS 5517, pp. 253–260. Available at http://dx.doi.org/10.1007/978-3-642-02478-8_32.
  • [5] P. Julián-Iranzo & C. Rubio-Manzano (2009): A declarative semantics for Bousi∼Prolog. In: Proc. of 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP’09, ACM, pp. 149–160. Available at http://doi.acm.org/10.1145/1599410.1599430.
  • [6] P. Julián-Iranzo & C. Rubio-Manzano (2010): An efficient fuzzy unification method and its implementation into the Bousi∼Prolog system. In: Proc. of the 2010 IEEE International Conference on Fuzzy Systems, IEEE, pp. 1–8. Available at http://dx.doi.org/10.1109/FUZZY.2010.5584193.
  • [7] M. Kifer & V. S. Subrahmanian (1992): Theory of generalized annotated logic programming and its applications. Journal of Logic Programming 12, pp. 335–367.
  • [8] J. Medina, M. Ojeda-Aciego & P. Vojtásˇ (2004): Similarity-based Unification: a multi-adjoint approach. Fuzzy Sets and Systems 146, pp. 43–62.
  • [9] P. J. Morcillo, G. Moreno, J. Penabad & C. Vázquez (2010): A Practical Management of Fuzzy Truth Degrees using FLOPER. In: Proc. of 4nd. Intl. Symposium on Rule Interchange and Applications, RuleML’10, Springer Verlag, LNCS 6403, pp. 20–34. Available at http://dx.doi.org/10.1007/978-3-642-16289-3_4.
  • [10] G. Moreno, J. Penabad & C. Vázquez (2013): Relaxing the Role of Adjoint Pairs in Multi-adjoint Logic Programming. In I. Hamilton & J. Vigo-Aguiar, editors: Proc. of 13th International Conference on Mathematical Methods in Science and Engineering, CMMSE’13 (Volume III), pp. 1156–1167.
  • [11] G. Moreno, J. Penabad & C. Vázquez (2014): Fuzzy Sets for a Declarative Description of Multi- adjoint Logic Programming. In: Proc. of the 9th International Conference on Rough Sets and Cur- rent Trends in Soft Computing, RSCTC 2014, Springer Verlag, LNCS 8536, pp. 71–82. Available at http://dx.doi.org/10.1007/978-3-319-08644-6_7.
  • [12] G. Moreno & C. Vázquez (2014): Fuzzy Logic Programming in Action with FLOPER. Journal of Software Engineering and Applications 7, pp. 237–298. Available at http://dx.doi.org/10.4236/jsea.2014.74028.
  • [13] S. Muñoz-Hernández, V. Pablos Ceruelo & H. Strass (2011): RFuzzy: Syntax, semantics and implementation details of a simple and expressive fuzzy tool over Prolog. Information Sciences 181(10), pp. 1951–1970. Available at http://dx.doi.org/10.1016/j.ins.2010.07.033.
  • [14] H. T. Nguyen & E. A. Walker (2006): A First Course in Fuzzy Logic. Chatman & Hall, Boca Rato ́n, Florida. Third edition.
  • [15] C. Rubio-Manzano & P. Julián-Iranzo (2014): A Fuzzy linguistic prolog and its applications. Journal of Intelligent and Fuzzy Systems 26(3), pp. 1503–1516. Available at http://dx.doi.org/10.3233/IFS-130834.
  • [16] M. I. Sessa (2002): Approximate reasoning by similarity-based SLD resolution. Theoretical Computer Sci- ence 275(1-2), pp. 389–426. Available at http://dx.doi.org/10.1016/S0304-3975(01)00188-8.