Re: Semi-explicit quantification

Dear Pierre Antoine,

Before I make up my mind here, I have some questions to better understand your proposal.

Am 26.08.2021 um 11:23 schrieb Pierre-Antoine Champin <pierre-antoine@w3.org<mailto:pierre-antoine@w3.org>>:

Hi all,

Following a number discussions (during calls, on github, and in private email conversations), here's a new crazy idea for revisiting quantification in N3. This is a variant of the "different kinds of curly brackets" idea that I mused with previously. The rationale is to (a) restrict the expressiveness of the language to avoid falling into full FOL, while (b) keeping it possible to use log:semantics (see issue #90) and similar constructs. Disclaimer: whether (a) is actually achieved by this proposal remains to be formally proven.


The proposal:

* universal variables are always represented by quick-variables (e.g. ?x); existential variables are always represented by blank nodes (e.g. _:b or [ ... ])

* @forAll and @forSome are not used anymore

* define two new keywords @QAE and @QE, that can be used in any formula, without any argument, directly followed by a period ("."). A good practice is to put them before any triple in the formula, but their position is actually irrelevant. E.g.

    :alice :believes { @QE. [] a :Unicorn. [] a :Dragon }.
    :doc1 :contains { @QAE. { ?x a :Unicorn } } => { ?x a :FantasticBeast } }.
Here, there is something wrong with the brackets. Do you mean

(1)  :doc1 :contains { { @QAE. { ?x a :Unicorn } } => { ?x a :FantasticBeast } }.

Or

(2) :doc1 :contains { @QAE. { ?x a :Unicorn } => { ?x a :FantasticBeast } }.

This leads to a question: where does the quantification indicated by your 2 new quantifiers stop? Always with the next closing bracket? So, would the universal in the conclusion from option (1) then be quantified on top level od would you expect that it unifies with the locally quantified variable in the premise?


* whenever a blank node appears, it is quantified in the inner-most enclosing formula that contains @QE or @QAE

* whenever a quick variable appears, it is quantified in the inner-most enclosing formula that contains @QAE

I think you have a reason to assume that local universal quantification only occurs in combination with local existential quantification. Could you explain it? Does it come from the examples you considered so far?

I think especially in the case of universal quantification you often actually wish to have some mixture of local and global universals.
My use-case below is a little bit artificial (I will simplify in the next mail when I had time to think about it), but let’s consider the example below:

We have some information about interesting classes and a graph containing rules and we wish to only get all rules about interesting classes.

:Dog a :interestingClass.
:Cat a :interestingClass.

{@QAE {?x a :Dog}=>{?x a :Animal}.  {?x a :Cat}=>{?x a :Animal}.  {?x a :Spider}=>{?x a :Animal}.} :my :graph.

I wrote the following rule for that:

{?x a :interestingClass. ?y :my :graph. ?y log:includes {{?z a ?x}=>?b} .}=>{{{?z a ?x}=>?b} a :InterestingRule}.

But now we have a problem with the universal variable ?z. Normally, that variable should be local, but if I put a local universal  quantifier in front of it, I will also make the ?x local and my rule would not fire anymore. Another problem is to get that locally scoped universal into the consequence of my rule, but here I am not sure whether your proposal allows that or not.


* @QAE is implicitly contained in the root formula of any N3 document

* @QE is implicitly contained in the formulae on either side of '=>' and '<='

The last bullet is optional -- I think it would make writing rules easier, but I know that Doerthe (at least) has reservations about it... Note that I propose to make it an effect of the '=>' and '<=' keywords, so entirely linked to the *surface* syntax.

So that last two bullets mean that default quantification for universals is on top level and default quantification for existentials depend on their position, that is if they do not occur in a rule, it is top level, if it is in a rule, it is the rule’s body or head, right? Lately, I was actually leaning towards accepting your initial proposal since I understood from the "Buckingham-example“ that the consequences of always assuming local blank node scoping leads to a reasoning behavior which is counter-intuitive to many users.



Unifying two formulae would require that their "quantification level" match, so the following would not match:

    { @QE. [] a :Unicorn. [] a :Dragon } log:includes { ?x a :Unicorn }.
    { @QE. [] a :Unicorn. [] a :Dragon } log:includes { _:u a :Unicorn }.

but the following would

    { @QE. [] a :Unicorn. [] a :Dragon } log:includes { @QE. _:u a :Unicorn }.


  best


<OpenPGP_0x9D1EDAEEEF98D438.asc>


As a very last question which would help us to better understand your proposal, I want to try to express our Buckingham Palace example with it, maybe you could correct my attempt to explain us how the quantification would work?

So, we had
{:will :lives _:b0. _:b0 :place :buckinham_palace. _:b0 :number 12} a :Lie. {{?x :lives ?y. ?y :place :buckinham_palace. ?y :number 12} a :Lie} => {?y a :IncorrectPlace}. If I now want the behavoir we discussed, i.e. I want _:b0 a :IncorrectPlace. and I assume local scoping for inside the graph (to make it complicated), I would have to write: {@QE. :will :lives _:b0. _:b0 :place :buckinham_palace. _:b0 :number 12} a :Lie. {{@QE. ?x :lives _:y. _:y :place :buckinham_palace. _:y :number 12} a :Lie} => {_:z a :IncorrectPlace}.  In that case I would be able to get a new blank note, but no blank note which corresponds to the one in the premise, right?







 From what I see so far, I think your local scoping goes into a nice direction, but we will need some more mails to sort it out. I see more problems for universals than for existantials mainly because universals are heavily used in rules and I think that it is rather unlikely that we only have local universals. It could help with the results of log:semantics though…


So, I am looking forward to your answer to my „writing while thinking“-mail.

Kind regards,
Dörthe