Re: Discussion from today

Dear Doerthe,

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.

Kind regards,
Jos

-- https://josd.github.io


On Wed, Jan 26, 2022 at 2:07 PM Doerthe Arndt <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>:
>
> 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
>
>
> On Tue, Jan 25, 2022 at 4:07 PM Jos De Roo <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 <William.Van.Woensel@dal.ca>
>> resolves
>> https://github.com/william-vw/n3-editor-js/issues/5
>>
>> Kind regards,
>> Jos
>>
>> -- https://josd.github.io
>>
>>
>> On Tue, Jan 25, 2022 at 1:29 PM Doerthe Arndt <
>> 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>:
>>>
>>> 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
>>>
>>>
>>> On Tue, Jan 25, 2022 at 11:56 AM Jos De Roo <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
>>>>
>>>>
>>>> On Tue, Jan 25, 2022 at 10:46 AM Doerthe Arndt <
>>>> 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>:
>>>>>
>>>>> 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>:
>>>>>
>>>>> 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
>>>>>
>>>>>
>>>>> On Mon, Jan 24, 2022 at 11:21 PM Doerthe Arndt <
>>>>> 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
>>>>>>
>>>>>
>>>>>
>>>>>
>>>
>