Unexpected behaviour (dummy list) due to double `log:onNegativeSurface`

[renyuneyun]

Hi. I'm encoding my formulas using RDF Surfaces, with a mixture of a few N3 logic (particular log:collectAllIn for temporary closed-world assumption). Most of them are working fine. However, today I face some unexpected behaviour of RDF Surfaces, due to nesting two log:onNegativeSurface. The minimal reproduction example is:

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <http://example.org/ns#>.

:a a :A.

(_:x) log:onNegativeSurface {
    _:x a :A.

    () log:onNegativeSurface {  # Remove these two negative surfaces to make it normal.
        () log:onNegativeSurface {
            (_:scope) log:onPositiveSurface {
                (
                    ()
                    {
                        :x :y :z.  # Some false statements
                    }
                    ()
                ) log:collectAllIn _:scope.
            }.
        }.
    }.

    () log:onNegativeSurface {
        _:x :like :b.
    }.
}.

(_:x _:vs) log:onNegativeSurface {
    ( _:scope) log:onPositiveSurface {
        (
            ?v
            {
                _:x :like ?v.
            }
            _:vs
        ) log:collectAllIn _:scope.
    }.

    () log:onNegativeSurface {
        _:m a :Result;
            :with _:vs.
    }.
}.

(_:s _:p _:o) log:onQuerySurface{
    _:s a :Result.
    _:s _:p _:o.
}.

I presume the logic (apart from the query) is equivalent to:

\forall x. (A(x) /\ ~false --> like(x, b))
\exists m. (\forall x, vs. (\forall v. (IN(v, vs) <--> like(x, v))) --> Result(m) /\ with(m, vs)))

(where ~ indicates NOT; IN is specially for testing list member. List member part may not be entirely correct; it's the N3 built-in at least.)

And the expected result is:

_:sk_75 a :Result.
_:sk_75 :with (:b).

However, the real result after running the reasoner is:

_:sk_72 a :Result.
_:sk_72 :with ().
_:sk_75 a :Result.
_:sk_75 :with (:b).

Surprisingly, if removing the nested double negation (log:onNegativeSurface at line 9 and 10), it gives expected result. But I need these nested log:onNegativeSurface to express logical disjunction (omitted in this example for simplicity).

Is this a bug or a feature? If it's a feature, how should this be understood?

[josd]

This is related with the mutual dependency between your 2 log:collectAllIn triples and can be resolved by using an explicit recursion level like defined in https://github.com/eyereasoner/eye/blob/master/log-rules.n3#L65 So the following

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix : <http://example.org/ns#>.

:a a :A.

(_:x) log:onNegativeSurface {
    _:x a :A.

    () log:onNegativeSurface {  # Remove these two negative surfaces to make it normal.
        () log:onNegativeSurface {
            (_:context) log:onPositiveSurface {
                                (
                                        ()
                                        {
                                                :x :y :z.  # Some false statements
                                        }
                                        ()
                                ) log:collectAllIn (_:context 1).
                        }.
        }.
    }.

    () log:onNegativeSurface {
        _:x :like :b.
    }.
}.

(_:x _:vs) log:onNegativeSurface {
        (_:context _:v) log:onPositiveSurface {
                (
                        _:v
                        {
                _:x :like _:v.
                        }
                        _:vs
                ) log:collectAllIn (_:context 2).
        }.

        () log:onNegativeSurface {
        _:m a :Result;
            :with _:vs.
        }.
}.

(_:s _:p _:o) log:onQuerySurface{
    _:s a :Result.
    _:s _:p _:o.
}.

should give

@prefix : <http://example.org/ns#>.

_:sk_72 a :Result.
_:sk_72 :with (:b).

[renyuneyun]

Thanks for the timely response! That does solve the issue.

I have read that link you posted, but am still in confusion. I actually have several questions for that after reading it and the example you gave. The most prominent one is: what does recursion and level of recursion mean here? Sure, there is a dependency of derivation, as you pointed out; but there is no derivation (assuming it's similar to function call in programming) depending on self, so it's confusing... In other words, there is no cyclic dependency, so I don't see why there is recursion.

More practically, in my case, is it the same as the topological order of the "dependency" of these conclusions (e.g. _:x :like :b is conclusion at level 1, and _:m a :Result is at level 2)? What if another rule also depends on _:x :like :b, but not _:m a :Result? Will it be level 2 or level 3 for uniqueness?

In my rules, there are several places where log:collectAllIn is used. So knowing the reason is necessary.

Please forgive my naiveness about N3 reasoning internals. Is there a document I can read?

[josd]

This is still under discussion in the W3C N3 CG and one day it will be explained in https://w3c.github.io/N3/reports/20230703/builtins.html#log:collectAllIn 👍

Think about recursion level as a prioritity: in your corrected case all rules (obtained from surfaces) will run till no more results are added to the deductive closure, then all rules including those with priority 1 will run till no more results are added to the deductive closure, then all rules including those with priority 1 and 2 will run till no more results are added to the deductive closure then all rules including those with priority 1, 2 and 3 will run till no more results are added to the deductive closure, etc ...

When the priorities are not resolved eye --warn will show the conflicting models.

[renyuneyun]

Thanks for the explanation! So the default recursion level (for log:collectAllIn _:scope) is... 0?

Anyway, I have done some further testing and things are all working now, except for performance that I'll try to solve. Thanks!

[josd]

So the default recursion level (for log:collectAllIn _:scope) is... 0?

The default recursion level is 1, so the __within_scope__ predicates (like log:collectAllIn) will only start to run after the initial saturated deductive closure.

[josd]

except for performance

Sometimes a small reordering of triples in the body of backward rules can give big speed improvements, like for instance in https://github.com/william-vw/pqn/commit/bf748cea56fa226a04178fb402fa370bc61ab688