Re: Blank node quantification

On 2021-06-22 12:50 p.m., Pierre-Antoine Champin wrote:
> (1) is not absolutely correct, although it "works" for simple cases 
> (complex cases being: if you have rules inside rules...) 

Can you give an example of where this does not work?

> (2) As I pointed out at the end of our last call, the question of 
> static vs. dynamic scoping is orthogonal to the question of where we 
> put the implicit quantifiers. Let's rephrase by saying that "the 
> purpose is to place implicit quantifiers in a way that hopefully makes 
> it easier to cleanly implement dynamic scoping".
>
Do you mean static scoping here? ..

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