Re: Blank node quantification

Hi Jos, everyone,

If I understood correctly:

(1) all blank nodes within cited formulas, aside from rule premises and 
conclusions, are skolemized, and (2) the purpose for this is to 
implement static scoping, which avoids their "leakage" as existential 
variables beyond the cited formula. Such leakage can be problematic when 
blank nodes are "pulled into" rules (i.e., blank node is unified with a 
rule variable); they'd be considered as rule variables and thus lose 
their role as local identifiers, which is how they are often used in 
practice. Another reason is that it would allow inferring an existence 
claim in the top scope that was previously only in a nested scope 
(personally I don't really think that's an issue, and more like "caveat 
emptor" - it's up to the rule author to attach importance to a nested 
formula).

Is this the case?

I do think this kind of static scoping will match many practical use 
cases (as opposed to "dynamic" scoping, which I now believe is only 
really useful for one particular use case.)

In that interpretation, I think the following should work:

{ {
     :will :hasName "will"

} log:includes {
     _:x :hasName "will"

} } => {
     :test1 a :SUCCESS
} .

(it works in cwm but not eye, as the latter skolemizes the blank node, 
even when directly embedded in the rule premise)

And the following should not, I suppose:

{ :will :hasName "will" } :label "formula1" .
{ _:x :hasName "will" } :label "formula2" .

{ ?f1 :label "formula1" .
   ?f2 :label "formula2" .
   ?f1 log:includes ?f2 } => { :test1 a :SUCCESS } .

(again, works in cwm but not eye)


William


On 2021-06-21 8:25 p.m., Jos De Roo wrote:
> You are right Doerthe and sorry for my failing recollection :-(
>
> Anyhow, as per my action of today's meeting I looked into the consequences
> of static (lexical) scoping of bnodes and changed eye accordingly
> at https://github.com/josd/eye/releases/tag/v21.0621.2307 
> <https://github.com/josd/eye/releases/tag/v21.0621.2307>:
> 1/ 
> https://github.com/josd/eye/blob/master/reasoning/bnodes/example7.n3 
> <https://github.com/josd/eye/blob/master/reasoning/bnodes/example7.n3> now
> produces 
> https://github.com/josd/eye/blob/master/reasoning/bnodes/example7-pass-all.n3 
> <https://github.com/josd/eye/blob/master/reasoning/bnodes/example7-pass-all.n3>
> and so ':d :e :f' is no longer produced.
> 2/ all the other tests at 
> https://github.com/josd/eye/tree/master/reasoning 
> <https://github.com/josd/eye/tree/master/reasoning>
> are still working fine as before.
>
> Jos
>
> -- https://josd.github.io/ <http://josd.github.io/>
>
>
> On Mon, Jun 21, 2021 at 5:52 PM Dörthe Arndt <doerthe.arndt@ugent.be 
> <mailto:doerthe.arndt@ugent.be>> wrote:
>
>     Hi Pierre Antoine,
>
>     I am still reading the comments and thinking about my own opinion
>     here, but I can say that your proposal has been implemented some
>     time ago in EYE (I even have an implementation of my grammar for
>     this case and I formalized it that way). So, if you want to „play“
>     with your idea, I think an EYE version from around 2017 should do
>     what you it (but please double check with Jos).
>
>     Hear you in a few minutes.
>     Dörthe
>
>     > Am 16.06.2021 um 09:26 schrieb Pierre-Antoine Champin
>     <pierre-antoine@w3.org <mailto:pierre-antoine@w3.org>>:
>     >
>     > Hi all,
>     >
>     > here's a crazy idea. I am not even sure I like it myself, but I
>     wanted to ear others' opinion about it.
>     >
>     > During our last call, William made a point, with which I agree
>     (assuming I understood it correctly). To sum it up: people use
>     blank node in data more as "local" identifiers than as proper
>     existential variables. This pleads for quantifying blank nodes at
>     the top level.
>     >
>     > On the other hand, as we also pointed out during the call, blank
>     nodes as used in rule bodies (and rule heads, I believe) need to
>     be quantified locally.
>     >
>     > Hence my crazy idea: why not make the scope of blank node
>     determined by the log:implies (=>) predicate?
>     >
>     > More precisely:
>     >
>     > * a formula that is the subject or object of log:implies defines
>     a new scope for blank nodes
>     >
>     > * any other formula inherits the scope of its immediate parent
>     >
>     > * blank nodes in the top level scope are quantified *before*
>     universals (which is consistent with viewing them as "local
>     constants")
>     >
>     > Below is a long (apologies) list of examples.
>     >
>     > WDYT?
>     >
>     >   pa
>     >
>     >
>     > Examples 1:
>     >
>     >     :alice :belives { [] a :Unicorn }.
>     >     [] a :Person.
>     >
>     > is equivalent to (using old-style explicit quantifiers)
>     >
>     >    @forSome v:u, v:p.
>     >    :alice :belives { v:u a :Unicorn }.
>     >    v:p a :Person.
>     >
>     > ----
>     >
>     > Example 2:
>     >
>     >     { [] a :Unicorn } => { :world a :MagicalPlace }.
>     >
>     > is equivalent to (using old-style explicit quantifiers)
>     >
>     >     { @forSome v:u. v:u a :Unicorn } => { :world a :MagicalPlace }.
>     >
>     > (i.e. no change with today's interpretation)
>     >
>     > ----
>     >
>     > Example 3:
>     >
>     >     { ?x a :Person } => { ?x :mother [] }.
>     >
>     > is equivalent to (using old-style explicit quantifiers)
>     >
>     >     { ?x a :Person } => { @forSome v:m. ?x :mother v:m }.
>     >
>     > (i.e. no change with today's interpretation)
>     >
>     > ----
>     >
>     > Example 4:
>     >
>     >     :alice :belives { [] a :Unicorn }.
>     >     { ?x :believes { [] a :Unicorn } } => { ?x a :GulliblePerson }.
>     >
>     > is equivalent to (using old-style explicit quantifiers)
>     >
>     >     @forSome v:u1.
>     >     :alice :believes { v:u1 a :Unicorn }.
>     >     { @forSome v:u2. ?x :believs { v:u2 a :Unicorn } } => { ?x a
>     :GulliblePerson }.
>     >
>     > which, unless I am mistaken, is also equivalent to
>     >
>     >     @forSome v:u1.
>     >     :alice :believes { v:u1 a :Unicorn }.
>     >     { ?x :believs { ?u2 a :Unicorn } } => { ?x a :GulliblePerson }.
>     >
>     > I would expect this to produce.
>     >
>     >     :alice a :GulliblePerson.
>     >
>     > ----
>     >
>     > Example 5:
>     >
>     >     :alice :belives { [] a :Unicorn }.
>     >     { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.
>     >
>     > is equivalent to (using old-style explicit quantifiers)
>     >
>     >     @forSome v:u1.
>     >     :alice :believes { v:u1 a :Unicorn }.
>     >     { ?x :believes { ?y a :Unicorn } } => { ?x :wishesToRide ?y }.
>     >
>     > I would have no problem with this producing
>     >
>     >     :alice :wishesToRide v:u1.  # where v:u1 is still quantified
>     by the top @forSome
>     >
>     >
>     > <OpenPGP_0x9D1EDAEEEF98D438.asc>
>