No distinction between variables and constants:

[doerthe]

Related to #6 , it can be a problem that variables and constants are not clearly distinguished. Look for example at the first occurence of :h in this formula:

@forSome :g. :g :p :h.  @forAll :h. :g :loves :h .

Given the reversal of quantifiers when interpreting it (∀h: ∃g: ...) it is not clear to me whether this :h is a universally quantified variable or a constant.

[gkellogg]

In my view, and the only sane way to process, IMO, is that scoping is also effectively lexical, with constants used before they are asserted in @forAll/@forSome remain constant. It's only when the declaration is in scope, both lexically and based on formula scope that it is clear.

I think we should make this clear.

[doerthe]

If we keep the behaviour of quantifiers (ie @forSome :g @forAll :h -> ∀h: ∃g:) your suggestion would be a good way to fix my problem here. I just wonder: if we give importance to the lexical order, why do we then at the same time have a scoping mechanism which doesn't take that order into account? I always supposed that the unusual scoping of N3 was to make sure that the exact position of a quantifier doesn't matter such as the order of triples shouldn't matter. How do you see that?

If we want to make sure that the position of the quantifier doesn't matter we could alternatively reserve a name space for variables, In that case it would be clear that the :h is a variable and it would not matter where its quantifier is located.

[gkellogg]

See my comment in #5 (comment).

The ordering of triples shouldn't matter, but for example, if you had @prefix foo: <http://foo.example.org> . followed by statements using foo, then redefined the foo prefix as @prefix foo: <http://bar.example.org> ., the lexical order certainly makes a difference to the parser, even if the order of the resulting statements doesn't matter. The same logic could be applied to variable definitions.

[doerthe]

I agree with you and would follow your argumentation if we hadn't what I describe in #6. What is your opinion there? In my opinion quantifiers are somehow like prefix-declarations (and based on your examples I think you share that opinion?) and their order should matter, but then we have the W3C team submission which says that on the same formula the universal quantification always dominates the existential quantification. I think either the order of quantifiers in a file matters or it does not, this statement with universals and existentials seems to me like a weird exception.

PS: I tested your prefix-example on EYE and Cwm and can report that EYE behaves the way you describe it while Cwm gives an error.

[gkellogg]

I confess that I really don't understand the distinction described in #6. I agree that they are similar to prefix definitions, in as much as where the exist in the source matters for how they are interpreted. I think the issues come if the variables have the same names, but I treat them all as being separate variables in any case.

but then we have the W3C team submission which says that on the same formula the universal quantification always dominates the existential quantification.

I don't really understand how this plays out in practice. I'd like to see an example to illustrate the difference in operation, which is independent of naming confusion.

[doerthe]

I hope that the discussion on the other issue already helped. I repeat it here to be in line with the issue, but if you want, I can also come up with another example.

So, take the case of Raymond again, but assume that we do not know his name, we only know that there is a person that every other person loves. I would expect that you could express that as:

@forSome x. 
:x a :Person.
@forAll :y.{:y a :Person.}=>{:y :loves :x.}.

In practice, we could apply the rule to other triples and derive from:

:Julie a :Person .
:Steve a :Person.
:Nancy a :Person.

That
@forSome :x. :Julie :loves :x. :Steve :loves :x. Nancy :loves :x.
Or, using a blank node:
:Julie :loves _:x. :Steve :loves _:x. Nancy :loves _:x.
The important thing here is, that it is always the same person who is loved.

The interpretation of N3 as stated in the w3c team submission now translates the statement above to:

@forAll :y.
@forSome x. 
:x a :Person.
{:y a :Person.}=>{:y :loves :x.}.

This means: "Everyone loves someone." In this interpretation the loved ones can be different. Applied on the triples above (Julies, Steve, Nancy) we would get the result:

@forSome :x.  :Julie :loves :x .
@forSome :x2.  :Steve :loves :x2.
@forSome :x3. :Nancy :loves :x3 .

Or, using blank node notation again:
:Julie :loves _:x. :Steve :loves _:x2. Nancy :loves _:x3.

Note, that here we have different blank nodes as the existential quantifier was dependent of the universal.

[gkellogg]

These examples raise the notion of binding of variables in the outer-most scope (default graph). My interpretation of @forSome x. :x a :Person. would be to bind x to all of Julie, Steve, and Nancy. If it were just one, which one? My understanding of existential quantification, is there is at least one, but may be more than one, so I'd see x => [Julie, Steve, Nancy] as a solution. as x is scoped to the outermost formula, it is in scope fo the implication. The antecedent also binds y to Julie, Steve, and Nancy so the consequent basically says "everybody loves everybody". Of course, CWM doesn't interpret this way.

I think that evaluating your intermediate solution would yield the following:

@forSome :x.
:x a :Person.
:Julie a :Person; :loves :x .
:Steve a :Person; :loves :x.
:Nancy a :Person; :loves :x.

However, this is not in the form of an implication, so doesn't actually add triples to the dataset, it simply creates more bindings.

Because :x can bind to everyone, you'd end up with the same solution. If you replaced :x with _:x, it could be different:

_:x a :Person; :loves _:x .
:Julie a :Person; :loves _:x .
:Steve a :Person; :loves _:x.
:Nancy a :Person; :loves _:x.

It is the same as the previous, if you make the graph lean.

... This means: "Everyone loves someone."

Yes, or "Everyone loves everyone" depending on if existential quantifiers can bind to more than one thing.

Can existential quantifiers bind to more than one node? If there are no bindings, is it bound to a new blank node?

[doerthe]

Note, that there is a difference between @forSome and @forAll.

These examples raise the notion of binding of variables in the outer-most scope (default graph). My interpretation of @forSome x. :x a :Person. would be to bind x to all of Julie, Steve, and Nancy. If it were just one, which one?

This is exactly the point, you do not know which one and you cannot simply bind your x to any possible person. Remember how I constructed the example, I was talking about Raymond and simply "forgot" his name, so I used the existential quantifier. How can you assume that the person whose name I forgot here was Nancy?

Your example is a little bit like when I say:

"There exists a person who speaks Chinese."

and you make from it:

"Ah, I know William and he is a person, so he must speak Chinese."

This is not a valid conclusion. You just know that someone exists. That is all. Not more, but also not less.

My understanding of existential quantification, is there is at least one, but may be more than one, so I'd see x => [Julie, Steve, Nancy] as a solution. as x is scoped to the outermost formula, it is in scope fo the implication. The antecedent also binds y to Julie, Steve, and Nancy so the consequent basically says "everybody loves everybody". Of course, CWM doesn't interpret this way.

This whole reasoning would be true if you had either the formula:

@forAll :y.
@forAll x. 
{:y a :Person. :x a :Person.}=>{:y :loves :x.}.

or

@forAll :y.
{@forSome x.  :y a :Person. :x a :Person.}=>{:y :loves :x.}.

In both cases the rule means that all persons love each other as you state above. But in the example I gave, the position of the @forSome was in fromt of the formula. We just know that there is some person who is loved by everyone.

I think that evaluating your intermediate solution would yield the following:

@forSome :x.
:x a :Person.
:Julie a :Person; :loves :x .
:Steve a :Person; :loves :x.
:Nancy a :Person; :loves :x.

However, this is not in the form of an implication, so doesn't actually add triples to the dataset, it simply creates more bindings.

Because :x can bind to everyone, you'd end up with the same solution. If you replaced :x with _:x, it could be different:

Please note that according to the w3c team submission, the two formulas

_:x a :Person.

and

@forSome :x. :x a :Person.

Have the same meaning. So yes, the below is another way to express the above.

_:x a :Person; :loves _:x .
:Julie a :Person; :loves _:x .
:Steve a :Person; :loves _:x.
:Nancy a :Person; :loves _:x.

It is the same as the previous, if you make the graph lean.

... This means: "Everyone loves someone."

Yes, or "Everyone loves everyone" depending on if existential quantifiers can bind to more than one thing.

It cannot have both meanings at the same time, it is either the first or the second.

[josd]

As discussed in the N3-dev meeting today, it is proposed to use Well-Known IRIs for the names of variables. This is similar to what RDF 1.1 is doing in https://www.w3.org/TR/rdf11-concepts/#section-skolemization but the proposal here is to register (for instance) the name "genid-n3" according to http://www.rfc-editor.org/rfc/rfc5785.html#section-5.1

Here is a concrete example:

PREFIX var: <http://example.com/.well-known/genid-n3/okUV7D18aoxPqAoy9zlZmgAyE4Q#>
@forSome var:y.
:s :p var:y.

When the variable name is not declared via @forAll or @forSome it is a free variable (also called a parameter).
For a concrete example (using the latest EYE) see:

#eye --no-qvars --nope --n3 http://josd.github.io/eye/reasoning/iq/iq.n3 --pass-all

PREFIX var: http://josd.github.io/.well-known/genid-n3/pCGZpyvjRMMypZsUVMeJGBW46yM#
PREFIX : http://example.org/test#

var:e_x_1 :says {var:e_x_2 :knows :Albert}.
:s :p :o.
:s :pp {:s :ppp :ooo}.
{var:sk_1 :knows :Albert} => {var:x_0 :knows :Kurt}.
{:e :p :a} => {:e :q :b}.
{{var:sk_2 :p :a} => {var:sk_2 :q :b}} => {{var:sk_2 :r :c} => {var:sk_2 :s :d}}.
{var:sk_3 :p :o} => {var:sk_3 :pp {var:sk_3 :ppp :ooo}}.
{var:sk_4 :p :o} => {{{var:sk_4 :p2 var:sk_5} => {var:sk_4 :p3 var:sk_5}} => {{var:sk_4 :p4 var:sk_5} => {var:sk_4 :p5 var:sk_5}}}.
{:e :r :c} => {:e :s :d}.
{{:s :p2 var:sk_0} => {:s :p3 var:sk_0}} => {{:s :p4 var:sk_0} => {:s :p5 var:sk_0}}.

[william-vw]

Sorry if this is a silly remark - but I assume that it is the intention that the N3 system would automatically generate the unique variable namespace for each document (e.g., based on the document hash)?

If so, would the developer then only use the "var" prefix and let the N3 system fill in the actual namespace (?)

[josd]

When writing n3 files manually as a developer you have the responsibility to mint your own free variable namespace prefix. Reasoners can also generate quantified/free variables e.g. each reasoning run is minting a unique var: namespace prefix.

[william-vw]

I'm unsure where we've landed on this issue - I think it was tabled at the time and we did not revisit it.

Currently the Jena+N3 system treats variables as originally in N3, I think - i.e., as IRIs that have a prior quantification, and without a separate var namespace. Whenever there is a potential conflict is found (e.g., using an IRI :x first and then "declaring" x a variable using a quantifier; or other scenarios) the system will show an error or warning, depending on the config. The implication being that the system very much disapproves of using IRIs both as constants and variables. The reason for all this is because the printed N3 may have a different meaning. E.g.,

:x a :Person .
@forSome :x . :x :loves :someone .

Can easily be printed as

@forSome :x . :x :loves :someone .
:x a :Person .

Asking developers to use a separate "var" prefix for variables side-steps this issue, but I really dislike having to coin a unique namespace for each N3 graph (and I don't think it's realistic to ask it of developers when manually authoring N3).

[doerthe]

In our last meeting, it was proposed to solve the above issue by using the SPARQL $-notation for variables together with quantifiers. Instead of an IRI such as:

@forSome :x . :x :loves :someone .

We would say

@forSome $x . $x :loves :someone .

In general, we could use the $-notation for free variables. Typically, we would expect these variables to be bound by a quantifier.

The use of IRIs for these cases would be deprecated.

Before we further discuss (and agree) on the way we handle quantifiers (issue #6 ), I would like to reach consensus for this decision, so could everyone please vote below (+1 or thumbs-up if you agree, 0 if neutral (no idea which emoji to use here, sorry) , -1 or thumbs-down if you disagree, for the latter please also state your arguments).

[josd]

This works fine now in EYE but would be in conflict when ($ ... $) sets would be introduced

[william-vw]

I believe this has become a moot point, since the current N3 spec would not support explicit quantification :-)