Re: Blank node quantification

Hi Pierre-Antoine,

Thank you for the nice examples and I collected them in
https://github.com/josd/eye/tree/master/reasoning/bnodes
and tested them with the latest eye
https://github.com/josd/eye/releases/tag/v21.0617.1321
At first sight the --pass-all answers look like what you expect :-)

Jos

-- https://josd.github.io/ <http://josd.github.io/>


On Wed, Jun 16, 2021 at 9:34 PM Pierre-Antoine Champin <
pierre-antoine@w3.org> wrote:

> And here's another example, which helped me put the finger on why I was
> not sure about that solution!
>
> Example 7:
>
>    :a :b :c.
>    { ?x :leadsTo ?y } => { ?x => ?y }.
>    { _:y :b :c } :leadsTo { :d :e :f }.
>
> is equivalent to (using old-style explicit quantifiers)
>
>   :a :b :c.
>    { ?x :leadsTo ?y } => { ?x => ?y }.
>    @forSome v:y { v:y :b :c } :leadsTo { :d :e :f }.
>
> This would then produce
>
>    @forSome v:y { v:y :b :c } => { :d :e :f }.
>
> which can not be serialized exactly without explicit quantification
> (it can be approximated with a witness).
> And this would therefore *not* produce  :d :e :f, which might be
> surprising...
>
> (interestingly, the current version of EYE, does *not* produce :d :e :f
> with this example,
>  while CWM does. EYE does if I replace _:y with ?y)
>
> ---
>
> I am not claiming that this is a problem, but it can be considered
> counter-intuitive at least...
>
> But maybe this is too much of a corner case to be a real problem...
>
>   pa
> On 16/06/2021 12:32, Pierre-Antoine Champin wrote:
>
> Fiddling with yet another example that came to my mind:
>
> Example 6:
>
>   _:u a :Unicorn.
>   _:e a :UnicornEater.
>   { ?x a :Unicorn } => { { [] a :UnicornEater } => { ?x :is :threatened }
> }.
>
> is equivalent to (using old-style explicit quantifiers)
>
>   @forSome v:u, v:e.
>   v:u a :Unicorn.
>   v:e a :UnicornEater.
>   { ?x a :Unicorn } => { { @forSome v:e2. v:e2 a :UnicornEater } => { ?x
> :is :threatened } }.
>
> I would expect it to produce (1)
>
>   { @forSome v:e2. v:e2 a :UnicornEater } => { v:u :is :threatened }. #
> with v:u still quantified by the top @forSome
>
> which in turn would produce (2)
>
>   v:u :is :threatened. # with v:u still quantified by the top @forSome
>
> Note that the rule produced at (1) can not be expressed with the implicit
> quantification scheme that I am proposing (nor is it with the *current*
> implicit quantification scheme, by the way). More precisely, v:u is
> existentially quantified outside the formula that contains it, despite the
> fact that this formula is the object of log:implies.
>
> So in that case, we would still need to skolemize v:u (generate a witness)
> in order to express that rule.
>
>   pa
> On 16/06/2021 09:26, Pierre-Antoine Champin wrote:
>
> 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
>
>
>