Re: FW: Discussion on log:notIncludes

Thank you very much William, your approach hinted us to make
log:collectAllIn
premis order independent in
https://github.com/josd/eye/releases/tag/v21.1215.1908

So when you could install that version,
http://ppr.cs.dal.ca:3002/n3/editor/s/Io4Pby3y
should then give

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

So now we might declare victory :-)

Kind regards,
Jos

-- https://josd.github.io


On Wed, Dec 15, 2021 at 3:52 PM William Van Woensel <
william.vanwoensel@gmail.com> wrote:

> 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> 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> 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>
> *Date: *Monday, December 13, 2021 at 9:29 AM
> *To: *William Van Woensel <william.vanwoensel@gmail.com>
> *Cc: *Jos De Roo <josderoo@gmail.com>, Pierre-Antoine Champin <
> pierre-antoine.champin@ercim.eu>, Gregg Kellogg <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
>
>
>
>
>
>
>
>