Re: Blank node quantification

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

Received on Monday, 21 June 2021 15:51:44 UTC