Re: [iris-reasoner-support] Built-ins and Bug(?)

[Barry B. <bar...@st...>]

Hi Murat,

Thanks for your interest in IRIS and thanks for spotting a bug for us!

1) Safe rules in IRIS

By default (using the default constructor of
StandardRuleSafetyProcessor), IRIS allows an arithmetic built-in to
compute up to one missing term, e.g.

q(?Y) :- p(?X), ADD(?X, ?Y, 5) (X is bound, Y can be calculated)

(Strictly speaking, this should not be allowed, because a safe rule in
Datalog is one where *all* head variables appear in positive ordinary
predicates.)

However, only one term (not one variable) can be computed, e.g.

q(?Y) :- p(?Z), ADD(?X, ?X, ?Z)

is not allowed, because two terms of ADD() are unbound. The fact that
both terms are the same variable is not considered. In the case of
addition, a value for X can be determined, but this is not true
generally for arithmetic built-ins, e.g. SUBTRACT( ?X, ?X, 0 ) would
allow any value for ?X, hence rules containing built-in arithmetic
predicates with more than 1 unbound *term* are considered unsafe rules.



2) Unsafe rules in IRIS

As you probably know from the source code, IRIS uses a simple trick to
turn unsafe rules in to safe rules. It simply adds UNIVERSE(?var)
literals to rule bodies for every unbound variable and then does it's
best to make sure that every ground term in the program is added to the
relation for this (Herbrand) universe predicate, e.g.

q(?X, ?Y) :- ADD(?X, ?Y, 5)

is unsafe and IRIS adds two literals to turn it in to this safe rule:

q(?X, ?Y) :- ADD(?X, ?Y, 5), UNIVERSE(?X), UNIVERSE(?Y)

Notice, that technically speaking, this rule only needs to add a single
universe term, either for ?X or for ?Y to make it safe. However, this
choice can alter the behaviour of the program and eventual query result
so the decision was made to try avoid any ambiguity. Therefore, when a
rule is unsafe, all the unbound variables from a built-in will get their
own universe predicate.

Also, ground terms in queries are not considered part of the universe of
terms. The simple reason being, that the model of the program should not
be affected by the query being asked. Again, this is an assumption that
is not clearly documented, but for IRIS, the knowledge base is first
initiliased and queries are later executed against it. (I'm willing to
be persuaded as to whether this is semantically correct!)


3) Your examples

Ex2. some_calc(?X,?Z) :- MULTIPLY(?X,?X,?Y), ADD(?Y,-1, ?Z).

becomes:
some_calc(?X, ?Z) :- MULTIPLY(?X, ?X, ?Y), ADD(?Y, -1, ?Z),
$UNIVERSE$(?Y), $UNIVERSE$(?X), $UNIVERSE$(?Z)

where $UNIVERSE$ contains only the single value '-1' and both built-ins
evaluate to false.


Ex3. eq_ordinary(?x, ?y) :- EQUAL(?x,?y).

becomes:
eq_ordinary(?x, ?y) :- EQUAL(?x,?y), $UNIVERSE$(?X), $UNIVERSE$(?Y)

and since there are no grounds terms in this program, the rule never fires.

4) The bug.

Yes indeed, you have correctly identified a serious bug and I am
somewhat embarrassed that there is no unit test that catches this. I
will try to remedy this situation as soon as possible, but thanks very
much for pointing it out.

For the sake of brevity I will stop now, but I hope this helps you to
understand some of the idiosyncrasies of IRIS.

Kindest regards,
barry


Murat Knecht wrote:
> Hi,
> 
> I have a question regarding built-ins. Having taken a look at the source 
> code, I would like to understand why the following datalog programs do 
> not work as (I) expected. (They are appended below.)
> 
> Program 1 works as expected, but 2 and 3, on the other hand, do not. 
> With 2 I expected to get the correct answer to the calculation, i.e. 24. 
> Program 3 was supposed to deliver 6, obviously. This ought to be 
> possible through the IRIS feature of deducing the last number involved 
> e.g. in a ternary mathematical predicate, but which also applies to the 
> EQUAL-predicate.
> 
> My explanation is that, after building the knowledge base, the facts are 
> all that is left - the rules are not looked at again during query 
> evaluation. This results in the might of the UNIVERSE variable, which 
> ought to solve problems like program 3, to get lost . It also leads to 
> the deduction capabilities of the EQUAL-predicate to not be applied to 
> the constant in the query - producing an empty result set.
> 
> Is my understanding of the matter correct?
> 
> 
> And I would like to know if the following is a bug or intended behavior.
> FiniteUniverseFact: The method
> 
> void extractGroundTerms( Collection<IRule> rules )
> 
> twice extracts the ground terms from the rule's head but never from the 
> body. I suppose this is a copy-and-paste error?
> http://iris-reasoner.svn.sourceforge.net/viewvc/iris-reasoner/iris/trunk/src/org/deri/iris/facts/FiniteUniverseFacts.java?view=markup&pathrev=1593
> 
> Thanks,
> Murat
> 
> 
> ==== 1. ====
> pred1('p1' , 'p2').
> pred2('p2' , 'p3').
> pred(?X,?Z) :- pred1(?X,?Y), pred2(?Y,?Z).
> ?-pred('p1',?X).
> ----------------------------------
> Query:      ?- pred('p1', ?X). ==>> 1 row in 0ms
> Variables:  ?X
> ('p3')
> 
> 
> ==== 2. ====
> some_calc(?X,?Z) :- MULTIPLY(?X,?X,?Y), ADD(?Y,-1, ?Z).
> ?-some_calc(5,?Z).
> ----------------------------------
> Query:      ?- some_calc(5, ?Z). ==>> 0 rows in 0ms
> Variables:  ?Z
> 
> 
> ==== 3. ====
> eq_ordinary(?x, ?y) :- EQUAL(?x,?y).
> ?-eq_ordinary(6,?q).
> ----------------------------------
> Query:      ?- eq_ordinary(6, ?q). ==>> 0 rows in 0ms
> Variables:  ?q
> 
> 
> -------------------------------------------------------------------------
> This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
> Build the coolest Linux based applications with Moblin SDK & win great prizes
> Grand prize is a trip for two to an Open Source event anywhere in the world
> http://moblin-contest.org/redirect.php?banner_id=100&url=/
> _______________________________________________
> iris-reasoner-support mailing list
> iri...@li...
> https://lists.sourceforge.net/lists/listinfo/iris-reasoner-support

-- 
Barry Bishop
Senior Scientific Programmer
Semantic Technology Institute (STI)
University of Innsbruck, Austria
-----------------------------------
E-Mail: bar...@st...
Tel:    +43 512 507 96873
-----------------------------------