Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Explicit quantification #6

Closed
doerthe opened this issue Jan 14, 2019 · 26 comments
Closed

Explicit quantification #6

doerthe opened this issue Jan 14, 2019 · 26 comments

Comments

@doerthe
Copy link
Contributor

doerthe commented Jan 14, 2019

N3 provides a way to express explicit quantification (by using @forall and @Forsome). An example formula is:

@forall <#h>. @Forsome <#g>. <#g> <#loves> <#h> .

which means in FOL:

∀h: ∃g: loves(h,g)

But the spec also says that "If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials" (see https://www.w3.org/TeamSubmission/n3/#Quantifica). So the formula

@Forsome <#g>. @forall <#h>. <#g> <#loves> <#h> .

also means

∀h: ∃g: loves(h,g)

I at least think that this is counter intuitive (but maybe there are good reasons to do it that way?).

@william-vw
Copy link
Contributor

william-vw commented Jan 25, 2019

I'd say that such a default interpretation is problematic since it rules out expressions/interpretations such as e.g., discussed here (yes, shamelessly plugging my issue here .. apologies). I.e., in this example: for some resource (exist), when all resources that are linked to it (univ) adhere to a particular condition, then an inference could be made. Inverting the existential and universal quantifiers in this expression would change its meaning entirely (i.e., for all resources, there exists a resource adhering to some condition).

In general I'd say that inverting the quantifier positions changes the meaning of the expression drastically. I.e., according to the predicate-logic quantification, @forSome <#g>. @forAll <#h>. <#h> <#loves> <#g> . would state that for some g, all h's love g ("Everybody loves Raymond"). Whereas the expression @forAll <#h>. @forSome <#g>. <#h> <#loves> <#g> . states that for all h's, there exists a g who is loved by h ("Everybody has somebody they love").

@gkellogg
Copy link
Member

gkellogg commented Jan 25, 2019

Interestingly, given the following input:

:Raymond a :Person .
:Julie a :Person; :loves :Raymond .
:Steve a :Person; :loves :Raymond .
:Nancy a :Person; :loves :Raymond .

@forSome :g .
@forAll :h .
{:g :loves :h} => {:g a :Lover} .

Neither CWM nor EYE produce any results. My implementation produces the following:

:Julie a :Lover, :Person;
  :loves :Raymond .

:Nancy a :Lover, :Person;
  :loves :Raymond .

:Steve a :Lover, :Person;
  :loves :Raymond .

:Raymond a :Person .

But clearly, I'm not handling existential quantification in a consistent way (my implementation uses SPARQL-like BGP where blank nodes are non-distinguished variables that behave the same as distinguished variables, for all practical purposes). CWM generates similar output if both :g and :h are universal quantifiers.

@doerthe
Copy link
Contributor Author

doerthe commented Jan 28, 2019

In this case the reasoner should not derive the triples

:Julie a :Lover.
:Nancy a :Lover.
:Steve a :Lover.

and that is independent of the fact whether or not the reasoner changes the order of the quantifiers. To see that, let's assume, that the reasoner keeps the order of thequantifiers as they are just like in first order logic. Then your formula

@forSome :g .
@forAll :h .
{:g :loves :h} => {:g a :Lover} .

Means:

"There exists some g such that for all h we have if g loves h, then g is a lover."

We do not know which g this "some g" is and we do not have a reason to assume that it could be Julie, Nancy or Steve.

So, Cwm and EYE are right here.

@doerthe
Copy link
Contributor Author

doerthe commented Jan 28, 2019

I'd say that such a default interpretation is problematic since it rules out expressions/interpretations such as e.g., discussed here (yes, shamelessly plugging my issue here .. apologies). I.e., in this example: for some resource (exist), when all resources that are linked to it (univ) adhere to a particular condition, then an inference could be made. Inverting the existential and universal quantifiers in this expression would change its meaning entirely (i.e., for all resources, there exists a resource adhering to some condition).

In general I'd say that inverting the quantifier positions changes the meaning of the expression drastically. I.e., according to the predicate-logic quantification, @forSome <#g>. @forall <#h>. <#g> <#loves> <#h> . would state that for some g, all h's love g ("Everybody loves Raymond"). Whereas the expression @forAll <#h>. @forSome <#g>. <#g> <#loves> <#h> . states that for all h's, there exists a g that loves h ("Everybody has somebody that loves them").

I am glad that you agree with me here, but I still wonder whether there are good reasons to have these inverted quantifiers and I just don't see them?

If we want to keep such a thing (but I think we both don't?), I would prefer to make sure that quantification always needs to be stated at the beginning of a formula (ie in the beginning of the document and then in the beginning of every {}-clause) and that there we need to have a fixed order of first universal then existential quantification.

Note that by auxiliary (and rather ugly) constructs you can still express what you wanted above:

@forSome <#g>. {@forall <#h>. <#g> <#loves> <#h> } a log:Truth.

@william-vw
Copy link
Contributor

william-vw commented Jan 28, 2019

Yes, I don't see a purpose for it either really. But I do wonder what you mean by:

"There exists some g such that for all h we have if g loves h, then g is a lover."

We do not know which g this "some g" is and we do not have a reason to assume that it could be Julie, Nancy or Steve.

This is confusing to me - as long as Julie, Nancy or Steve adhere to the conditions in the antecedent then they could certainly act as g, no?

Rather, I'd say the reason that this formula should not return anything since there does not exist some g that loves all h in the domain of discourse. However, in case:

:Raymond a :Person .
:Steve a :Person; :loves :Raymond .
:Steve a :Person; :loves :Steve.

Since Steve loves all people in the domain, I think it should be returned by the formula. Of course, this is under a closed world assumption :-p

Regarding:

I would prefer to make sure that quantification always needs to be stated at the beginning of a formula (ie in the beginning of the document and then in the beginning of every {}-clause) and that there we need to have a fixed order of first universal then existential quantification.

I agree with the former, but I'm unsure why you'd want to enforce a fixed order of quantifiers - seeing how we've established that it disallows certain expressions.

@william-vw
Copy link
Contributor

william-vw commented Jan 28, 2019

I feel that there's some confusion about universal vs. existential quantification (at least to me after reading some of the posts). For instance:

@forAll :x <condition> => <conclusion>

Afaik, this means that only if <condition> is met by all members of the universe of discourse then <conclusion> can be inferred. Hence my plugging of the closed-world assumption, since I think that this kind of quantification can never hold in an open-world.

Now, one can of course define a subset of the universe:

@forAll :x, <definition> : <condition> => <conclusion>

Means that if <condition> is met by the set of all universe members defined by <definition> then <conclusion> can be inferred. Still, in an open world assumption this condition can never hold since one can never be guaranteed that the condition holds for the entire universe - although we could introduce a semantics where this quantification is scoped to the local document.

Note that this means that expressions such as (example taken from here):

@forAll :child, :parent. 
{:child gc:parent :parent. :child :gender :M} log:implies {:parent gc:son :child} . 

Mean that, for all resources in the universe, this resource needs to have as parent all resources in the universe, and also have gender "m" - else the conclusion cannot be drawn. In this case, I believe that the intended meaning - if any child and parent exist where the child is male, the child is the parent's son - can only be obtained by replacing both universals with existentials.

I'd greatly appreciate any feedback on this interpretation since it seems, at least to me, that we're not on the same page.

@gkellogg
Copy link
Member

gkellogg commented Jan 28, 2019

@william-vw said:

I feel that there's some confusion about universal vs. existential quantification

There certainly is for me, at least from a practical perspective rather than a formal definition.

@forAll :x <condition> => <conclusion>

Afaik, this means that only if <condition> is met by all members of the universe of discourse then <conclusion> can be inferred.

I see <condition> as defining the criteria against which :x is bound. If the universe of discourse includes things of different types (say People and Cars) would it be the case that {:x a :Person} would have no solutions, because not all members of the universe are People? I think it's consistent with FOL as well, otherwise in ∀x(Px → Qx), Px would need to be true for the universe for their to be implication for Qx. Clearly, the intention is that Px acts as a condition upon the universe to select all those x for which that condition holds.

I treat this as a Basic Graph Pattern as in SPARQL, where the pattern defined in <condition> is matched against the dataset to come up with solutions for the variables contained within that pattern. So, if the pattern was {:x a :Person}, it would bind :x to the subject of every statement having the type :Person in the dataset. In your example, :child would match all subjects having a gc:parent property and also having a :gender property with the value :M, and :parent all the objects for statements with the subject :child (for all such subjects matching :child) and property gc:parent.

Also note, in SPARQL, that the only difference between variables and blank nodes is that variables can be used in things like filters and projection, where blank nodes just connect parts of the graph pattern with each other (distinguished vs. non-distinguished). It does beg the question on if SPARQL variables should be interpreted as universal or existential quantifiers

Mean that, for all resources in the universe, this resource needs to have as parent all resources in the universe, and also have gender "m" - else the conclusion cannot be drawn.

That's not my interpretation, though. In any case, we can only reason over things in a concrete dataset, not the hypothetical dataset composed of all graphs in the universe.

@william-vw
Copy link
Contributor

william-vw commented Jan 28, 2019

@gkellogg said:

I see as defining the criteria against which :x is bound. If the universe of discourse includes things of different types (say People and Cars) would it be the case that {:x a :Person} would have no solutions, because not all members of the universe are People?

Yes, according to the definition of universal quantification, the formula @ forAll :x a :Person could never hold when not all members of the universe are people. (Not even talking about the fact that any potential inference requires a closed world - more on that below).

As I mentioned, one could define a subset of the universe on which the condition must hold, instead of the entire universe:

@ forAll :x, <definition> : <condition> => <conclusion>

Means that if is met by the set of all universe members defined by then can be inferred.

But even when first limiting the universe to all Persons (abusing notation here), i.e.,

@ forAll [ :x a :Person ] { :x :hasChild :child } => { :x a :Parent }

This would not have your intended meaning - i.e., only when the condition holds for all persons, i.e., they have a child, could it be inferred that all those persons are parents.

I feel that many of the "universal quantification" examples actually mean existential quantification. Indeed, the formula

@forSome :x { :x a :Person . :x :hasChild :child } => { :x a :Parent }

Will likely have the intended meaning - stating that, if any person exists with a child, we can infer that person is a parent.

Else, what would be the difference between universal and existential quantification?

That's not my interpretation, though. In any case, we can only reason over things in a concrete dataset, not the hypothetical dataset composed of all graphs in the universe.

Well, in an open-world assumption, this would exactly be the case - you're working with a hypothetical dataset composed of all graphs in the universe. This assumption has many repercussions on which inferences may be generated by a reasoner (see e.g., here for my thoughts on that).

Hence, a true universal condition can never hold, even when restrained to a subset, since one can never guarantee that all members (everywhere, so not just in your dataset) adhere to the condition. Hence my insistence on having an option for closing the world for N3 formula :-)

@josd
Copy link
Collaborator

josd commented Jan 28, 2019

@doerthe
Copy link
Contributor Author

doerthe commented Jan 30, 2019

Reading all the confusion, it took me some time to decide where (in which issue and answering to which comments) I start.

So, first of all, there is a difference between @forSome (= existential quantifier) and @forAll (= universal quantifier).

###################################################################################################################################
general

@Forsome
The @forSome is used to say that "there exists an instance such that the formula written after it is true." For simple formulas, it is the same to say:

@forSome <#g>. <#g> <#loves> <#you>.

and

[ <#loves> <#you> ] .

Both expressions mean: "There exists someone who loves you." The example is take form the spec.

Note, that you always have to name the concrete variable the quantifier is valid for to be able to identify it in the formula that follows. We quantified over the variable <#g> but not over <#you>

@forall
The @forAll means that what follows is true for all instances. So, indeed, if I say that

@forAll :x. :x a :Person .

You declare that every instance in your whole universe is a :Person.

#########################################################################################################################################
comments on what William said

Yes, according to the definition of universal quantification, the formula @ forAll :x a :Person could never hold when not all members of the universe are people. (Not even talking about the fact that any potential inference requires a closed world - more on that below).

When you write down knowledge, you explain the world to the computer, so that "could never hold" is nothing the computer can decide,
it relies on what you tell it and if you say that really everything is a person, it must believe you (your statement is declarative).

But you are right, typically, we do not use statements like that in an isolated fashion, we use them whith rules. You could for example say:

@forAll :x. {:x a :Person}=>{:x a :Human.}.

Which translates to: "Every instance x which is a person is also a human."

You still explain the world to the computer by telling it that everything in the whole universe which is a person is also a human. So, what you do is not so different from what you said above, only your formula is more specific. You will only get conclusions if something can be identified as a person.

I feel that there's some confusion about universal vs. existential quantification (at least to me after reading some of the posts). For instance:

@forAll :x <condition> => <conclusion>

Afaik, this means that only if <condition> is met by all members of the universe of discourse then <conclusion> can be inferred. Hence my plugging of the closed-world assumption, since I think that this kind of quantification can never hold in an open-world.

Please think of the rule as a rule in the logical sense (I think we had that discussion before on the mailing list, that there are many ways to understand rules).

Here we do not talk of a rule in a imperative programming way which would be something like "if condiction X is met the DO ..." we talk about a logical rule:
"If A is true, then B is true."
This is logically equivalent to:

"Either A is false or B is true."
This is what Jos wanted to say in his comment. If you have a rule like:

{:moon :madeOf :cheese} => {:cows :can :fly}.

which means: "Either the moon is not made out of cheese or cows can fly." That rule is true since we know that the moon is not made out of cheese.

Having the latter in mind, you can give universal statements to the computer. You can say that for every x in the whole universe either x is no person or x is a human. You do that by declaring:

@forAll :x. {:x a :Person}=>{:x a :Human.}.

We do not harm the open world assumption here.

I also want to emphasize that a quantifier always needs to be understood together with its context. It has a position it has variables it quantifies over. Taking your example from above:

@forAll :x <condition> => <conclusion>

If I say for example:

@forAll :x. {:moon :madeOf :Cheese} => {:cows :can :fly}.

The quantifier does not change the truth value of the rule since :x does not occur in your rule.

I use what you said here:

Afaik, this means that only if <condition> is met by all members of the universe of discourse then <conclusion> can be inferred.

to also show how the position of the quantifier matters. What you express here, that something holds if the condition is met by all members of the universe of discourse can also be expressed by using the quantifier inside the antecedent of the rule. For example:

{ @forAll :x. :x a :Person}=> {:that :is :strange}.

Here we actually say "if everything in the domain of discourse is a person, then that is strange". It is rather unlikely that the antecedent of the rule will be met as you already pointed out. Nevertheless, this rule is still correct, if everything would be a person, that would be strange.

Note that this means that expressions such as (example taken from here):

@forAll :child, :parent. 
{:child gc:parent :parent. :child :gender :M} log:implies {:parent gc:son :child} . 

Mean that, for all resources in the universe, this resource needs to have as parent all resources in the universe, and also have gender "m" - else the conclusion cannot be drawn. In this case, I believe that the intended meaning - if any child and parent exist where the child is male, the child is the parent's son - can only be obtained by replacing both universals with existentials.

Here you again do not take the position of the quantifier into account. The rule you describe in words would be:

{@forAll :child, :parent. :child gc:parent :parent. :child :gender :M} log:implies {Concludion} .

What the rule you write above with the quantifier in front means:

"For every resource :child and every resource :parent the fact that :parent is the :parent of :child and the :child is masculine implies that :child is the son of the :parent."

I hope I could clarify your doubts.

###########################################################################################################################################
Comments of what Gregg said

Now, one can of course define a subset of the universe:

@forAll :x, <definition> : <condition> => <conclusion>

Means that if <condition> is met by the set of all universe members defined by <definition> then <conclusion> can be inferred. Still, in an open world assumption this condition can never hold since one can never be guaranteed that the condition holds for the entire universe - although we could introduce a semantics where this quantification is scoped to the local document.

Interestingly, given the following input:

:Raymond a :Person .
:Julie a :Person; :loves :Raymond .
:Steve a :Person; :loves :Raymond .
:Nancy a :Person; :loves :Raymond .

@forSome :g .
@forAll :h .
{:g :loves :h} => {:g a :Lover} .

Neither CWM nor EYE produce any results. My implementation produces the following:

:Julie a :Lover, :Person;
  :loves :Raymond .

:Nancy a :Lover, :Person;
  :loves :Raymond .

:Steve a :Lover, :Person;
  :loves :Raymond .

:Raymond a :Person .

But clearly, I'm not handling existential quantification in a consistent way (my implementation uses SPARQL-like BGP where blank nodes are non-distinguished variables that behave the same as distinguished variables, for all practical purposes). CWM generates similar output if both :g and :h are universal quantifiers.

Reading again what you said, especially the comment about SPARQL, I think you have the same problem here as William: You need to take into account the position of the quantifier.

Note, that @forAll has a different meaning than @forSome. The example you mention here would produce the output you expect if you had:

 @forAll :g .
 @forAll :h .
 {:g :loves :h} => {:g a :Lover} .

Then you get all the lovers.

If you want the rule from above to give you results you need to add a triple for :g here

 @forSome :g .
 @forAll :h .
:g :loves :h.
 {:g :loves :h} => {:g a :Lover} .

This would then result in:

 @forSome :g .
:g a :Lover.

In words: "There exists a lover" or with blank nodes: _:g a :Lover.

I think your confusion come from the fact that in SPARQL, it does not make any difference whether you use a blank node in a query or a query variable (only that you cannot use blank nodes in your results). Think of a query like:

SELECT ?x
WHERE {
    ?x :loves _:y .
}

This query would indeed give you :Julie, :Nancy and :Steve. You can translate this query into a rule. Consider the following rule:

{?x :loves _:y}=>{?x a :Lover}.

With your input triples above, cwm and EYE would both produce the output:

:Julie a :Lover .

:Nancy a :Lover .

:Steve a :Lover .

The reason for that is, that this rule is the same as:

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

Note that the @forSome is inside the rule here. The rule means: "For all x the following is valid: if there exists someone (named y here) who :x loves then :x is a lover."

This is the same as saying:

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

(This is a classical rule of first order logic, if I have time, I will add a link here, but if you want, I can also elaborate on this one later.)

And the latter is now again the same as

 { ?x :loves ?y}=>{?x a :Lover}.

which is why you get your desired conclusion.

@william-vw
Copy link
Contributor

william-vw commented Jan 30, 2019

Thanks very much to @josd and @doerthe for their comments. Indeed, I was rather thinking about the truth value of the premise instead of the implication - i.e., to @doerthe's point I was scoping the quantifier to the premise instead of the entire implication. I haven't yet used a rule language that involved universal quantifiers so apologies for my ignorance.

Just so we're on the same page, by declaring that
@forAll :x. {:x a :Person}=>{:x a :Human.}.`

When the condition holds for any individual, then the consequent should hold for the individual as well - if the condition does not hold, then nothing is said about the consequent. So, to guarantee that this expression is true, a reasoner is safe to infer the consequent for an individual matching the condition?

So what could a reasoner infer if you put a @forSome instead of @forAll?

@doerthe
Copy link
Contributor Author

doerthe commented Jan 31, 2019

Just so we're on the same page, by declaring that
@forAll :x. {:x a :Person}=>{:x a :Human.}.`

When the condition holds for any individual, then the consequent should hold for the individual as well - if the condition does not hold, then nothing is said about the consequent. So, to guarantee that this expression is true, a reasoner is safe to infer the consequent for an individual matching the condition?

yes.

So what could a reasoner infer if you put a @forSome instead of @forAll?

Without further context, the reasoner could not derive anything if you just state

@forSome :x. {:x a :Person}=>{:x a :Human.}.

since you have no further information about your :x.

The existential quantifier could be useful in situations you want to make rules involving blank nodes you mentioned earlier. If you remember your :Raymond example where I just "forgot" Raymond's name, but I still know that there exists this guy everybody loves, then I cannot state that using blank nodes. With the triples

_:y a :person.
{?x a :person} =>{?x :loves _:y}.

Since the scope of the blank node in the consequence of the rule is local, the two _:y's you see above are not the same. Here is makes sense to say instead:

@forSome :y. 
:y a :person.
{?x a :person} =>{?x :loves :y}.

That way we can link all persons to the same blank node when applying the rule.

@william-vw
Copy link
Contributor

william-vw commented Feb 19, 2019

As with #5 (implicit quantification) it seems that the discussion has evolved in such a way that it would be quite daunting for any newcomer to get a good grasp of where we stand.

I think this could be a summary of where we currently stand (feel free to comment):

@doerthe: N3 provides a way to express explicit quantification (by using @ forAll and @ forSome). An example formula is:

@forAll <#h>. @forSome <#g>. <#g> <#loves> <#h> .

which means in FOL:

∀h: ∃g: loves(h,g)

But the spec also says that "If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials" (see https://www.w3.org/TeamSubmission/n3/#Quantifica). So the formula

@forSome <#g>. @forAll <#h>. <#g> <#loves> <#h> .

also means

∀h: ∃g: loves(h,g)

This seems counter intuitive, but maybe there are good reasons to do it that way?

@william-vw Inverting the quantifier positions would drastically change the meaning of the expression. I.e., according to the predicate-logic quantification, @forSome :g. @forAll :h. :h :loves :g . would state that for some g, all h's love g ("Everybody loves Raymond"). Whereas the expression @forAll :h . @forSome :g. :h :loves :g . states that for all hs, there exists a g who is loved by h ("Everybody has somebody they love"). Hence, I don't really know a good reason for doing it this way.

There were discussions about positions of quantifiers in implications, the differences between @ forSome and @ forAll (see here), the scoping of quantification in an implication (starting from here) and how an implication will only allow for inferences when its variables are universally quantified (see here).

@mielvds
Copy link

mielvds commented Aug 20, 2019

There were discussions about positions of quantifiers in implications, the differences between @ forSome and @ forAll (see here), the scoping of quantification in an implication (starting from here) and how an implication will only allow for inferences when its variables are universally quantified (see here).

@william-vw can you split these up into three issues and continue there?

@william-vw
Copy link
Contributor

william-vw commented Aug 21, 2019

@mielvds these were mostly clarifications (graciously provided by @doerthe and @josd) pertaining to core logical aspects afaicm and not anything that would be changed in an updated N3 standard

@william-vw
Copy link
Contributor

william-vw commented Aug 6, 2020

Resurrecting this issue again. I believe @doerthe and @josd talked to the designers of N3 and got some insight into the choice of the following:

If both universal and existential quantification are specified for the same formula, then the scope of the universal quantification is outside the scope of the existentials

Perhaps @doerthe or @josd can explain it here (in case I'd get anything wrong :-) . I don't think we've landed on a concrete decision here.

@doerthe
Copy link
Contributor Author

doerthe commented Aug 10, 2020

You remember correctly that we talked to Tim Berners-Lee about that issue and he explained me that the main reason for the choice of putting universal quantification first was simply consistency, he wanted to be in-line with the implicit quantification.

In my opinion it would be best to simply take the order of quantifiers into account but I remember that we did not reach full agreement here. As far as I remember the main question left was whether a variable is quantified when it occurs before a quantification like for example in

:x :p :o. @forAll :x. :x :a :b.

The problem does not occur if we have a dedicated variable name space or we we only allow quantifiers at the beginning of a (sub-)formula.

@domel
Copy link
Collaborator

domel commented Aug 11, 2020

Morover, if you analyze other keywords like @prefix or @base you will see that the N3 parsers and serializers are one-pass. I think that this rule should apply to @forAll and @forSomeas as well.

@pchampin
Copy link
Contributor

pchampin commented Aug 11, 2020

I also think that taking into account the position and order of @forAll and @forSome would make things easier and more intuitive (after all, the position of @prefix and @base do matter).

For the same reason (homogeneity with @prefix and @base), I don't think it would be wise to forbid @forAll and @forSome to appear anywhere in a formula, but at least the parsers could issue an error (or maybe just a warning) if they are quantifying a name that was used before in that formula.

So
:s :p :o. @forAll :s. { :s a :Person } => { :s a :Human } would be disallowed (or at least discouraged), but
:s :p :o. @forAll :x. { :x a :Person } => { :x a :Human } would be fine.

@william-vw
Copy link
Contributor

william-vw commented Aug 12, 2020

For the same reason (homogeneity with @prefix and @base), I don't think it would be wise to forbid @forAll and @forSome to appear anywhere in a formula, but at least the parsers could issue an error (or maybe just a warning) if they are quantifying a name that was used before in that formula.

This requires you, during a single pass, to perform an index lookup to check whether a quantified IRI occurred sans quantifier before (which has performance implications). (This is actually what Jena+N3 does currently by checking a limited IRI cache, but I never saw that as a permanent solution.)

@josd
Copy link
Collaborator

josd commented Nov 30, 2020

PROPOSED: leave out explicit quantification for the first release of N3

@gkellogg
Copy link
Member

gkellogg commented Nov 30, 2020

@mielvds
Copy link

mielvds commented Jan 5, 2021

Scope question about the directives @forall and @forsome: shouldn't these be always be made explicit in the syntax to avoid issues?

What I mean is something like:

@forall :s {
    { :s a :Person } => { :s a :Human }
} .

@forall :s;  @forSome :y {
    { :s a :Person } => { :s a :Human }
  
    :y a :person.
    {?x a :person} =>{?x :loves :y}.
} .

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

@pchampin
Copy link
Contributor

pchampin commented Jan 5, 2021

@mielvds on the contrary, the current proposal is to ban @forall and @forsome, and keep only implicit quantification. More precisely, blank nodes (_:x) are existentially quantified in the scope of the "deepest" pair of curly brackets containing them, and quickvars (?x) are universally quantified in the scope of the whole N3 document containing them.

Dealing with all the possible subtleties that explicit quantification allows was deemed overly complicated, while implicit quantification seems to address most practical use-cases.

@mielvds
Copy link

mielvds commented Jan 5, 2021

oh, missed that. Nevermind then! I'm all for simplicity

@william-vw
Copy link
Contributor

william-vw commented Feb 25, 2021

Same here - I believe this has become a moot point.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

7 participants