Definition of log:includes

[william-vw]

Perhaps I'm overly confusing myself about log:includes .. but it seems to me that the following would be incorrect:

{ { 
    :will :hasName "will"
} log:includes {
    ?x :hasName "will"
} } => {
    :rule1 :out :success
} .

Since ?x :hasName "will" seems much more general than :will :hasName "will" (and hence would not be "included" in the subject formula). Although it seems to meet the definition of the builtin (see https://www.w3.org/2000/10/swap/doc/CwmBuiltins) and Eye considers it to be correct. Inversely, I'd consider the following to be correct:

{ { 
    ?x :hasName "will"
} log:includes {
    :will :hasName "will"

} } => {
    :rule2 :out :success
} .

Which Eye also confirms.

[pchampin]

Aside: comparing EYE and CWM on these examples is misleading, because both are interpreting the quickvar ?x differently (they put the quantifier in different places). In order to ensure the same interpretation, we need explicit quantification:

@forAll :x.
{ { 
    :will :hasName "will"
} log:includes {
    :x :hasName "will"
} } => {
    :rule1 :out :success
} .

Here, EYE and CWM both fire the rule.

@forAll :x.
{ { 
    :x :hasName "will"
} log:includes {
    :will :hasName "will"
} } => {
    :rule2 :out :success
} .

Here, only EYE fires the rule.

[pchampin]

Now, about the question itself :)

?x :hasName "will" seems much more general than :will :hasName "will"

It really depends on where ?x is quantified. In my examples above with explicit quantification (which are in line with how we decided to interpret quickvars), I find it perfectly OK that both rules fire, at least from a purely logical point of view. In both cases, there is a value for ?x (namely, :will) that makes the formula on each side of log:includes equal, and therefore included in each other. So that particular value of ?x makes the rule fire.

Notice that if you replace :success with ?x in the consequence of your rule, EYE will give you :ruleX :out :will.

[william-vw]

I still find it awkward that :will :hasName "will" includes ?x :hasName "will" since in anopen-world interpretation ?x could match anything, including things not in this document.

[william-vw]

Regarding your comparison between cwm and Eye, note that the cwm builtin document states the following:

Formula A includes formula B if there exists some substitution which when applied to B creates a formula B' such that for every > statement in B' is also in A, every variable universally (or existentially) quantified in B' is quantified in the same way in A

So strangely cwm only considers variable substitutions in the object, which is even less intuitive to me ..

[pchampin]

I still find it awkward that :will :hasName "will" includes ?x :hasName "will"

I think it is because you interpret it as {:will :hasName "will"} log:includes {@forAll :x. :x :hasName "will"} or maybe as @forAll :x. {:will :hasName "will"} log:includes {:x :hasName "will"}. Both of these formulae are indeed false.

But in your rule, ?x is quantified to an even higher layer. Let me rephrase your rule in english and in a more imperative way:

• for all ?x
• check if { :will :hasName "will" } includes { ?x :hasName "will" }
• if so, generate the triple :rule1 :out :success

There are many values of ?x for which the rule does not fire. But there is one (:will) for which it does. That's enough for the "success" triple to be generated.

[pchampin]

So strangely cwm only considers variable substitutions in the object, which is even less intuitive to me ..

Agreed, this is very strange of cwm...

[afs]

Just the name "includes" suggests that A is larger B. "A subsumes B". "A is more general than B".
Liskov Substitution Principle -- "can use B where an A is required".

So variables substitution in the object is strange.

Is there the inverse relationship "A refines B"?

[william-vw]

I still find it awkward that :will :hasName "will" includes ?x :hasName "will"

I think it is because you interpret it as {:will :hasName "will"} log:includes {@forAll :x. :x :hasName "will"} or maybe as @forAll :x. {:will :hasName "will"} log:includes {:x :hasName "will"}. Both of these formulae are indeed false.

But in your rule, ?x is quantified to an even higher layer. Let me rephrase your rule in english and in a more imperative way:

* for all ?x

* check if `{ :will :hasName "will" }` includes `{ ?x :hasName "will" }`

* if so, generate the triple `:rule1 :out :success`

There are many values of ?x for which the rule does not fire. But there is one (:will) for which it does. That's enough for the "success" triple to be generated.

Aha .. thanks for clarifying. I didn't see it this way at all - I saw it as a type of containment check where some terms simply may be more general (and not in the context of a rule). Indeed, as @doerthe is known to say, it all depends on the quantification :-)

I collected some tests here: includes1.n3

[william-vw]

Just the name "includes" suggests that A is larger B. "A subsumes B". "A is more general than B". Liskov Substitution Principle -- "can use B where an A is required".

So variables substitution in the object is strange.

Is there the inverse relationship "A refines B"?

Some context: we were initially planning to have N3 builtins that simply work in both directions, depending on whether the subject or object is concrete. For instance, 1.5708 math:degrees ?x gives the degrees of 1.5708 radians, whereas ?x math:degrees 90 gives the radians of 90 degrees.

In this "philosophy", if case of log:includes, if A includes B someone should simply read this as B refines A too, instead of having an explicit inverse predicate. But recently we've been talking about explicitly including inverse predicates just for ease of use.

[josd]

Thanks William for collecting log:includes and log:notIncludes tests in includes1.n3 https://github.com/w3c/N3/blob/master/tests/N3Tests/log/includes1.n3 and here I agree with the conclusions and eye as well:

$ eye --quiet --nope https://w3c.github.io/N3/tests/N3Tests/log/includes1.n3 --pass 2> /dev/null PREFIX log: http://www.w3.org/2000/10/swap/log# PREFIX : https://w3c.github.io/N3/tests/N3Tests/log/includes1.n3#

:test1 a :SUCCESS. :test2 a :SUCCESS. :test3i a :SUCCESS. :test4 a :SUCCESS. :test6 a :SUCCESS. :test7i a :SUCCESS. :test8 a :SUCCESS. :test9 a :SUCCESS. :test10 a :SUCCESS. :test11i a :SUCCESS.

Strangely enough I can't get anything out with cwm at this point:

$ cwm https://w3c.github.io/N3/tests/N3Tests/log/includes1.n3 --think --data

Processed by Id

    #    using base

https://w3c.github.io/N3/tests/N3Tests/log/includes1.n3

and as far as I can see it is because cwm has a different scope for quickvars.

Jos

-- https://josd.github.io/ http://josd.github.io/

On Wed, Mar 10, 2021 at 1:54 PM William Van Woensel < notifications@github.com> wrote:

I still find it awkward that :will :hasName "will" includes ?x :hasName "will"

I think it is because you interpret it as {:will :hasName "will"} log:includes {@forAll :x. :x :hasName "will"} or maybe as @forAll :x. {:will :hasName "will"} log:includes {:x :hasName "will"}. Both of these formulae are indeed false.

But in your rule, ?x is quantified to an even higher layer. Let me rephrase your rule in english and in a more imperative way:

• for all ?x

• check if { :will :hasName "will" } includes { ?x :hasName "will" }

• if so, generate the triple :rule1 :out :success

There are many values of ?x for which the rule does not fire. But there is one (:will) for which it does. That's enough for the "success" triple to be generated.

Aha .. thanks for clarifying. I didn't see it this way at all - I saw it as a type of containment check where some terms simply may be more general (and not in the context of a rule). Indeed, as @doerthe https://github.com/doerthe is known to say, it all depends on the quantification :-)

I collected some tests here: includes1.n3 https://github.com/w3c/N3/blob/master/tests/N3Tests/log/includes1.n3

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/w3c/N3/issues/71#issuecomment-795372435, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABPHJBXNKWQJK6FLOJG2D3TC5MWFANCNFSM4YVFHLRQ .