Existential variable in the rule head and conclusion

[eyusupov]

According to the N3 semantics,

{_:x a :Human} => {_:x a :Mortal}.

becomes ({},{},{<{},{x},{(x,rdf:type,:Human)}>,log:implies,<{},{x},{(x,rdf:type,:Mortal)}>})

So having a graph like

:bill a :Human
{_:x a :Human} => {_:x a :Mortal}.

will lead to a conclusion

[] a :Mortal.

, not

:bill a :Mortal.

1. Can this case be added to the examples?

2. Maybe some clarification can be done in N3 grammar that the blank node with the same identifier inside the graph term is not the same blank node as the one outside.

I think Note that this identifier is only usable within our local N3 Graph can be understood as _:x will be the same in both graph terms (and outside of it, if it was present there).

[eyusupov]

Actually there is an example like that in log-entailment section:

({},{},{((:socrates,rdf:type,:Human),<{},{x},{(x,rdf:type,:Human)}>,log:implies,<{},{x},{(x,rdf:type,:Mortal)}>)})
– in concrete syntax: :socrates a :Human. {_:x a :Human} => {_:x a :Mortal}.
log-entails
({},{x},{(x,rdf:type,:Mortal)})({},{x},{(x,rdf:type,:Mortal)})
– in concrete syntax: _:x a :Mortal. 

But maybe it's worth clarifying that _:x in entailed graph can be different from _x in the graph from which it was entailed from.

[doerthe]

With the local graph, we meant the graph term. But I understand that this is not that clear or it was not when you first read it. I will come back with a proposal...

[eyusupov]

Thank you. Maybe it's worth to explain more explicitly why there is no practical difference between

{_:x a :Human} => {_:x a :Mortal}.

and a

{?a a :Human} => {?b a :Mortal}.

[eyusupov]

Which probably means that we can't say that blank nodes are existential variables and variable terms are universals. It seems that it's more correct to say that unbound nodes (in the rule conclusion) act as existential variables and the bound nodes as universals. However, because of the scoping, the blank nodes in the rule conclusions are always local and cannot be bound, thus always acting as existential variables.

[doerthe]

Blank nodes are really existentially quantified and not unbound. The question is more: where exactly do we put the quantifier? If I take your example from above
{_:x a :Human} => {_:x a :Mortal}.
and try to translate it to FOL (informally, for the sake of this example, using a predicate tr to indicate a triple), we could either do
∃x: (tr(x,a,Human)→tr(x,a,Mortal))
or
(∃x: tr(x,a,Human))→(∃x:tr(x,a,Mortal))
The choice has consequences. If I have for example a triple
:socrates a :Human.or also _:y a :Human.
these triples would become
tr(socrates, a, Human) and ∃y:tr(y,a,Human)
only the second rule would fire on these two triples but not the first and derive in both cases
∃x: tr(x,a,Mortal)
or as a triple
_:x a :Mortal.
In N3 blank nodes are quantified within the graph terms they appear in, that is, the second interpretation is the correct one. This also makes sense in the broader context of the Web where you might want to produce new blank nodes. Note, that this interpretation of the rules is also very close to the theory of existential rules.

[doerthe]

Thank you. Maybe it's worth to explain more explicitly why there is no practical difference between

{_:x a :Human} => {_:x a :Mortal}.

and a

{?a a :Human} => {?b a :Mortal}.

Please note, that the semantics makes a difference between these two, only the implementation in EYE does not and the reason is of rather practical nature: If you allow universal quantification on triple level, you can make statements like
?b a :Mortal.
which is a universal statement about literally everything in your universe. You could derive
rdf:type a Mortal. :Mortal a :Mortal., 1 a :Mortal, 2 a :Mortal, ...
This is difficult to handle for a reasoner and most likely also nothing the user wants. Therefore, EYE converts such universal variables into blank nodes (There are also ways around, but this leads to far...)

[eyusupov]

Thank you. I think these explanations have cleared up the situation mostly for me. I was wondering about the EYE behavior too.

[josd]

Right and the scope of blank nodes has been for a long time a thorn in the eye ;-)
It has been changed quite often from global (as in RDF) to graph term local (as in N3).
In the latest version EYE v10.7.6 (2024-05-16) it is again graph term local

always doing bnode relabeling except when flag --no-bnode-relabeling

So

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

:bill a :Human.
{_:x a :Human} => {_:x a :Mortal}.

will pass as

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

:bill a :Human.
_:sk_0 a :Mortal.

[eyusupov]

Are blank nodes existential though in this sense?

:a :a :b.
:c :a :d.
{ _:x :a _y } => { _:x :a _:y }.

In my understanding, with the existential variables x and y, the inference engine would produce only one triple _:x1 :a _:y1. With the universal variable:

:a :a :b.
:c :a :d.
{ ?x :a ?y } => { _:x :a _:y }.

I'd expect the rule to match two times, and produce another triple (say _:x2 :a _:y2).

Also with the universal vs existential treatment of blank nodes & variables rules like

... => { ?unbound ... ... }

should not produce any triples, which seems to be not the case at the moment.

[eyusupov]

I understand that in the absence of universal variables in the produced triple, the produced triples with blank nodes will be "isomorphic" to one another, so they can be treated as the same object. But that seems like a bit different aspect of the picture for now.

[eyusupov]

Would it also be possible to codify the universal/existential/blank node semantics in the N3 tests? That would also help to elaborate various cases. Unless I'm mistaken, the test can't be specified with the exact graph comparison, but would canonicalization work here?

[eyusupov]

I understand that in the absence of universal variables in the produced triple, the produced triples with blank nodes will be "isomorphic" to one another, so they can be treated as the same object. But that seems like a bit different aspect of the picture for now.

Ok, I think I forgot about Skolemization here, so this treatment of existential variables is indeed close to the theory of existential rules.