Re: FW: Discussion on log:notIncludes

Rather miraculously, a rule like


                :cmp0 a :task.

:cmp1 a :task.



:cmp0 :subTask :task99.



{(?task {?x :subTask ?task.} ?ys) log:collectAllIn <> . ?x a :task. ?ys log:equalTo ().}

       => { ?x :empty1 :true }.

Works in jen3 because of its particular clause ordering – clauses with “universals” (such as log:collectAllIn) are pushed to the very back of the rule body, unless there’s a clause with (some) terms that are not yet bound: for a triple pattern, all s/p/o need to be bound; for a builtin clause, it depends on the particular builtin whether s, o, or both need to be bound.

For instance, in the case of the rule above, this ordering is:

“?x a :task.” “?ys log:equalTo ()” “{(?task {?x :subTask ?task.} ?ys) log:collectAllIn <>”

Re the log:equalTo builtin in the second clause: it only requires one of its arguments to be bound (“?ys” will be bound to the empty list) so it is not pushed back. E.g., the builtin log:notEqualTo would require all its arguments to be bound. But, the universal is pushed to the back of the rule body.

In more detail:

if current variable bindings *do not* match the builtin’s domain, then:
do not delay this clause (priority 0) (we want this clause to fail as quick as possible)

if current variable bindings *do* match the builtin’s domain, then:
if *not all* required terms are bound, then:
delay this clause as long as possible (priority -2)
if *all* required terms are bound, then:
                if the builtin is a “universal”, then:
                                delay (priority -1)
                else, then:
                                do not delay (priority 0)

(e.g., the domain for math:sum would require a subject to be a concrete list with numbers, and an object that is either numeric or unbound)

The reasoning behind this delay for universal builtins (e.g., log:collectAllIn) is that we want any co-referring variable, i.e., that also occurs in other rule premises (in this case, “?x”), to be bound before the universal builtin is executed. Else, log:collectAllIn will simply iterate over all “x’s” with a :subTask relation, and it will be unclear what “?x” in the other premise (and rule conclusion) is referring to.

This is a very straightforward heuristic and I’m sure this will fail in some cases, but it seems to work for the cases I’ve considered until now.


W

From: Jos De Roo <josderoo@gmail.com>
Date: Wednesday, December 15, 2021 at 9:38 AM
To: William Van Woensel <william.vanwoensel@gmail.com>
Cc: public-n3-dev@w3.org <public-n3-dev@w3.org>
Subject: Re: FW: Discussion on log:notIncludes
Was declaring victory for http://ppr.cs.dal.ca:3002/n3/editor/s/0HrLHpgS too early ..
There is still an issue with premis order dependency  as none of the following gives an answer:

{?Scope e:findall (?task {?x :subTask ?task.} ?ys). ?x a :task. ?ys log:equalTo ().} => { ?x :empty1 :true }.
{?Scope e:find (?task {?x :subTask ?task.} ?ys). ?x a :task. ?ys log:equalTo ().} => { ?x :empty2 :true }.
{(?task {?x :subTask ?task.} ?ys) log:collectAllIn ?Scope. ?x a :task. ?ys log:equalTo ().} => { ?x :empty3 :true }.

{?Scope e:findall (?task {?x :subTask ?task.} ?ys). ?ys log:equalTo (). ?x a :task.} => { ?x :empty1 :true }.
{?Scope e:find (?task {?x :subTask ?task.} ?ys). ?ys log:equalTo (). ?x a :task.} => { ?x :empty2 :true }.
{(?task {?x :subTask ?task.} ?ys) log:collectAllIn ?Scope. ?ys log:equalTo (). ?x a :task.} => { ?x :empty3 :true }.

{?ys log:equalTo (). ?Scope e:findall (?task {?x :subTask ?task.} ?ys). ?x a :task.} => { ?x :empty1 :true }.
{?ys log:equalTo (). ?Scope e:find (?task {?x :subTask ?task.} ?ys). ?x a :task.} => { ?x :empty2 :true }.
{?ys log:equalTo (). (?task {?x :subTask ?task.} ?ys) log:collectAllIn ?Scope. ?x a :task.} => { ?x :empty3 :true }.

For the moment I see only one solution which is with log:notIncludes and bind all the variables in its object
via extra :subTask declarations like in http://ppr.cs.dal.ca:3002/n3/editor/s/fCR2HSVh
That gives the expected answer
:cmp1 :empty :true.

Kind regards,
Jos

-- https://josd.github.io


On Mon, Dec 13, 2021 at 8:15 PM Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>> wrote:
Doerthe was testing alternative SNAF ways in http://ppr.cs.dal.ca:3002/n3/editor/s/0HrLHpgS
but there is an issue with e:find which is now solved in https://github.com/josd/eye/releases/tag/v21.1213.1906
So if William could do an upgrade, the results should then be

:cmp1 :empty1 :true.
:cmp1 :empty2 :true.
:cmp1 :empty3 :true.
:cmp1 :empty4 :true.
:cmp1 :empty5 :true.
:cmp1 :empty6 :true.

Kind regards,
Jos

-- https://josd.github.io


On Mon, Dec 13, 2021 at 6:12 PM William Van Woensel <william.vanwoensel@gmail.com<mailto:william.vanwoensel@gmail.com>> wrote:
Dear mailing list,

Below you can find a conversation on log:notIncludes that may be of interest!


Regards,

William

From: Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>>
Date: Monday, December 13, 2021 at 9:29 AM
To: William Van Woensel <william.vanwoensel@gmail.com<mailto:william.vanwoensel@gmail.com>>
Cc: Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>>, Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu<mailto:pierre-antoine.champin@ercim.eu>>, Gregg Kellogg <gregg@greggkellogg.net<mailto:gregg@greggkellogg.net>>
Subject: Re: Discussion on log:notIncludes
Dear William,

Sorry for my late answer. I agree with your explanation and I also think that the main question is: what does the local scoping of variables mean? Related to that, it is also important to know where exactly our negation is (so we have „implicit negation :) ).


To come to your examples



To continue our discussion on log:notIncludes (and in general the floundering issue) I found a good link yesterday: https://github.com/dtonhofer/prolog_notes/blob/master/other_notes/about_negation/floundering.md


I was wondering why my particular example made sense, but the one in the above article does not, even when *not* exposing variables outside of the “notIncludes” statement.


Starting from the beginning, the following doesn’t make sense much sense because of floundering (as mentioned in the article):


:bart :allergicTo :penicillin .


{ <> log:notIncludes { :bart :allergicTo ?y } } => { :bart :canTake ?y } . # no

{ <> log:notIncludes { :bart :allergicTo :eyrthromycin } } => { :bart :canTake :eyrthromycin } . # yes (contradiction; above rule did not output anything, meaning that bart cannot take anything)

{ <> log:notIncludes { :lisa :allergicTo ?y } } => { :lisa :canTake ?y } . # yes, but don't know what to bind to y


(there is much more in the article, such as possible general solutions to this problem)


This actually made clear to me why having “builtin-local” variables, i.e., not exposing “y” to the rule consequent, could be a solution to the problem, as they would at least prevent these use cases. I believe this was implied during our last discussion but I hadn’t gotten that far yet :-)
The examples here seems to assume that the variable here is universally quantified on top level.



The problem is indeed, that if we wanted the rule to work as it might was intended by its inventor, we would have to list everything which :bart can take which would be everything (in the world) except :penicillin. We can’t list everything except penicillin.

In the last rule we have the same, but here, there is no exception. We can state :lisa :canTake ?y., if we allow universal variables on top level and have some shorthand for „Lisa can take everything“.





However, if we slightly re-write these examples to not expose any builtin-local variables:


:bart :allergicTo :penicillin .


{ <> log:notIncludes { :bart :allergicTo ?y } } => { :bart :canTakeSomeDrug true } . # still no

{ <> log:notIncludes { :lisa :allergicTo ?y } } => { :lisa :canTakeSomeDrug true } # still yes


This still doesn’t make much sense to me – due to the intuition that, just because bart has an allergy to one particular drug, it doesn’t mean they cannot take some other drug. (This is similar to the first statement in the first example: just because bart has an allergy to one particular drug, it doesn’t mean they cannot take some other drug.)
Here, it depends on the meaning you assume for the universal. If you are consistent with the example above, you would still have universal scoping on top level. So, what you say here would be in FOL:

\forall y: (\not allegicTo(bart,y))-> canTakeSomeDrug(bart, true).

Which means the same as:

(\exists y: \not (allegicTo(bart,y)))-> canTakeSomeDrug(bart, true).

In that interpretation, the rule makes sense.

What you describe (and what is also implemented) is different. From your lines above I see that you understand the rule as:

( \not (\exists y: allegicTo(bart,y)))-> canTakeSomeDrug(bart, true).

With that interpretation, the rule does not make sense, but the behavior of the reasoner does.



Now, compare with my use case:


:cmp0 :subTask :s0 .


{ <> log:notIncludes { :cmp0 :subTask ?y } } => { :cmp0 :empty :true } . # no (e.g., “cmp0” could have been bound in an earlier triple)

{ <> log:notIncludes { :cmp1 :subTask ?y } } => { :cmp1 :empty :true } . # yes (idem)


Here, the mere mentioning of a composite task with the property “subTask" *indeed means* that it is not empty. Having one subtask means something is not empty (counter-example).


I can again translate.

The rule you want to express is:
( \not (\exists y: subTask(cmp0,y)))-> isEmpty(cmp0, true).

What we would get if we had the y quantified on top level would be:

\forall y: (   \not (subTask(cmp0,y)))-> isEmpty(cmp0, true).

which can be transformed to:

( \exists y:  \not (subTask(cmp0,y)))-> isEmpty(cmp0, true).


But, in the drug example, the mere mentioning of a person with property “allergicTo” property *does not mean* that they cannot take something. Having one drug allergy does not mean one cannot take some (other) drug (not a counter-example).





So it is related to the meaning we assign to the inference. E.g., the following would make much more sense:


{ <> log:notIncludes { :bart :allergicTo ?y } } => { :bart :hasAllergies false } . # still no, but this is good


Or


{ <> log:notIncludes { :bart :allergicTo ?y } } => { :bart :canTakeAnyDrug true } . # still no, but this is good



Hence I feel that the second drug example (“canTakeSomeDrug”) is rather an anti-pattern, as it does not search for the non-existence of a counter-example – this could be mentioned in the N3 spec (yes remember that thing? >:). Could this, combined with a “builtin-local” scoping of the variables, be a solution for the notIncludes problem? (Sorry if some of you may have already gotten to this point – I just needed a bit more exposition)



As I pointed out above with the examples. I think that the examples of negation where we have „floundering“ are actually cases where the universal quantification which is supposed to be on top-level suddenly switched to a local level. This is something which should not happen and therefore, I agree with Jos that we should be very strict here.

I also see, that the use of negated predicates as you describe them has many use cases and I know that I did similar things before (but with e:findAll, where it is easier to understand the variable as locally quantified). So, I would suggest, that we go for some kind of local variable here.

We could for example use blank nodes in that context and use their specification as it was in the original proposal. There, they are local.

It even works if they are existential quantified. In that case, it still depends on the position of the implicit negation, whether or not we get the meaning you intended in your example. But if we say that the existential quantifier comes before the negation, then your example would work.

It is interesting to see that this is also how cwm sees it. With the original meaning of blank nodes (so no re-interpretation), your example works. You can see that in Cwm: http://ppr.cs.dal.ca:3002/n3/editor/s/yRnwKhdK

Kind regards,
Dörthe