Re: Blank node quantification

Hi William, everyone,

In short, I agree and added your 2 examples to
https://github.com/josd/eye/tree/master/reasoning/bnodes
as example8 and example9.
They now run according to your expectations with the latest
eye https://github.com/josd/eye/releases/tag/v21.0622.1431

Thanks and kind regards,
Jos

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


On Tue, Jun 22, 2021 at 2:59 PM William Van Woensel <
william.vanwoensel@gmail.com> wrote:

> Hi Jos, everyone,
>
> If I understood correctly:
>
> (1) all blank nodes within cited formulas, aside from rule premises and
> conclusions, are skolemized, and (2) the purpose for this is to implement
> static scoping, which avoids their "leakage" as existential variables
> beyond the cited formula. Such leakage can be problematic when blank nodes
> are "pulled into" rules (i.e., blank node is unified with a rule variable);
> they'd be considered as rule variables and thus lose their role as local
> identifiers, which is how they are often used in practice. Another reason
> is that it would allow inferring an existence claim in the top scope that
> was previously only in a nested scope (personally I don't really think
> that's an issue, and more like "caveat emptor" - it's up to the rule author
> to attach importance to a nested formula).
>
> Is this the case?
>
> I do think this kind of static scoping will match many practical use cases
> (as opposed to "dynamic" scoping, which I now believe is only really useful
> for one particular use case.)
>
> In that interpretation, I think the following should work:
>
> { {
>     :will :hasName "will"
>
> } log:includes {
>     _:x :hasName "will"
>
> } } => {
>     :test1 a :SUCCESS
> } .
>
> (it works in cwm but not eye, as the latter skolemizes the blank node,
> even when directly embedded in the rule premise)
>
> And the following should not, I suppose:
>
> { :will :hasName "will" } :label "formula1" .
> { _:x :hasName "will" } :label "formula2" .
>
> { ?f1 :label "formula1" .
>   ?f2 :label "formula2" .
>   ?f1 log:includes ?f2 } => { :test1 a :SUCCESS } .
>
> (again, works in cwm but not eye)
>
>
> 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:
> 1/ 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
> and so ':d :e :f' is no longer produced.
> 2/ all the other tests at
> 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>
> 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>:
>> >
>> > 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>
>>
>>