- From: William Van Woensel <william.vanwoensel@gmail.com>
- Date: Mon, 13 Dec 2021 17:10:32 +0000
- To: "public-n3-dev@w3.org" <public-n3-dev@w3.org>
- Message-ID: <DM6PR06MB6058DDD81F61C32BDAC7BC82FC749@DM6PR06MB6058.namprd06.prod.outlook.com>
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
Received on Monday, 13 December 2021 17:11:47 UTC