Navigation
Interesting Links
Home | How to Use FLOPER

Declarative Traces

Domain of weight values

It is possible to extend the information given by a lattice. Let us consider consider now the so called domain of weight values W used in the QLP (Qualified Logic Programming framework), whose elements are intended to represent proof costs, measured as the weighted depth of proof trees. In essence, W can be seen as lattice (ℕ ∪ {∞}, ≥), where ≥ is the reverse of the usual numerical ordering (with ∞ ≥ d for any d ∈ ℕ) and thus, the bottom elements is ∞ and the top element is 0 (and not vice versa). Moreover, lattice W is just the Dedeking-MacNeille completion of ℕ. Note that in this lattice the arithmetic operation “+” plays the role of a conjunction (it is easy to prove that in this setting such definition of & verifies the properties required).

Moreover, we can obtain the residual implication of the “+” t-norm, defined as
[[y ← z]] = sup{t ∈ W : t + z ← y},
 
which in this particular case acquires the following form:
 
So, the reader can easily check that (+, ←) conforms an adjoint pair in (ℕ ∪ {∞}, ≥), which implies that W is in fact a multi-adjoint lattice.
 
A valid implementation of W lattice presents the following definitions:
 
member(infty).
member(X) :- number(X).
leq(infty,X).
leq(X,Y):-X>=Y.
top(0).
bot(infty).
and_plus(X,infty,infty). and_plus(infty,X,infty).
and_plus(X,Y,Z):-Z is X+Y.
W Lattice
 
Now, if we call V to the multi-adjoint lattice ([0,1], ≤) based on real numbers in the unit interval presented in the introduction section, which is equipped with three adjoint pairs modeling implication and conjunction symbols collected from the Lukasiewicz logic, Gödel intuitionistic logic and product logic then, in the Cartesian product V × W we will find the top and bottom elements (1, 0) and (0,∞), respectively, as well as the following definitions of conjunction operations (among other connectives) whose names are mirroring to extensions of the product logic and Lukasiewicz logic:
 
[[(v1,w1) &P+ (v2,w2)]] = (v1 * v2, w1 + w2)
[[(v1,w1) &L+ (v2,w2)]] = (max(0, v1 + v2 − 1), w1 + w2)
 
Now, each element has two components, coping with truth degrees and cost measures. In order to be loaded into FLOPER, we must define in Prolog the new lattice, whose elements could be expressed, for instance, as data terms of the form "info(Fuzzy Truth Degree, Cost Number Steps)":
 
member(info(X,W)) :-number(X), 0=<X,X=<1,(W=infty,!; number(W),1=<W).
leq(info(X1,W1),info(X2,W2)):-X1 =< X2, (W1=infty,!; number(W2), W2 =< W1).
bot(info(0,infty)).
top(info(1,1)).
 
pri_add(infty,_,infty).
pri_add(_,infty,infty).
pri_add(X,Y,Z) :- number(X), number(Y), Z is X+Y.
and_prod(info(X,W1),info(Y,W2),info(Z,W3)) :- pri_prod(X,Y,Z), pri_add(W1,W2,W3).
V × W Lattice
 
Finally, if the weights assigned to the rules of our running example be “info(0.4,1)” for R1, “info(0.8,1)” for R2, “info(0.9,1)” for R3 and so on, for goal “c(X)” we would obtain the desired f.c.a. <info(0.38, 4); {X/peter}> with the obvious meaning that we need 4 admissible steps to prove that the query is true at a 38% degree when X is "peter".
 

Domain of strings

One step beyond, we will also see that if instead of the number of computational steps, we are interested in knowing more detailed data about the set of program rules and connective definitions evaluated for obtaining each solution then, instead of W it will be mandatory to use a new lattice S based on strings or  labels (i.e., sequences of characters) for generating the Cartesian product V × S. In order to achieve our purposes, we firstly must to show not only that S is a complete multi-adjoint lattice, but also that the concatenation operation of strings, usually called append in many programming languages, plays the role of a conjunction connective in such lattice. In order to be loaded into FLOPER, we need to define again the new lattice as a Prolog program, whose elements will be expressed now as data terms of the form "info(Fuzzy Truth Degree, Label)" as shown below (note that the complex version of the average connective is called here agr_aver2 and invokes the simple version agr_aver).
 
member(info(X,_)) :-number(X),0=<X,X=<1.
bot(info(0,_)).
top(info(1,_)).
leq(info(X1,_),info(X2,_)) :- X1 =< X2.
and_prod(info(X1,X2),info(Y1,Y2),info(Z1,Z2)) :-
             pri_prod(X1,Y1,Z1),
             pri_app(X2,Y2,Dat1),
             pri_app(Dat1,’&PROD.’,Z2).
%% other connectives
 
pri_app(X,Y,Z) :- name(X,L1), name(Y,L2), append(L1,L2,L3), name(Z,L3).
pri_prod(X,Y,Z) :- Z is X * Y.
%% other primitives
V × S Lattice
 
Here, we see that when implementing for instance the conjunction operator of the Product Logic, in the second component of our extended notion of “truth degree”, we have appended the labels of its arguments with the label '&PROD.' (see clauses defining and_prod, pri_app and append). Of course, in the fuzzy program to be run, we must also take into account the use of labels associated to the program rules. For instance, the set of rules of our example must have the form:
 
y(peter) with info(0.4, 'RULE1.').
y(mary) with info(0.8, 'RULE2.').
h(peter) with info(0.9, 'RULE3.').
h(mary) with info(0.3, 'RULE4.').
e(peter) with info(0.5, 'RULE5.').
e(mary) with info(0.95, 'RULE6.').
c(X) <prod (h(X) |prod e(X)) &prod y(X) with info(1, 'RULE7.').

Program P1 with extended information

 
Now, the reader can easily test that, after executing goal p(X), we obtain the desired fuzzy computed answers which includes the desired declarative trace regarding program-rules/connective-calls/primitive-operators evaluated till finding the final solution:
 
>> run.
 
[Truth_degree=info(0.72, RULE1.RULE2.RULE3.RULE4.
                                    @AVER2.|GODEL.|LUKA.
                                    @AVER.&GODEL.&PROD.), X=a]
f.c.a of extended P1

Domain of strings with primitive operators

With very little effort, we can extend the previous lattice to have into account also the exploited primitive operators in the interpretive phase. We include a label in each primitive operator in order to identify them. For instance, "#PROD" refers to the product primitive operator.
 
member(info(X,_)) :-number(X),0=<X,X=<1.
bot(info(0,_)).
top(info(1,_)).
leq(info(X1,_),info(X2,_)) :- X1 =< X2.
and_prod(info(X1,X2),info(Y1,Y2),info(Z1,Z2)) :-
             pri_prod(X1,Y1,Z1,DatPROD),pri_app(X2,Y2,Dat1),
             pri_app(Dat1,’&PROD.’,Dat2),pri_app(Dat2,DatPROD,Z2).
%% other connectives
 
pri_app(X,Y,Z) :- name(X,L1), name(Y,L2), append(L1,L2,L3), name(Z,L3).
pri_prod(X,Y,Z,’#PROD.’) :- Z is X * Y.
%% other primitives
V × S Lattice
 
The result of executing again goal "c(X)"  will be:
 
>> run.
 
[Truth_degree=info(0.72, RULE1.RULE2.RULE3.RULE4.
                                    @AVER2.|GODEL.#MAX.|LUKA.
                                    #ADD.#MIN.@AVER.#ADD.#DIV.
                                    &GODEL.#MIN.&PROD.#PROD.), X=a]
f.c.a of extended P1
 

In this fuzzy computed answer we obtain both the truth value (0.72) and substitution (X = a) associated to our goal, but also the sequence of program rules exploited when applying admissible steps as well as the proper fuzzy connectives evaluated during the interpretive phase, also detailing the set of primitive operators (of the form #label) they call.