Re: Blank node quantification

Hi Pierre-Antoine,

That's an excellent idea!
I had a similar idea i.e. "global scope except rule premise"
but your idea is more perfect :-)

The real benefit is that we can keep blank node identifiers
and don't need Skolem IRIs.

The examples look nice and I will try to make an
experimental implementation for eye in the coming days.

Jos


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


On Wed, Jun 16, 2021 at 9:28 AM Pierre-Antoine Champin <
pierre-antoine@w3.org> 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
>
>
>