Re: Blank node quantification

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