Re: Semi-explicit quantification

On 26/08/2021 14:01, Dörthe Arndt wrote:
> 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 } }.

Sorry about that! I meant (2).

>
> This leads to a question: where does the quantification indicated by 
> your 2 new quantifiers stop? Always with the next closing bracket?
Not sure what you mean by the "next" closing bracket... The idea is that 
quantification scopes the entire formula where it occurs. Assuming that 
@QAE and @QE always occur just after an opening bracket, the 
quantification stops at the corresponding 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?
Actually, I fail to parse option (1) above... In { @QAE. { ?x a :Unicorn 
} }, the inner formula is a term not involved in any triple...
>
>>
>> * 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?

It comes from the current rules of implicit quantification, which could 
be described as is:

* any N3 document implicitly starts with @QAE.

* any quoted formula in an N3 document implicitly starts with @QE.

>
> 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.

Yes, that would be a problem.

But even in the current situation, the only way to solve it is to use 
explicit quantification, right? Actually, your example seems to show 
that "semi-explicit quantification" is actually reducing expressiveness 
compared to explicit quantification, which was one of the design goals. 
So, I would argue that "it's not a bug, it's a feature" ;-)

>
>>
>> * @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?
yes
> 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.
The last bullet is very similar to my initial proposal, with a slight 
difference: in my initial proposal, I suggested to make the scope change 
dependent on the abstract syntax (the use of the log:implies predicate). 
Here I am suggesting to make it dependent on the concrete syntax (the 
use of the => or <= tokens in the predicate position). I think the 2nd 
option is better, but this is really a detail that does not impact the 
rest of the proposal.
>
>>
>>
>> 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?
>
>  
>
>
>
Yes

But you can also solve it the other way around. In the original form, 
the rule would now fire, because _:b0 is globally scoped, so it can be 
matched by ?y .


>
>
> 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…

May be the most useful scenarios, where local universals are required, 
could be solved by introducing appropriate builtins?

   best

>
>
> So, I am looking forward to your answer to my „writing while 
> thinking“-mail.
>
> Kind regards,
> Dörthe
>
>