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

[Murat K. <mur...@st...>]

Hi Barry,

thanks for your answer, it did not only made parts of the implementation
clearer, but more importantly also your intention behind them.
Since I don't want to steal too much of your time, I'll try to be brief,
too.

1) Interesting, but understandable. (It is possible, of course, but
would require checking, if the Builtin can handle the particular situation.)
2) I understand your concern towards query-independence (I think). Also,
I understand where the implementation is restricted in respect to query
evaluation (predicates are gone, only precomputed facts remain), which
really is a consequence of the former. I think, where I do not follow is
that the following two queries deliver different results.

?- EQUAL(5,?x).

eq(?x,?y) :- EQUAL(?x,?y).
?- eq(5,?x).

Note that I do understand /why/ that is, I only don't think those
programs /ought/ to behave differently. But then again, I am no expert
in logic programming, and my guts may be simply wrong. :)

Thanks again for that piece of insight. Time for some more code diving. :]

Greetings,
Murat

B.Sc.
Hasso-Plattner-Institute
www.hpi-web.de


Barry Bishop wrote:
> 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
>>     
>
>