Re: Semi-explicit quantification

Pointing to https://en.wikipedia.org/wiki/First-order_logic#Formation_rules
only variables and functions (incl. individual constants) can be used as
terms.
A formula in the first order sense can not be a term.
P => C is a formula meaning 'formula P log:implies formula C'.
Any other use like {triples} :p :o is meaning 'graph literal {triples} has
property :p with value :o'.
So there is a distinction between formulae and graph literals and
I like the hybrid scope for blank nodes in that respect in that it has
global scope for graph literals and local scope for formulas.
This is also what is actually implemented in the latest EYE reasoner.

Jos

-- https://josd.github.io


On Mon, Aug 30, 2021 at 1:03 PM Pierre-Antoine Champin <
pierre-antoine.champin@ercim.eu> wrote:

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