Blank nodes cause issues inside formulas called with `log:call`

[tpluscode]

Of course I fail to create a minimal repro but I found the problem that sometimes, presumably because I pass graphs around using backward rules, log:includes behaves "differently"

Typically, I should be able to use a blank node to match any node, right?

?response log:includes {
  [] tuner:url.path ?path
} .

However, in some cases this stops working for me because it appears that the blank node is compared a face value (?)

Instead, I had to change there to

?response log:includes {
  ?foo tuner:url.path ?path
} .

Using eye v11.10.0

[tpluscode]

I think this causes one more effect, when I use resource paths with backward rules.

For example, I have this rule:

{
  ?res tuner:body ?body .
} <= {
  ?res log:includes {
    [] a tuner:Response ; tuner:body ?body .
  } .
} .

I should be able to write ?res!tuner:body log:includes {} to inline but in some cases it just doesn't work and I have to write the "full"

?res tuner:body ?body .

?body log:includes {}

I believe this could be related but I cannot yet explain why I observe inconsistent behavior. What I think is happening it that the shorthand is expanded so that ?body is interpreted as a blank node and does not match the ?body used in the backward rule.

Does any of that make sense?

[tpluscode]

Indeed, when I add these line to the rule above, I see this

"res" log:trace ?res.
"body" log:trace ?body.

"res" TRACE _:sk_5
"body" TRACE ?_27608
"INFO" TRACE "Calling GET http://localhost:1429/data/tbbt"
"res" TRACE _:sk_5
"body" TRACE ?_35166
"res" TRACE { ... }
"body" TRACE _:e_243

So it passes the rule twice while waiting for the response and then what? Why in the last line the ?body is bound to a blank node?

[josd]

I spent 1/2 hour trying to construct an example that I can run straight with eye but I failed to discover an issue. Could you please provide concrete files that I can run and say: I get this result but expect that result?

[josd]

So also give the command line that you used.

[tpluscode]

Ah, I finally managed to nail it and reduce the ruleset to provide a meaningful reproduction.

The factor is calling a formula with log:call

Here's Gist with the failing rules: https://gist.github.com/tpluscode/cb4b4563469dd8cc439a6ad3ec172869

[josd]

The issue is that in a graph term (aka formula) an existential is not the same as a universal. ?res!tuner:body string:contains "Example" is interpreted as

?res tuner:body _:b .
_:b string:contains "Example" .

which is totally different from

?res tuner:body ?b .
?b string:contains "Example" .

[tpluscode]

I figured as much. And it means it's by design?

[josd]

_:x blank nodes are existentially quantified variables and ?x quickvars are universally quantified variables. They are logically different, see https://chatgpt.com/share/6800add5-d85c-800b-9c6a-20ceb0f4ce3f

[tpluscode]

Well yes, but is the fact that they are interpreted differently inside a graph term is by N3's design?

Does it effectively mean that I cannot use resource paths in formulas?

[josd]

That is indeed the case for eye. It would be good if you raise this N3 issue at https://github.com/w3c/N3/issues

[josd]

The simplest case I could find is formula.n3

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

:test1 :formula { ?A!:b :d :e }.
:test2 :formula { ?A :b ?C. ?C :d :e }.

{
    ?T :formula ?F.
    ?F log:includes { :a :b :c. :c :d :e }.
} => {
    ?T :is true.
}.

wich gives

$ eye --quiet --nope formula.n3 --pass-only-new
@prefix : <http://example.org/#>.

:test2 :is true.

[josd]

As you can see in https://editor.notation3.org/s/Xz75FQ0O the jen3 reasoner also agrees with eye.