Re: Discussion from today

the example is adapted at http://ppr.cs.dal.ca:3002/n3/editor/s/57nZbogQ
and both cwm and eye give the same results:

@prefix : <#> . :bob a :NaivePerson1, :NaivePerson2, :NaivePerson3,
:NaivePerson4, :NaivePerson5, :NaivePerson6, :NaivePerson7, :NaivePerson8 .

-- https://josd.github.io


On Mon, Jan 31, 2022 at 5:33 PM Jos De Roo <josderoo@gmail.com> wrote:

> 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
>
>
> On Mon, Jan 31, 2022 at 5:03 PM Pierre-Antoine Champin <
> 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
>>
>>
>> On Wed, Jan 26, 2022 at 3:20 PM Doerthe Arndt <
>> 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
>>>
>>>
>>> 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
>>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>
>>>>
>>>