Universally quantified vars: inconsistencies and/or unexpected results

[MichelSc]

I use eye version EYE v11.19.3 (2025-05-18) SWI-Prolog version 8.4.2.

I consider graph 1:

:Test1
    rdf:type :Test;
    :testVar ?a ;
    :testFormula  { ?a rdf:type :A.}.

I observe

• 1: ?a of line 3 is different from ?a of line 4: Unexpected
• 2: ?a of line 3 is of type log:ForAll: OK
• 3: ?a of line 4 is of type log:ForAll: OK

I consider now graph 2:

true =>{
:Test1
    rdf:type :Test;
    :testVar ?a ;
    :testFormula  { ?a rdf:type :A.}.
}.

I observe

• 4: ?a of line 4 is the same ?a of line 5: OK
• 5: ?a of type log:Other: Unexpected

Q1: why is the result different from graph 1? The graph is just inferred instead of being stated!

I consider now graph 3:

:Test1
    rdf:type :Test;
    :testVarAndFormula ( ?a { ?a rdf:type :A} ).

I observe

• 6: both ?a are the same term: OK
• 7: ?a is of type log:ForAll: OK

Q2: why is this different from graph 1? I just put the var and the formula in a list!

I finally consider graph 4:

:Test1
    rdf:type :Test;
    :testVarAndFormula {
        :thing :testVar ?a.
        :thing :testFormula { ?a rdf:type :A}
    }.

I observe

• 8: both ?a are the same term: OK
• 9: ?a is of type log:ForAll: OK

In summary:

• when my var and my formula are terms in the stated graph (graph 1), the var is not in the scope of the formula
• when my var and my formula are terms in the inferred graph (graph 2), the var is no longer a var
• when my var and my formula are in a list (graph 3), it works as expected
• when my var and my formula are in a subgraph (graph 4), it works as expected

Are observations 1 and 5 expected? In my opinion, we should have consistency between graphs 1 to 4.

[josd]

Yes, this is how eye is designed and implemented:
For 1: the scope of a quickvar is the statement level.
For 5: the rule is seen as an existential rule and will create a witness for ?a.
Please do the same excercise for Cwm and you will see another design and raise the issues at https://github.com/w3c/N3/issues
Those issues must first be resolved at the spec level and then eye can be made spec compliant.

[MichelSc]

Thank you for the replies.

I will have a look at Cwm.

Is it documented somewhere, what is the design and the semantics implemented by eye? How can I make the difference between bug and feature? What is the rationale of the choices implemented?

And I have one more case to submit.

This was graph 3 that behaves as expected (?a is existential, both ?a refer to the same var):

:Test1
    rdf:type :Test;
    :testVarAndFormula ( ?a { ?a rdf:type :A} ).

Consider now graph 5 that is the same, except that the list is expressed as rdf:

:Test2
    rdf:type :Test;
    :testVarAndFormula [
        rdf:first ?a;
        rdf:rest [
            rdf:first { ?a rdf:type :A } ;
            rdf:rest rdf:nil
        ]
    ].

I observe: both ?a refer to different vars. This is not expected, not consistent with graph 3, and in my understanding NOK.

How this behavior can be explained?