Re: Blank node quantification

Dear all,

As we identified them as different topics, I will treat dynamic scoping and context dependent quantification as two different cases:

1. Dynamic scoping: After carefully reading William’s mail again, I am still not sure whether I fully understand what you want here. Do you want the following to be correct (copied from our meeting minutes, not supported by EYE)?
_:y :b :c.
{?U_0 :b ?U_1} => {{?U_0 :u :v} => {?U_1 :b :c}}.
Produces
{?U_2 :u :v} => {:c :b :c}.

If so,  I dislike the whole idea because it seems to be far away from first order logic and thereby from RDF. How would you write a proof for the reasoning above?  How would you  translate it into first order logic (this should be possible in this case since we do not use cited formulas).


2. As a second point, I thought about the context dependent quantifiers and I think having these would break our built-ins. As an example, take log:semantics:

If we have a file containing a blank node like for example

[] a :Unicorn.

„Unicorns exist."

And we write a rule saying that we do not trust the information in that file using log:semantics:

{<example.n3> log:semantics ?x} => {we doubt ?x }.

Using the traditional interpretation, we would conclude

:we doubt {[ ] a :Unicorn.}.

„We doubt that unicorns exist“

This would be exactly what I would expect here. But the last expression would, following the new proposal, mean: „There is some instance x and we doubt that this instance is a unicorn.“ This is not what log:semantics is expected to do. The built-in is meant to provide the content of a file which can then be used for further reasoning. So, here we need some extra solution. We could try to use a skolem iri in the output and simply create a witness.

:we doubt {:skolemiri_x a :Unicorn.}.

This solution is not wrong, but we loose information here.

You can see a modified example for the described behavior here (I [] a :Person. instead of [] a :Unicorn. because that triple was already present in the examples we discussed): Link<http://ppr.cs.dal.ca:3002/n3/editor/s/2kqzxbi2>

I did not check yet, but I would expect similar problems for other builtins.

Kind regards,
Dörthe




Am 22.06.2021 um 20:22 schrieb William Van Woensel <william.vanwoensel@gmail.com<mailto:william.vanwoensel@gmail.com>>:



On 2021-06-22 12:50 p.m., Pierre-Antoine Champin wrote:
(1) is not absolutely correct, although it "works" for simple cases (complex cases being: if you have rules inside rules...)

Can you give an example of where this does not work?

(2) As I pointed out at the end of our last call, the question of static vs. dynamic scoping is orthogonal to the question of where we put the implicit quantifiers. Let's rephrase by saying that "the purpose is to place implicit quantifiers in a way that hopefully makes it easier to cleanly implement dynamic scoping".

Do you mean static scoping here? ..


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