Allow SPARQL-style variables to be quantified.

[pchampin]

In the current EBNF grammar, quantifiers @forAll and @forSome expect IRIs, and only IRIs.

I must says I was always confused by the fact that N3 uses IRIs as variables, while IRIs anywhere else are more akin to "constants" (at least intuitively -- I know that their formal semantics is not that of proper constants). But that ship has sailed, and I am not suggesting to change that.

However, I would really like to be also allowed to write
@forAll ?x. { @forSome ?y. ?x :likes ?y } => { ?x a :Liker }.
rather than
@forAll :x. { @forSome :y. :x :likes :y } => { :x a :Liker }.

This would not introduce backward inconsistency, because currently this syntax is simply not allowed.

I know that SPARQL-style variables already have a semantics of their own. But so do IRIs, and we are happy with the fact that quantifiers are altering this default semantics for IRIs. So I do not think that this alteration of SPARQL-style variables' default semantics would make quantifiers more confusing than they already are.

I even expect that, in the long run, quantifying IRIs would become an obsolete practice (even if still allowed, for backward compatibility) in favour of always using variables with quantifiers. But that's just my opinion ;-)

[gkellogg]

This should just have the affect of introducing the top scope for the variable. In your cases, the affect would be the same without using @forAll at all, but if the variables were used deeper within a formula hierarchy, it could create different variables. Using @forAll at the top-level would be a way to join all those separate uses to be a single variable.

[william-vw]

@pchampin I think it's certainly worth thinking about! Personally I think that using a separate syntax for variables would make sense (we've talked about this often).

But, just playing devil's advocate here, allowing multiple ways of doing the same thing may cast confusion (what's the difference with using IRIs vs. quick-vars? would using IRIs vs. quick-vars be equivalent?). Or, confusion with the "regular" use of quick-vars. One could possibly issue a info/warning when a non-explicitly quantified variable occurs - along the lines of "this will be univ quantified on top level".

[doerthe]

First of all: as William already pointed out, you are not the only one who thinks that it is confusing to use URIs as variables, see for example the discussion here: #7 or also the question whether we need free variables #19

Having said that, I think that using quantified universals would be even more confusing. Suppose you have a very long document and somewhere in the beginning of that document you write

@forSome ?x. ?x :likes :coffee. 

Now, at some point in time you decide that you want to support subclass reasoning and add a simple rule at the end of your document stating:

{?x rdfs:subClassOf ?y. ?z a ?x} => {?z a ?y}.

This rule will never fire because opposed to its intended meaning, the variable ?x will not be universally quantified, it will be existentially quantified and scoped under the existential quantifier you added at the beginning.

In my opinion such situations can easily happen because people tend to name their variables ?x, ?y, ?z.

Maybe there is another solution what we could do here? I also see the problem and agree with you. I thought a variable name space could help, but maybe you have a better idea?

[pchampin]

@william-vw I would expect @forAll :x and forAll ?x to be absolutely equivalent. Yes, having two ways of doing the same thing may bring confusion, but it could easily (?) be explained as "one of them is for backward compatibility, the other one is the preferred way".

@doerthe your "very long document" argument also applies to IRIs. Generally speaking, someone could quantify an IRI somehwhere in the document, then use it as a "regular" IRI further down the document... The only reason why this would be less of a problem with IRIs than with variables is that:

In my opinion such situations can easily happen because people tend to name their variables ?x, ?y, ?z.

... so you seem to assume that "variable IRIs" will look more like :x or :y, while "regular IRIs" will look more like :alice or :Person. I tend to agree, but still, that kind of "protection" is brittle.

Having a separate namespace for variables sounds like a cure which is worse than the disease... Either one would use the empty prefix for that namespace, then all local IRIs would have to be prefixed, which is not nice:
@forAll :x { :x a my:Person } => { :x a my:Human }.
or the empty prefix would kept for IRIs, and variables would have to be prefixed:
@forAll var:x { var:x a :Person } => { var:x a :Human }.
which is ugly.

[doerthe]

I agree that my long document argument goes for both, uris and universals, the only difference is that I expect people to be more careful with their uris than with their universals, but my expectation might not the best argument

Your second option @forAll var:x { var:x a :Person } => { var:x a :Human }. is actually how I would solve it. That might be ugly, but it is the cleanest solution I have found so far. I agree that it is not optimal. Do you have any other suggestion? Should we use the SPARQL variable notation $x?

[josd]

Well, I am since long very using var: namespace prefix and being ugly, it is quite practical in proofs like e.g.
https://github.com/josd/eye/blob/master/reasoning/socrates/socrates_proof.n3

[pchampin]

@doerthe

Do you have any other suggestion?

My suggestion was to use syntactically different items (i.e. ?x instead of :x) 😛 .

My second choice, if we keep IRIs for quantified variables, would be to keep things as they are. As you pointed out, people usually name their "variable-IRIs" differently from their "constant-IRIs", so an informal namespacing is already in place. Creating a proper "variable namespace" would, in my opinion, create even more confusion.

@josd

it is quite practical in proofs like e.g. https://github.com/josd/eye/blob/master/reasoning/socrates/socrates_proof.n3

What would prevent you to replacevar:x_0, var:x_1 with :x_0, :x_1? Unless I'm missing something, this would work just the same, and the "informal namespacing" I mentioned above ("x_0" and "x_1" clearly are variables, regardless of their prefix) makes it readable enough, IMO.

[josd]

@pchampin

What would prevent you to replacevar:x_0, var:x_1 with :x_0, :x_1? Unless I'm missing something, this would work just the same, and the "informal namespacing" I mentioned above ("x_0" and "x_1" clearly are variables, regardless of their prefix) makes it readable enough, IMO.

When writing N3 manually it is fine but when writing a program that produces N3 such as the above proof it is not practical to hijack the : namespace prefix. Look for instance at another proof like https://github.com/josd/eye/blob/master/reasoning/gedcom/gedcom-proof.n3 and it is not that obvious to use http://www.agfa.com/w3c/euler/gedcom-facts#x_0 instead of http://josd.github.io/var#x_0

[pchampin]

@josd
Ok, got it. Thanks for the explanation.

Just to be clear: I do not propose to forbid the use of a separate namespace for variables...
But I don't think it would be a good idea to force users to use a separate namespace.

[william-vw]

@pchampin

What would prevent you to replacevar:x_0, var:x_1 with :x_0, :x_1? Unless I'm missing something, this would work just the same, and the "informal namespacing" I mentioned above ("x_0" and "x_1" clearly are variables, regardless of their prefix) makes it readable enough, IMO.

When writing N3 manually it is fine but when writing a program that produces N3 such as the above proof it is not practical to hijack the : namespace prefix. Look for instance at another proof like https://github.com/josd/eye/blob/master/reasoning/gedcom/gedcom-proof.n3 and it is not that obvious to use http://www.agfa.com/w3c/euler/gedcom-facts#x_0 instead of http://josd.github.io/var#x_0

Perhaps this is an extra argument to have a separate syntax (with syntax, I also mean separate namespace) for variables, i.e., if automatically generated N3 code would look quite confusing without it.

Regrettably, there don't seem to be silver-bullet solutions. I think @doerthe raises a good point, i.e., when allowing ?x to be explicitly quantified, variable names can be unexpectedly "tainted" by earlier quantifiers . E.g., using @forSome ?x . early on would interfere with { ?x :p :o } => { ?x :y :z } as it means that ?x would no longer be universally quantified, as per the default semantics. I agree that this could be very unexpected behavior.

Using a var prefix (with or without requiring a var namespace declaration each time) doesn't have that specific problem, i.e., @forSome var:x . early on wouldn't interfere with { ?x :p :o } => { ?x :y :z }. Well, I suppose that depends on what ?x is equivalent to - @forAll :x , @forAll var:x , or something else? (This is actually a question I've been meaning to ask!)

[william-vw]

I believe this point has become moot, since we made it easier on ourselves and currently not supporting explicit quantification :-)