Re: Blank node quantification

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