Re: FW: Discussion on log:notIncludes

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
>
>
>
>
>
>
>