Re: Discussion from today

Dear Pierre-Antoine,

I dislike here that you introduce a new blank node and - as we all know - nested blank nodes in N3 can be problematic, so I would like to avoid them where possible.

I also still don't understand the problem you had with the other proposal. The subject of the quantification triple is a list, there is only one graph involved. What am I missing here?

Kind regards,
Dörthe

Am Montag, 31. Januar 2022, 17:34:51 MEZ hat Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>> Folgendes geschrieben:


Nice and I have done a small test at http://ppr.cs.dal.ca:3002/n3/editor/s/HO51TdBf

and so far it works for nesting and triple permutation too.

Jos

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


On Mon, Jan 31, 2022 at 5:03 PM Pierre-Antoine Champin <pierre-antoine.champin@ercim.eu<mailto:pierre-antoine.champin@ercim.eu>> wrote:

I find interesting the proposal of modelling explicit quantification with "standard" triples.

However, I find the log:scope construction weird, using two levels of graphs

  { (log:universal ?x) log:scope { ?x :b :c }

why not simply something like

  [ log:universal ?x ; log:graph { ?x :b :c } ]

?

Some experiment here (using blank nodes rather than quickvars for the "quantified" variables)

http://ppr.cs.dal.ca:3002/n3/editor/s/yi3A4XKi


  pa

On 26/01/2022 15:54, Jos De Roo wrote:
Dear Doerthe,

Blank nodes occurring in built-ins (such as log:implies) are in
our current implementation local to the built-in.

Kind regards,
Jos

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


On Wed, Jan 26, 2022 at 3:20 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>> wrote:
Dear Jos,



In our current implementation blank nodes are N3 document global
so we already have "(global) existential quantification on top level"
and it is indeed done with blank nodes.

Do you also do that with blank notes occurring in rules? Or do we need a solution for these?

Kind regards,
Dörthe



Kind regards,
Jos

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


On Wed, Jan 26, 2022 at 2:07 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>> wrote:
Dear Jos,

The nesting and the opportunity to use that to impose an order on the quantifiers was one of the motivations for the proposal. I am still wondering whether it would be better to have a more special notion for quantification (like @forAll) to make sure that people only  manipulate quantified triples when they know what they are doing, but I am not sure yet. For sure the notion has the advantage of an explicit scope.

What is still missing here is a way to have (global) existential quantification on top level. We could change the meaning of blank nodes or use the explicit quantifier here? What would you propose?

Kind regards,
Dörthe

Am 26.01.2022 um 13:49 schrieb Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>>:

Dear Doerthe,

To deal with both log:universal and log:existential we can simply use
nested log:scope like in the example http://ppr.cs.dal.ca:3002/n3/editor/s/1Jisg9ES


@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://example.org/etc#>.

:bob :smurfs {
    (log:universal :a) log:scope {
        (log:existential :x :u) log:scope {
            :x a :Unicorn.
            :u :p :x.
        }.
        :a :p :o.
    }
}.

{
    ?y :smurfs {
        (log:universal :b) log:scope {
            :b :p :o.
            (log:existential :v :y) log:scope {
                :v :p :y.
                :y a :Unicorn.
            }
        }
    }
} => {
    ?y a :NaivePerson.
}.

Using the latest eye<https://github.com/josd/eye/releases/tag/v22.0126.1149> it can derive

:bob a :NaivePerson.

Kind regards,
Jos

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


On Tue, Jan 25, 2022 at 4:07 PM Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>> wrote:
Dear Doerthe,

Your log:scope is an excellent proposal and I was able to extend unify/2
in the latest eye https://github.com/josd/eye/releases/tag/v22.0125.1445

so that http://ppr.cs.dal.ca:3002/n3/editor/s/SHY7RXbG should give
:bob a :NaivePerson1 but not :bob a :NaivePerson1
of course after that @William Van Woensel<mailto:William.Van.Woensel@dal.ca>  resolves
https://github.com/william-vw/n3-editor-js/issues/5


Kind regards,
Jos

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


On Tue, Jan 25, 2022 at 1:29 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>> wrote:
Dear Jos,

That is very interesting and I like the compact notion. I am not sure about the use of the universal, but that is a separate discussion.  I  still have two bigger concerns:

1. We can only quantify over triples and not over formulas which is what we would actually need.
2. The quoted variable could still be seen as a constant, look for example here: http://ppr.cs.dal.ca:3002/n3/editor/s/ioYMxfcC


So we could do something like :bob :smurfs { (log:existential :x) log:scope {:x a :Unicorn.} }.

This looks far less elegant than your solution but we have the advantage that the scope is clearly defined and that we can quantifiy over formulas. Maybe you have an idea ho to improve that?

Kind regards,
Dörthe

Am 25.01.2022 um 12:20 schrieb Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>>:

Dear Doerthe,

Forgot to point to a concrete example http://ppr.cs.dal.ca:3002/n3/editor/s/IT3znjsL

Here the log: namespace is (mis)used instead of the e: namespace.
Both Cwm and Eye agree again.

Kind regards,
Jos

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


On Tue, Jan 25, 2022 at 11:56 AM Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>> wrote:
Dear Doerthe,

Agreed and a while ago I did some experiments in which the variables
in quoted graphs were replaced by either
(e:existential ?X)
or
(e:universal ?X)
and then using rules like you also suggested to transform that into
regular data N3 data/rules/queries.

It is also quite close to Pierre-Antoine's proposal of one variable type.
The scope of those variables is the so-called statement level.

It actually worked quite well.

Kind regards,
Jos

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


On Tue, Jan 25, 2022 at 10:46 AM Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>> wrote:
Dear Jos,

I was too fast in the previous mail. There is one example where cwm and Eye differ: http://ppr.cs.dal.ca:3002/n3/editor/s/okGlsqyV


But that does not change the message from the previous mail.

Kind regards,
Dörthe


Am 25.01.2022 um 10:38 schrieb Arndt, Dörthe <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>>:

Dear Jos,

Thank you for sharing. To complete your example, I also added universal quantification: http://ppr.cs.dal.ca:3002/n3/editor/s/IWXT3bhG

The reasoners still both do the same.

I think that from a logical point of view, some of these derivations are problematic.  But I also better understand, why you would be against fully introducing explicit quantification. That would require us to make a whole theory how reasoning works for the cases mentioned and then to also implement it  accordingly which most likely will never be done since there are not that many use cases which really require that complexity.

My proposal was thus more to have some kind of notation for example for proofs with which we can only do further derivation if we express that structure in the rules. Maybe there is a third option between skolem iris and explicit quantification with only minimal support which I am not seeing (yet)?

Kind regards
Dörthe



Am 25.01.2022 um 01:10 schrieb Jos De Roo <josderoo@gmail.com<mailto:josderoo@gmail.com>>:

Dear Doerthe,

I was curious how your 5 examples currently fare with cwm and eye
and they both give the same results! Yes, the same results!

You can try it at http://ppr.cs.dal.ca:3002/n3/editor/s/tR5T9red


So there is a state of the art with explicit quantification and I was
not expecting that cwm and eye were so close here.

Jos

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


On Mon, Jan 24, 2022 at 11:21 PM Doerthe Arndt <doerthe.arndt@tu-dresden.de<mailto:doerthe.arndt@tu-dresden.de>> wrote:
Dear all,

After our meeting today I thought about explicit quantification and can say that I actually like the idea to have it in N3 as some kind of annotation which has no meaning for the reasoning except that it is a kind of pattern. My vision here is that we would have a  variable namespace which can be combined with quantifiers. Whenever a cited graph contains a quantifier, we simply disallow unification with the triples in that graph unless we also have the quantifier. So, if we come back to my example:

:bob :smurfs { @forSome :X. :X a :Unicorn. }.

{ ?y :smurfs { @forSome :X. :X a :Unicorn } } => { ?y a :NaivePerson }.
Should result in :bob a :NaivePerson. but
:bob :smurfs { @forSome :X. :X a :Unicorn. }.

{ ?y :smurfs { _:x a :Unicorn } } => { ?y a :NaivePerson }.
should not.
Of course, things could get more complicated here:
:bob :smurfs { @forSome :X. :X a :Unicorn. }.

{ ?y :smurfs ?g. ?g log:includes {?x a :Unicorn} } => { ?y a :NaivePerson }.
Should not fire, but what about
:bob :smurfs { @forSome :X. :X a :Unicorn. :Unicorn a :MagicalCreature }.

{ ?y :smurfs ?g. ?g log:includes {?x a :MagicalCreature } } => { ?y a :NaivePerson }.
So, here we would have to agree and either decide that the moment that there is a quantifier involved in the graph, we stay away and do not match anything, we could use the name-space to know when not to match or we make a more fine-grained theory about scopes (but here we can really get into the problems, Jos mentioned). An example:
:bob :smurfs { @forSome :X. :X a :Unicorn. :X :says {:sokrates a :Person} }.
{ ?y :smurfs ?g. ?g log:includes {?x :says {:sokrates a :Person} } } => { ?y a :NaivePerson }.
Here, we see that the namspace alone can’t be a reason to allow or disallow a unification. We would need some concept to express, when a triple is scoped, and this theory could indeed get complicated.
(So,I see your concerns here, Jos.)
So, why do I even propose that kind of pattern? The answer is that I like that we would have some way to express the patterns which go beyond our logic which is limited to implicit quantification without loosing the possibility to involve them to our theory. We could then explicitly define our reasoning calculus which only allows implicit quantification and provide rules to support more sophisticated theories. We cannot express that by only having constants because then there would be no way of blocking unification.
My ideas are not really thought through yet (it cn perfectly be that I change my mind next week, also depending on your comments ;) ). But I wanted to elaborate why (for now), it seems to be an interesting idea to me.
Kind regards
Dörthe